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