Injective type families

[Gabor Greif]

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 <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
>