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