Injective type families
|Reported by:||lunaris||Owned by:||jstolarek|
|Keywords:||TypeFamilies, Injective||Cc:||simonpj@…, mokus@…, eir@…, nathanhowell@…, nfrisby, conal@…, shane@…, andy.adamsmoran@…, byorgey@…, douglas.mcclean@…, ollie@…, acowley@…, ekmett@…, jan.stolarek@…, ggreif@…, vogt.adam@…, haskell@…|
|Type of failure:||None/Unknown||Test Case:||T6018, T6018fail, T6018rnfail, T6018th, T6018failclosed1, T6018failclosed2, T6018ghci, T6018ghcifail, T6018ghcirnfail|
|Related Tickets:||#4259, #10832, #10833||Differential Rev(s):||Phab:D202|
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 Falseis inferred as
ais 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.
Change History (121)
comment:112 Changed 19 months ago by
|Status:||new → closed|
|Test Case:||→ T6018, T6018fail, T6018rnfail, T6018th, T6018failclosed1, T6018failclosed2, T6018failclosed3, T6018failclosed4, T6018failclosed5, T6018failclosed6, T6018failclosed7, T6018failclosed8, T6018failclosed9, T6018failclosed10, T6018failclosed11, T6018failclosed12, T6018ghci, T6018ghcifail, T6018ghcirnfail|
comment:117 Changed 19 months ago by
|Test Case:||T6018, T6018fail, T6018rnfail, T6018th, T6018failclosed1, T6018failclosed2, T6018failclosed3, T6018failclosed4, T6018failclosed5, T6018failclosed6, T6018failclosed7, T6018failclosed8, T6018failclosed9, T6018failclosed10, T6018failclosed11, T6018failclosed12, T6018ghci, T6018ghcifail, T6018ghcirnfail → T6018, T6018fail, T6018rnfail, T6018th, T6018failclosed1, T6018failclosed2, T6018ghci, T6018ghcifail, T6018ghcirnfail|