Injective type families

[Isaac Dupree]

On 07/10/2014 02:34 PM, Gabor Greif wrote:
> Jan, this is great! Thanks for attacking this issue.
> 
> Regarding "result", I do not like the idea to introduce arbitrary
> words with special meanings. What if somebody writes
> 
>>    injective type family F a result c | result -> a result c
> 
> it will be totally confusing.
> 
> One could write like this:
> 
>>    injective type family F a b c | F a b c -> a b c  -- (*)
> 
> or even shorter:
> 
>>    injective type family F a b c | F -> a b c  -- (**)
> 
> in (*) the syntax is inconsistent because to the left of the "|"
> juxtaposition is not meaning application. Also (*) would permit "... |
> F x b c -> a b c" which is confusing and would require a naming rule.
> 
> (**) can be read as "F's result uniquely determines all of a b and c".
> It sounds ok if you repeat it often enough :-)

At the risk of being too clever, one could use the keyword "type" to
reference the result.  If F is a family of types (a "type family"), then
the result is conceptually a single type in this family.

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

-Isaac