Injective type families

[Jan Stolarek]

Hi all,

I'd like to take a stab at implementing injective type families (#6018). My plan of attack looks 
like this:

1. Implement injective type families that are:
   a) injective in all arguments
   b) only admit RHS that is a concrete type or a type variable introduced by the LHS or a 
recursive call to self.
2. Lift restriction a) ie. allow type families injective only in some arguments
3. Lift restriction b) ie. allow injective type families to call other type families.

I'm not sure if 3) really gets implemented as this seems more in lines of #4259, which I don't 
intend to approach.

Now, let's discuss the most important of all matters - the syntax! :-) Note that syntax must:
1. allow to define injectivity only for some parameters
2. work for both open and closed type families

Here's my proposal (based on Richard's idea to use functional-dependencies-like syntax):

1. Standard injective type family (all parameters uniquely determined by the RHS):

   injective type family F a b c | a b c
   type family instance F Int  Char Bool = Bool
   type family instance F Char Bool Int  = Int
   type family instance F Bool Int  Char = Char

2. Type family injective only in some parameters (ie. only some parameters uniquely determined by 
the RHS):

   injective type family G a b c | a b
   type family instance G Int  Char Bool = Bool
   type family instance G Int  Char Int  = Bool
   type family instance G Bool Int  Int  = Int

   Here knowing the RHS allows us to determine a and b, but not c.

3. Type families where knowing the RHS and some parameters on the LHS makes other parameters 
injective:

   Example 1: knowing the RHS and any single parameter uniquely determines other parameters

   injective type family H a b c | a -> b c, b -> a c, c -> a b
   type family instance H Int  Char   Double = Int
   type family instance H Bool Double Char   = Int

   Example 2: knowing the RHS and either a or b allows to uniquely determine other parameters, but 
knowing the RHS and c gives us no information about a or b

   injective type family J a b c | a -> b c, b -> a c
   type family instance J Int  Char   Double = Int
   type family instance J Bool Double Double = Int

For closed type families this notation would be identical: type family declaration would be 
followed by the "where" keyword.

In comment 34 of #6018 Richard proposed a notation that uses a keyword "Result". This would allow 
for a more uniform notation. Notice that in my proposal some families use ->, while others don't. 
The idea is that on the right side of the arrow we write what we can infer from the things on the 
left of the arrow. If the only thing left of the arrow is the right hand side of the type family 
equation (the result) then the arrow can be elided. In other words these would be equivalent:

   injective type family F a b c | a b c
   injective type family F a b c | result -> a b c

   injective type family G a b c | a b
   injective type family G a b c | result -> a b
   (note: it is also true that "injective type family G a b c | result c -> a b")

   injective type family H a b c | a -> b c, b -> a c, c -> a b
   injective type family H a b c | result a -> b c, result b -> a c, result c -> a b

   injective type family J a b c | a -> b c, b -> a c
   injective type family J a b c | result a -> b c, result b -> a c

I find the notation explicitly using "result" to be easier to understand, but it is also more 
verbose. I also suspect that it might be a bit easier to parse. Which of the notations do you 
find better? What do you think about using the "injective" keyword? Are there any alternative 
proposals?

Janek