[GHC] #6018: Injective type families

[GHC]

#6018: Injective type families
-------------------------------------+-------------------------------------
        Reporter:  lunaris           |                   Owner:  jstolarek
            Type:  feature request   |                  Status:  new
        Priority:  normal            |               Milestone:  7.12.1
       Component:  Compiler          |                 Version:  7.4.1
      Resolution:                    |                Keywords:
Operating System:  Unknown/Multiple  |  TypeFamilies, Injective
 Type of failure:  None/Unknown      |            Architecture:
      Blocked By:                    |  Unknown/Multiple
 Related Tickets:  #4259             |               Test Case:
                                     |                Blocking:
                                     |  Differential Revisions:  Phab:D202
-------------------------------------+-------------------------------------

Comment (by jstolarek):

 Dominic, do throw in thoughts at any time. My patch will be ready Real
 Soon Now but after the merge there will be room for further development of
 this feature.

 I will not comment on the proposal of having a separate kind for injective
 type families. I don't have sufficient knowledge of typechecker to judge
 whether this would make things easier. Perhaps Simon or Richard can offer
 some insight here. Regarding your proposed new syntax I believe it does
 not offer anything new compared to the syntax we decided to use (unless I
 missed something?). These pairs of definitions would be equivalent:

 {{{#!hs
 type family Id a = result | result -> a where {...}
 type family (Id :: * >-> *) a where {...}

 type family F a b c = d | d -> a b c
 type family (F :: * >-> * >->) a b c

 type family G a b c = foo | foo -> a b where
 type family (G :: * >-> * -> *) a b c
 }}}

 Your syntax however does not extend to injectivity where knowing the
 result and some of the arguments allows to determine some other arguments:

 {{{#!hs
 type family Plus a b = (sum :: Nat) | sum a -> b, sum b -> a where
 type family H a b c = xyz | xyz a -> b c, xyz b -> a c
 }}}

 This kind of injectivity is not implemented in my patch but we want to
 leave the door open for such a possibility in the future. I'm also not
 sure if I like how your proposed syntax interacts with PolyKinds: it seems
 that there would be two alternative places to specify kinds.

 David, what do you mean by injectivity lemmas? At the moment I don't have
 a solid stance on the subject of calling type families in the RHS of
 injective type families. When I started this work it seemed to me that
 this is not possible. Now I have some more experience so I plan to revisit
 my earlier decisions. Incidentally, now it seems to me that self-recursion
 might actually be doable. Calling other type families in the RHS still
 seems very problematic. First of all called families would have to be
 injective to declare that a type family that calls them is also
 injective*. This implies that type families would have to be typechecked
 in dependency order, which sounds lika a non-trivial technical obstacle.
 Of course this would prevent type families that form cycles (including
 mutual recursion) from being injective. Another problem is issue of
 overlap:

 {{{#!hs
 type family Foo a = r | r -> a where
      Foo (Bar a)   = X a
      Foo (Baz a b) = Y a b
 }}}

 To determine whether `Foo` is injective or not we must know whether `X a`
 and `Y a b` can have identical values (well, types not values). Given that
 `X` and `Y` can also call other type families I don't see a simple way of
 checking this. Anyway, the ice here seems very thin and I don't feel
 confident proceeding further with calling type families by injective type
 families without formal proof.

 *) This is a simplifying assumption. It is possible to write a type family
 that is injective despite calling non-injective type families.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:107>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler