<div dir="ltr">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.<div><br></div><div>If you want a type family to work on defined cases, and error otherwise, you must write a manual TypeError message:</div><div><br></div><div>type family TurnOff (s :: Bool) where<br> TurnOff True = False<br> TurnOff _ = TypeError (Text "You tried to use TurnOff with False, but it can only be used with True.")<br><br>Where TypError etc comes from `GHC.TypeLits`</div></div><div class="gmail_extra"><br clear="all"><div><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div>Matt Parsons</div></div></div></div>
<br><div class="gmail_quote">On Fri, Jun 22, 2018 at 12:22 PM, Artem Pelenitsyn <span dir="ltr"><<a href="mailto:a.pelenitsyn@gmail.com" target="_blank">a.pelenitsyn@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>Dear Benjamin,</div><div><br></div><div>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?</div><div><br></div><div>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 (<a href="https://cs.brynmawr.edu/~rae/papers/2012/singletons/paper.pdf" target="_blank">https://cs.brynmawr.edu/~rae/<wbr>papers/2012/singletons/paper.<wbr>pdf</a>). <br></div><div><br></div><div>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.</div><div><br></div><div><span style="font-family:monospace"><span class="">{-# LANGUAGE DataKinds, TypeFamilies #-}<br><br></span>data State (s :: Bool) = State deriving Show<span class=""><br><br>off :: State False<br>off = State<br><br></span><span class="">type family TurnOff s where<br> TurnOff True = False<br><br></span><span class="">turnOff :: State True -> State False<br></span>turnOff State = State<br><br>bad = turnOff off -- <-- error: Couldn't match type ‘'False’ with ‘'True’<br><br>main = print bad</span></div><div><a href="https://ideone.com/boWN1q" target="_blank">https://ideone.com/boWN1q</a></div><div><br></div><div>--</div><div>Best, Artem<br></div><div><br></div><div><br></div></div><div class="HOEnZb"><div class="h5"><br><div class="gmail_quote"><div dir="ltr">On Fri, 22 Jun 2018 at 12:46 Benjamin Franksen <<a href="mailto:ben.franksen@online.de" target="_blank">ben.franksen@online.de</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I have observed that type functions seem to be lazy. A type function<br>
that is partial does not give me a type error when it is called with an<br>
argument for which it is not defined.<br>
<br>
Is there a 'seq' at the type level?<br>
<br>
Here is my use case, simplified of course. Suppose we want to statically<br>
track the state of a switch with a phantom type parameter:<br>
<br>
> {-# LANGUAGE DataKinds, TypeFamilies #-}<br>
><br>
> data State (s :: Bool) = State Bool deriving Show<br>
><br>
> off :: State False<br>
> off = State False<br>
<br>
We want user code to be able to call the function 'turnOff' only if the<br>
switch is currently on:<br>
<br>
> turnOff :: State True -> State False<br>
> turnOff (State True) = State False<br>
<br>
This works fine:<br>
<br>
*Main> turnOff off<br>
<br>
<interactive>:1:9: error:<br>
? Couldn't match type ?'False? with ?'True?<br>
Expected type: State 'True<br>
Actual type: State 'False<br>
<br>
But now I want to abstract this pattern and write a (closed) type function<br>
<br>
> type family TurnOff s where<br>
> TurnOff True = False<br>
<br>
> turnOff' :: State x -> State (TurnOff x)<br>
> turnOff' (State True) = State False<br>
<br>
> bad = turnOff' off<br>
<br>
*Main> :t bad<br>
bad :: State (TurnOff 'False)<br>
*Main> bad<br>
*** Exception: TypeLevelSeq.lhs:37:3-37: Non-exhaustive patterns in<br>
function turnOff'<br>
<br>
______________________________<wbr>_________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/haskell-<wbr>cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div>
</div></div><br>______________________________<wbr>_________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/haskell-<wbr>cafe</a><br>
Only members subscribed via the mailman list are allowed to post.<br></blockquote></div><br></div>