<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">https://cs.brynmawr.edu/~rae/papers/2012/singletons/paper.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">{-# LANGUAGE DataKinds, TypeFamilies #-}<br><br>data State (s :: Bool) = State deriving Show<br><br>off :: State False<br>off = State<br><br>type family TurnOff s where<br>  TurnOff True = False<br><br>turnOff :: State True -> State False<br>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">https://ideone.com/boWN1q</a></div><div><br></div><div>--</div><div>Best, Artem<br></div><div><br></div><div><br></div></div><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">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>
_______________________________________________<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-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div>