Injective type families
Injective type families have been discussed several times on the mailing list and identified as a potentially useful feature.
I've naively attempted a proof-of-concept in GHC. It's almost certainly incorrect and probably breaks the type system, but I thought it best to put it here and see if it can be made workable.
In summary, my changes are:
Add a new keyword,
injective, which is available only when the
TypeFamiliesextension is enabled. Injective families may then be defined thus:
` injective family F a :: * type instance F Int = Bool type instance F Bool = Int
injective family G a :: * type instance G a = a `
Syntax is of course completely changeable; I've simply picked one of the possible designs. Hopefully this won't be subjected to too much bike-shedding.
Add the constructor
TyConRhsand the family flavour
HsSyn. Again, I've opted to encode injectivity as a flavour rather than (say) a
Boolattached to type families. This is a completely arbitrary choice and may be utterly stupid.
Altered the definition of decomposable
TyCons to include injective families (
isDecomposableTyCon). This effectively introduces a typing rule that says if we have
(F a ~ F b)then we can deduce
(a ~ b)(
Modified the unifier so that it will attempt to replace saturated injective families with their left-hand sides where possible (
TcUnify). This means that in a function such as:
f :: F a -> F a f = ...
The type of
f False is inferred as
F Int (i.e.,
a is no longer ambiguous).
Some things work, some things don't. For example, the attached file typechecks, but if I actually try to evaluate
f False I get nothing (not even a Segmentation fault).
See what you think.