Injective type families

[lunaris]

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.

[lunaris]

Demonstration of injective families

[lunaris]

Patch against GHC HEAD to support injective families

[lunaris]

Oops -- I forgot to list all that was wrong with the current implementation. Namely:

• In the example, g's type is inferred as a -> a (and not G a -> G a). This is in some sense `correct', but seems a bit dodgy.

• I don't actually *enforce* that the declared instances of a family *are* injective yet -- I've put that off until what's there is semi-stable.

• I've messed up and inadvertently included whitespace changes in one of the patches. Apologies.

[simonpj]

Some functions might be injective in one argument but not another. For example:

  F a b ~ F c d   ===>    a ~ c
                but not   b ~ d

[lunaris]

Indeed; I'd not considered that case. I'm not aware of a well-defined semantics for injective type functions in the context of constraint solving so I've no idea how to proceed. There are of course syntactic complications also.

[mokus]

An interesting use case is type-level co-naturals using -XDataKinds (which I'm using as the "height" type index for an experimental 2^{k-tree implementation):}

data Nat 
    = Zero
    | Suc Nat

data CoNat
    = Co Nat
    | Infinity

type family Succ (t ::  CoNat) :: CoNat
type instance Succ (Co n)           = Co (Suc n)
type instance Succ Infinity         = Infinity

Succ can't be a constructor, because then Succ Infinity /~ Infinity. Succ as a type family half-works, but you end up needing (logically-)unnecessary type annotations all over the place because GHC doesn't know that Succ n ~ Succ m => n ~ m. It might be possible to devise some kind of type-level bisimilarity constraint, but I suspect it would actually increase the need for type annotations rather than decrease it.

I've also tried an alternate definition of the tree type using "Pred" instead of "Succ", but that seems to lead to really bizarre types - it accepts obviously non-flat trees at a type indicating that the tree's height is zero (or actually, any CoNat? I want), because it accepts the existence of types such as "Pred (Co Zero)". Is this expected behavior (e.g., due to the open-world assumption) or should I file a bug report on that?

[igloo]

Simon, I'm no sure what the status of this is, but it looks like your area so I'm assigning it to you.

[conal]

Note  this discussion, which includes the subtlety of injective in various arguments (holding other fixed).

[goldfire]

Also see the discussion in #4259, which is about strengthening type families along a different dimension. The two tickets are related.

[morabbin]

Noting for completeness: possibly related to #7205 and #5591.

Why I'm interested: I'm modeling the Java type system in Haskell (overload resolution in particular) a la chak and Andrew's Salsa, using type families and type functions heavily. Their code worked under earlier versions of GHC, but not under 7.4 and beyond.

[simonpj]

Andy, No version of GHC had injective families. If you have code that you think should work, and used to, and doesn't now, by all means submit a but report!

Simon

[morabbin]

It turns out I was missing -XscopedTypeVariables?. I'm still interested in injective type families, but it's not a blocker (and Manuel and Andrew's code still compiles).