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. |
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 -- Best, Artem On Fri, 22 Jun 2018 at 12:46 Benjamin Franksen <[hidden email]> wrote: I have observed that type functions seem to be lazy. A type function _______________________________________________ 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'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 <[hidden email]> wrote:
_______________________________________________ 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. |
On 06/22/2018 08:40 PM, Matt wrote:
> 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` Thanks! That was exactly the missing piece. Cheers Ben _______________________________________________ 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. |
In reply to this post by Matt
On Jun 22, 2018, at 2:40 PM, Matt <[hidden email]> wrote:
> Haskell's type families are strict Not quite. Haskell's type families have no specific order of operation, at all. Here's a telling example: > data Nat = Zero | Succ Nat > > type family Inf where > Inf = Succ Inf > > type family F a b where > F True x = Int > F False x = Char > > type family Not a where > Not True = False > Not False = True > > x :: F True Inf > x = 5 > > y :: F False Inf > y = 'a' > > z :: F (Not False) Inf > z = 42 Any attempt to evaluate Inf will cause GHC's evaluation stack to overflow and will result in an error. But x and y are accepted, because GHC can reduce F right away. z, on the other hand, causes this stack overflow, because GHC needs to reduce arguments in order to reduce F. GHC is not clever enough to notice that it needs to reduce only the first argument. This is silly, but it's unclear how to performantly do better. Richard _______________________________________________ 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. |
Free forum by Nabble | Edit this page |