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 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.

Trac metadata

Trac field	Value
Version	7.4.1
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	simonpj@microsoft.com
Operating system
Architecture