Ticket #6018 (new feature request)
Injective type families
|Reported by:||lunaris||Owned by:||simonpj|
|Keywords:||TypeFamilies, Injective||Cc:||simonpj@…, mokus@…, eir@…, nathanhowell@…, nfrisby, conal@…, shane@…, andy.adamsmoran@…, byorgey@…|
|Type of failure:||None/Unknown||Difficulty:||Unknown|
|Test Case:||Blocked By:|
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 TypeFamilies extension 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 InjFamilyTyCon to TyConRhs and the family flavour InjectiveFamily to HsSyn. Again, I've opted to encode injectivity as a flavour rather than (say) a Bool attached 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) (TcCanonical).
- 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.