[Haskell-cafe] Type level seq

[Richard Eisenberg]

On Jun 22, 2018, at 2:40 PM, Matt <parsonsmatt at gmail.com> 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