Re: [Haskell-cafe] Type level seq

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 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 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.