[GHC] #6018: Injective type families

[GHC]

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

Comment (by goldfire):

 Replying to [comment:84 jstolarek]:
 > Richard, either I'm not getting the subtleties of your arguments or
 you're misunderstanding what I meant to say on the wiki page. Or both :-)
 >
 > I now see the theoretical difference between "overlaps" and "subsumes"
 but I don't yet see how that is important in my algorithm outline. I re-
 read parts of the closed type families paper and now I'm not even sure
 whether I meant "overlaps" or "unifies".

 To be clear, I am considering the expressions "two types overlap" and "two
 types unify" to be synonymous. Subsumption is a finer, directed relation
 between types than overlap/unify.

 > {{{#!hs
 > type family E1 a = r | r -> a where ...
 > }}}

 Yes yes yes. You're right here. I was wrong. The wiki page is updated.

 >
 > Now `E2`:
 >
 > {{{#!hs
 > type family E2 (a:: Bool) = r | r -> a where
 >   E2 False = True
 >   E2 True  = False
 >   E2 a     = False
 > }}}
 > I consider almost identical example on the wiki:
 > {{{#!hs
 > type family Bak a = r | r -> a where
 >      Bak Int  = Char
 >      Bak Char = Int
 >      Bak a    = a
 > }}}
 > The difference is the RHS of the last equation: a concrete type in your
 example, a type variable in mine. Yet I believe that both examples are
 intended to demonstrate the same problem - see discussion below that
 example.

 I think these cases are different. In yours, the RHS unification (`a`
 unifies with `Char`) refines the LHS (`a |-> Char`) so that it is subsumed
 by an earlier equation. This action does not happen in my example, and
 different reasoning (noting that `False` and `True` are both impossible)
 is required.

 > I have a question about closed type families paper. Paragraph just after
 Candidate Rule 2 (section 3.2, page 3) says: "As a notational convention,
 apart(ρ, τ) considers the lists ρ and τ as tuples of types; the apartness
 check does ''not'' go element-by-element.", where "not" is emphasized. Why
 is this important? Seems like the choice of representing patterns and
 types as tuples or lists is just an implementation detail.

 Agreed that choosing a list vs. a tuple is irrelevant, but choosing
 element-by-element vs. as-a-whole is quite important. For example `(a, a)`
 is quite apart from `(Int, Bool)`, when considered as a whole, even though
 `a` is neither apart from `Int` nor `Bool` looking at individual elements.

 Does that clarify?

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