[Haskell-cafe] Injective type families for GHC - syntax proposals

[Jan Stolarek]

Haskellers,

there is some discussion going on at the moment about implementing injective
type families in GHC [1]. I'd like to hear your opinions on proposed syntax for this
new feature.

== Problem ==

Currently GHC assumes that type families are not injective. This is of course
conservative and the idea behind implementing injective type families is to
allow the programmer to explicitly declare that a type family has the
injectivity property (which GHC will of course verify).

== Forms of injectivity ==

Injectivity can take forms more complicated than just determining the LHS from
RHS:

A. RHS determines all arguments on the LHS. Example:

   type family Id a where
        Id a = a

   Here the RHS uniquely determines LHS.

B. RHS determines some but not all arguments on the LHS. Example (contrieved):

   type family G a b c where
        G Int  Char Bool = Bool
        G Int  Char Int  = Bool
        G Bool Int  Int  = Int

   Here RHS uniquely determines `a` and `b` but not `c`.

C. RHS and some LHS arguments uniquely determine some LHS arguments. Example:

   type family Plus a b where
        Plus Z     m = m
        Plus (S n) m = S (Plus n m)

   Here knowing the RHS and one of LHS arguments uniqely determines the other
   LHS argument.

At the moment we've only seen use cases for A, which means that we will most likely only
implement A. If someone comes up with compelling examples of either B or C we
will revise and consider implementing these more involved forms of injectivity.


== Syntax ==

So the most important decission to make is what syntax do we want for this new
feature :-) One of the features we would like is extensibility, ie. if we only
implement injectivity of type A we still want to be able to add injectivities B
and C sometime in the future without breaking A.

When thinking about syntax an important (and open) question is whether
injectivity becomes part of TypeFamilies language extension or do we add a new
InjectiveTypeFamilies extension for this feature. The problem with incorporating
injectivity into existing TypeFamilies is that we would have to come up with
syntax that is fully backwards compatible with what we have now.

Below is a list of proposals that have come up until now in the discussion
between developers. Note that all proposals are given for closed type families.
For open type families things would be identical except that the `where` keyword
would be skipped.


=== Proposal 1 ===

Use syntax similar to functional dependencies. The injectivity declaration
begins with `|` following type family declaration head. `|` is followed by a
list of comma-separated injectivity conditions. Each injectivity condition has
the form:

{{{
result A -> B
}}}

where `A` is a possibly-empty list of type variables declared in type family
head and `B` is non-empty list of said type variables. Things on the left and
right of `->` are called LHS and RHS of an injectivity condition,
respectively. `result` becomes a restricted word that cannot be used as a type
variable's identifier in a type family head. Examples:

   type family Id a | result -> a where
   type family G a b c | result -> a b where
   type family Plus a b | result a -> b, result b -> a where

Pros:

  * has natural reading: `result a -> b` reads as "knowing the result and the
    type variable a determines b".

  * extensible for the future

Cons:

  * steals `result` identifier in the type family head. This means it would be
    illegal to have a type variable named `result` in a type family.

  * the above also makes this proposal backwards incompatible with TypeFamilies
    extension.

Further proposals are based on this one in an attempt to solve the problem of
stealing syntax and backwards incompatibility.


=== Proposal 2 ===

Use `Result` instead of `result`:

   type family Id a | Result -> a where
   type family G a b c | Result -> a b where
   type family Plus a b | Result a -> b, Result b -> a where

Pros:

  * has natural reading

  * extensible for the future

  * allows to have type variables named `result` (does not steal syntax)

Cons:

  * all other keywords in Haskell are lowercase. This would be the first one
    that is capitalized.

  * confusion could arise if we have a type `Result` and use it in the type
    family head.

Unknowns (for me):

  * not sure if it would be possible to avoid name clash between `Result` and
    type of the same name. If not then this proposal would also be backwards
    incompatible with TypeFamilies.


=== Proposal 3 ===

Use `type` instead of `result`:

   type family Id a | type -> a where
   type family G a b c | type -> a b where
   type family Plus a b | type a -> b, type b -> a where

Pros:

  * extensible for the future

  * no syntax stealing

Cons:

  * no natural reading

  * usage of `type` here might seem unintuitive


=== Proposal 4 ===

Use name of the type family instead of `result`:

   type family Id a | Id -> a where
   type family G a b c | G -> a b where
   type family Plus a b | Plus a -> b, Plus b -> a where

Pros:

  * extensible for the future

  * no syntax stealing

Cons:

  * writing something like `Plus a` might be confusing. It looks as if Plus
    could be partially applied.


== Further discussion ==

I'd like to hear what you think about these proposals. Neither of them is
perfect so perhaps someone can come with something better. You can also check
out the GHC Trac ticket [1] and the GHC Wiki page [2] (which repeats most of this but has some 
more details as well).

[1] https://ghc.haskell.org/trac/ghc/ticket/6018
[2] https://ghc.haskell.org/trac/ghc/wiki/InjectiveTypeFamilies

Janek