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 [email protected] http://www.haskell.org/mailman/listinfo/ghc-devs
