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