I'm not convinced I have very good taste where it comes to concrete syntax, but I will say that the `injective` keyword below is redundant -- it can be inferred from the presence of the `|`. 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. Thanks for taking this on! Richard On Jul 10, 2014, at 10:37 AM, Jan Stolarek wrote:

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 _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

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 :-) Regarding "injective" I go with Richard. It is unneeded noise. Cheers, Gabor On 7/10/14, Jan Stolarek wrote:

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 _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs