#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