[Haskell-cafe] Mild confusion around type family

Adam Gundry adam at well-typed.com
Fri Jun 19 13:19:32 UTC 2015

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 Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/

More information about the Haskell-Cafe mailing list