id,summary,reporter,owner,description,type,status,priority,milestone,component,version,resolution,keywords,cc,os,architecture,failure,difficulty,testcase,blockedby,blocking,related
6018,Injective type families,lunaris,simonpj,"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 {{{TyCon}}}s 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.
  ",feature request,new,normal,7.8.1,Compiler,7.4.1,,"TypeFamilies, Injective",simonpj@… mokus@… eir@… nathanhowell@… nfrisby conal@… shane@… andy.adamsmoran@… byorgey@…,Unknown/Multiple,Unknown/Multiple,None/Unknown,Unknown,,,,#4259