[Haskell-cafe] 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 <a.pelenitsyn at gmail.com>
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
> https://ideone.com/boWN1q
>
> --
> Best, Artem
>
>
>
> On Fri, 22 Jun 2018 at 12:46 Benjamin Franksen <ben.franksen at online.de>
> 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.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20180622/80d32405/attachment.html>