[Haskell-cafe] Mild confusion around type family

[Adam Gundry]

On 18/06/15 17:19, Nicholls, Mark wrote:
>> data Z
>> data S n
> 
>> type family Sub a b
>> type instance Sub a Z = a
>> type instance Sub (S a) (S b) = Sub a b
> 
> I want this to be a type error!...but the above type family appears to
> not be partial…this IS defined….”Sub Z (S Z)” is a type! (I thought it
> wasn’t)
> 
>> oneMinusTwo :: Sub Z (S Z)
>> oneMinusTwo = undefined :: Sub (S Z) (S (S Z))

This is a slightly subtle point about type families. The type family
application `Sub Z (S Z)` does not reduce, but neither is it an error.
In this case, because Sub is an open type family, there is nothing to
stop someone subsequently defining something like

    type instance Sub Z (S b) = Z

in another module.

Type families are functional relations, not functions in the FP sense.

See also the discussion here, about the corresponding situation for a
closed type family: https://ghc.haskell.org/trac/ghc/ticket/9636

Hope this helps,

Adam

-- 
Adam Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/