Injective type families

[Jan Stolarek]

To Richard:
>  the `injective` keyword below is redundant -- it can be inferred from the presence of the `|`.
Yes, I was wondering if someone will point it out. I agree it can be omitted. Since Gabor also 
raised that concern I officially drop the idea of using "injective" keyword :-)

> Also, by restriction (b), I imagine you also allow things like `Maybe a`, where `a` is a
> variable bound on the LHS. That doesn't seem to be included in a tight reading of your
> proposal.
Isn't 'Maybe a' a "concrete type"?

To Kim-Ee:
Roman has this right, but let me attempt to clarify further:
>  I no longer know what "RHS" in OP means! It could be (1) the result. Or (2) the right of the
> vertical bar.
RHS means (1) the result. So in this example:

   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

Bool is the RHS of the first equation, Int is the RHS of the second equation and Char is the RHS 
of the third equation. Note: I sometime use terms "equation" and "clause" interchangeably.

Now that you brought it up it would be a Good Thing to give "(2) the right of the vertical bar" a 
concrete name, so we can refer to it concisely in a discussion. How about "injectivity 
conditions"?

> So when you say "arguments always determine result", one has to pause and think about what that
> means in the presence of multiple arguments as we have here. Because that doesn't hold when
> only some arguments are applied.
Type families cannot be partially applied - you alwyas have all the parameters.

> When a single-argument function is injective, we say that the argument 'uniquely determines'
> (as opposed to just determine) the result.
No, you have the definition backwards. When an argument of a relation uniquely determines the 
result then we call that relation a "function". When a function is injective it means that every 
element of the image is assigned to at most one element of the domain. Which means you can 
determine the argument from the result.

> When defining a type family case-by-case, one works from arguments to the result determined by
> the arguments. But saying "Injectivity means that the *parameters* are determined by the
> result" raises the specter of the inverse function
We want to define functions as injective so that GHC can infer (a ~ b) based on (F a ~ F b). So in 
a sense we want inverse functions here. Why do you say about a "specter of the inverse function" 
as if it was something unthinkable?

To Gabor:
> Jan, this is great! Thanks for attacking this issue.
Thank me when it's implemented.

> Regarding "result", I do not like the idea to introduce arbitrary
> words with special meanings
Well, if we followed that path then certainly "result" would become an "arbitrary word with a 
special meaning" a.k.a. "keyword". I'm not pushing strongly for this (in fact I'm not pushing in 
any direction with the syntax), but these are the alternatives I see:
1) use the "result" keyword: syntax is more coherent and easier to understand, but we pay the 
price of introducing a new keyword and more verbosity
2) don't use the "result" keyword: syntax is shorter, but a bit incoherent which may make it 
harder to understand (it does for me, even though I wrote down these examples).

> What if somebody writes
>
> >    injective type family F a result c | result -> a result c
>
> it will be totally confusing.
This would become an error.

Janek