#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 jstolarek): I've read section 7.4 of OutsideIn(X) paper. Code makes more sense now but still I have some questions. Most importantly I'm trying to understand FINST top-level reaction rule (OutsideIn paper, fig. 24 page 65), which according to my understanding is implemented by `doTopReactFunEq`. Since I don't have LaTeX in the wiki I'll be using following notation: \Q - set of top-level axiom schemes \g - little gamma \d - little delta \th - little theta \t - little tau \e - little epsilon _0 - 0 in a subscript \vec{...} - a vector of values, in paper denoted using overline \in - set membership realtion Now the rule: {{{ forall \vec{a}. F \vec{Xi_0} ~ Xi_0 \in \Q -- (1) \vec{b} = ftv(\vec{Xi_0}) -- (2) \vec{c} = \vec{a} - \vec{b} -- (3) \g fresh -- (4) \th = [\vec{b |-> \t_a},\vec{c |-> \g}] -- (5) \th \vec{Xi_0} = \vec{Xi} -- (6) if (l = w) then \vec{\d} = \vec{\g} else \vec{\d} = \e -- (7) ------------------------------------------------------------- topreact[l](\Q, F \vec{Xi}~Xi) = {\d, \th Xi_0 ~ Xi} -- (8) }}} Here's how I understand (or misunderstand that rule): Premise (1) represents a type family equation written by the user (either from a closed or open type family). `\vec{Xi_0}` represents the LHS of `F` ie. patterns in that equation. So for example if the equation is `F [b] Bool c` then `\vec{Xi_0}` is `([b],Bool, c)`. I'm not sure about `[b]` - I think that's not canonical? Are axioms canonicalized? I'm also not sure about the meaning of `\vec{a}` in (1)'s forall. My intuition would be that these are type variables in the LHS (`b` and `c` in above example). But then I don't know how to understand premise (2). If `\vec{b}` represents free variables if `\vec{Xi_0}` then wouldn't this be identical to `\vec{a}`? This does not make sense because in that situation `\vec{c}` in premise (3) would always be empty. Premise (5) is a substitution used in premise (6) to turn the LHS of the original axiom into LHS of a constraint we are trying to solve. But what does `\t_a` represent? Instantiation of variables in the original axiom to some particular values present in `\vec{Xi}`? Premise (7) says that if a constraint is wanted then we introduce new variables. I'm not sure why. Maybe this will become clear once I understand the rest. I'm not sure if I understand the conclusion (8). Reading the rule I see that if we have `F \vec{Xi} ~ Xi` constraint we use it to figure out the `\th` substitution and then use that substitution to create a new constraint that tries to equate the RHS of our current constraint with the RHS of original axiom. But why do we want this? I could use an example with more comments than in the paper (and the example could be more complicated too). Before proceeding with the implementation I'd like to understand how injectivity affects FINST rule. What is not clear to me is whether the new constraint we are producing is wanted or given? My guess is that we produce a given if the original constraint was given and wanted if the original was wanted. I also wonder whether injectivity gives us a new interaction rule: {{{ INJFEQFEQ interact[l] (F \vec{Xi_1} ~ Xi, F \vec{Xi_2} ~ Xi) = (F \vec{Xi_1} ~ Xi, \vec{ Xi_1 ~ Xi_2 }) }}} where `\vec{ Xi_1 ~ Xi_2 }` represents vector of pairwise constraints. A few more questions unrelated to the paper: 1. Are axioms for associated types treated differently than for open type families? 2. What does `BuiltInSynFamTyCon` constructor represent? 3. `Note [Basic Simplifier Plan]` in `TcInteract` mentions "inert reactions" and "spontaneous reactions". What's the difference between the two? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/6018#comment:89 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler