[Haskell-cafe] 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
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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20180622/0078cce5/attachment.html>