Type level seq

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
5 messages Options
Reply | Threaded
Open this post in threaded view
|

Type level seq

Ben Franksen
I have observed that type functions seem to be lazy. A type function
that is partial does not give me a type error when it is called with an
argument for which it is not defined.

Is there a 'seq' at the type level?

Here is my use case, simplified of course. Suppose we want to statically
track the state of a switch with a phantom type parameter:

> {-# LANGUAGE DataKinds, TypeFamilies #-}
>
> data State (s :: Bool) = State Bool deriving Show
>
> off :: State False
> off = State False

We want user code to be able to call the function 'turnOff' only if the
switch is currently on:

> turnOff :: State True -> State False
> turnOff (State True) = State False

This works fine:

*Main> turnOff off

<interactive>:1:9: error:
    ? Couldn't match type ?'False? with ?'True?
      Expected type: State 'True
        Actual type: State 'False

But now I want to abstract this pattern and write a (closed) type function

> type family TurnOff s where
>   TurnOff True = False

> turnOff' :: State x -> State (TurnOff x)
> turnOff' (State True) = State False

> bad = turnOff' off

*Main> :t bad
bad :: State (TurnOff 'False)
*Main> bad
*** Exception: TypeLevelSeq.lhs:37:3-37: Non-exhaustive patterns in
function turnOff'

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Type level seq

Artem Pelenitsyn
Dear Benjamin,

I'm not sure I quite get your problem. My guess: you want a type-level guarantee that `turnOff'` function will only be applied to the terms of type `State True`, and so, you expect a compile-time error from `turnOff' off`. Am I get it right?

In your solution you seem to over engineer the solution. You try to relate type-level informaton (the value of of the type parameter `s` of `State`) to the term-level one (the value of the field stored in the `State` datatype). I think you'd better read how this task is solved with the technique known as singletons (https://cs.brynmawr.edu/~rae/papers/2012/singletons/paper.pdf).

But I bet you don't need to solve that task to just address the problem at hand, if I understand the problem correctly. Please, tell me if the simpler solution below suits you: it doesn't use term-level (field of State) information at all.

{-# LANGUAGE DataKinds, TypeFamilies #-}

data State (s :: Bool) = State deriving Show

off :: State False
off = State

type family TurnOff s where
  TurnOff True = False

turnOff :: State True -> State False
turnOff State = State

bad = turnOff off  --  <-- error: Couldn't match type ‘'False’ with ‘'True’

main = print bad

--
Best, Artem



On Fri, 22 Jun 2018 at 12:46 Benjamin Franksen <[hidden email]> wrote:
I have observed that type functions seem to be lazy. A type function
that is partial does not give me a type error when it is called with an
argument for which it is not defined.

Is there a 'seq' at the type level?

Here is my use case, simplified of course. Suppose we want to statically
track the state of a switch with a phantom type parameter:

> {-# LANGUAGE DataKinds, TypeFamilies #-}
>
> data State (s :: Bool) = State Bool deriving Show
>
> off :: State False
> off = State False

We want user code to be able to call the function 'turnOff' only if the
switch is currently on:

> turnOff :: State True -> State False
> turnOff (State True) = State False

This works fine:

*Main> turnOff off

<interactive>:1:9: error:
    ? Couldn't match type ?'False? with ?'True?
      Expected type: State 'True
        Actual type: State 'False

But now I want to abstract this pattern and write a (closed) type function

> type family TurnOff s where
>   TurnOff True = False

> turnOff' :: State x -> State (TurnOff x)
> turnOff' (State True) = State False

> bad = turnOff' off

*Main> :t bad
bad :: State (TurnOff 'False)
*Main> bad
*** Exception: TypeLevelSeq.lhs:37:3-37: Non-exhaustive patterns in
function turnOff'

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Type level seq

Matt
Haskell's type families are strict -- they evaluate (or, try to evaluate) all of their arguments before they compute the result. When a type family doesn't have a matching equation, it is "stuck", and GHC just carries the applied type family around. This can be pretty confusing.

If you want a type family to work on defined cases, and error otherwise, you must write a manual TypeError message:

type family TurnOff (s :: Bool) where
  TurnOff True = False
  TurnOff _ = TypeError (Text "You tried to use TurnOff with False, but it can only be used with True.")

Where TypError etc comes from `GHC.TypeLits`

Matt Parsons

On Fri, Jun 22, 2018 at 12:22 PM, Artem Pelenitsyn <[hidden email]> wrote:
Dear Benjamin,

I'm not sure I quite get your problem. My guess: you want a type-level guarantee that `turnOff'` function will only be applied to the terms of type `State True`, and so, you expect a compile-time error from `turnOff' off`. Am I get it right?

In your solution you seem to over engineer the solution. You try to relate type-level informaton (the value of of the type parameter `s` of `State`) to the term-level one (the value of the field stored in the `State` datatype). I think you'd better read how this task is solved with the technique known as singletons (https://cs.brynmawr.edu/~rae/papers/2012/singletons/paper.pdf).

But I bet you don't need to solve that task to just address the problem at hand, if I understand the problem correctly. Please, tell me if the simpler solution below suits you: it doesn't use term-level (field of State) information at all.

{-# LANGUAGE DataKinds, TypeFamilies #-}

data State (s :: Bool) = State deriving Show

off :: State False
off = State

type family TurnOff s where
  TurnOff True = False

turnOff :: State True -> State False
turnOff State = State

bad = turnOff off  --  <-- error: Couldn't match type ‘'False’ with ‘'True’

main = print bad

--
Best, Artem



On Fri, 22 Jun 2018 at 12:46 Benjamin Franksen <[hidden email]> wrote:
I have observed that type functions seem to be lazy. A type function
that is partial does not give me a type error when it is called with an
argument for which it is not defined.

Is there a 'seq' at the type level?

Here is my use case, simplified of course. Suppose we want to statically
track the state of a switch with a phantom type parameter:

> {-# LANGUAGE DataKinds, TypeFamilies #-}
>
> data State (s :: Bool) = State Bool deriving Show
>
> off :: State False
> off = State False

We want user code to be able to call the function 'turnOff' only if the
switch is currently on:

> turnOff :: State True -> State False
> turnOff (State True) = State False

This works fine:

*Main> turnOff off

<interactive>:1:9: error:
    ? Couldn't match type ?'False? with ?'True?
      Expected type: State 'True
        Actual type: State 'False

But now I want to abstract this pattern and write a (closed) type function

> type family TurnOff s where
>   TurnOff True = False

> turnOff' :: State x -> State (TurnOff x)
> turnOff' (State True) = State False

> bad = turnOff' off

*Main> :t bad
bad :: State (TurnOff 'False)
*Main> bad
*** Exception: TypeLevelSeq.lhs:37:3-37: Non-exhaustive patterns in
function turnOff'

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Type level seq

Ben Franksen
On 06/22/2018 08:40 PM, Matt wrote:

> Haskell's type families are strict -- they evaluate (or, try to evaluate)
> all of their arguments before they compute the result. When a type family
> doesn't have a matching equation, it is "stuck", and GHC just carries the
> applied type family around. This can be pretty confusing.
>
> If you want a type family to work on defined cases, and error otherwise,
> you must write a manual TypeError message:
>
> type family TurnOff (s :: Bool) where
>   TurnOff True = False
>   TurnOff _ = TypeError (Text "You tried to use TurnOff with False, but it
> can only be used with True.")
>
> Where TypError etc comes from `GHC.TypeLits`

Thanks! That was exactly the missing piece.

Cheers
Ben

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Type level seq

Richard Eisenberg-4
In reply to this post by Matt
On Jun 22, 2018, at 2:40 PM, Matt <[hidden email]> wrote:

> Haskell's type families are strict

Not quite. Haskell's type families have no specific order of operation, at all.

Here's a telling example:

> data Nat = Zero | Succ Nat
>
> type family Inf where
>   Inf = Succ Inf
>
> type family F a b where
>   F True x = Int
>   F False x = Char
>
> type family Not a where
>   Not True = False
>   Not False = True
>
> x :: F True Inf
> x = 5
>
> y :: F False Inf
> y = 'a'
>
> z :: F (Not False) Inf
> z = 42

Any attempt to evaluate Inf will cause GHC's evaluation stack to overflow and will result in an error. But x and y are accepted, because GHC can reduce F right away. z, on the other hand, causes this stack overflow, because GHC needs to reduce arguments in order to reduce F. GHC is not clever enough to notice that it needs to reduce only the first argument.

This is silly, but it's unclear how to performantly do better.

Richard

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.