Injective type families

[Richard Eisenberg]

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.stolarek at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs