[Haskell-cafe] OutsideIn(X) question
Alejandro Serrano Mena
trupill at gmail.com
Wed Feb 26 15:07:56 UTC 2014
Dear Haskell-café,
I don't know if this is the best forum to ask questions about the
OutsideIn(X) paper that lies below type inference in GHC. But given that
this is the place where I know many GHC devs look at, I'll just try :)
My question related about the proof of soundness and principality,
specifically Lemma 7.2 (to be found in page 67). In that lemma, it's stated
that QQ and \phi' Q_q ||- \phi Q_w <-> \phi' Q_w'. I'm trying to recover
the proof (which is omitted in the text), but I stumble upon a wall when
trying to work out what happens in the case an axiom is applied.
In particular, I'm playing with an example where
QQ (the set of axioms) = { forall. C a => D a } (where C and D are
one-parameter type classes)
Q_q = { }
Q_w = { D Int }
Thus, if I apply the rule DINSTW (to be found in page 65), I get a new
Q_w' = { C Int }
Now, if the lemma 7.2 is true, it should be the case that
(1) QQ ||- C Int <-> D Int
which in particular means that I have the two implications
(2) { forall. C a => D a, C Int } ||- D Int
(3) { forall. C a => D a, D Int } ||- C Int
(2) follows easily by applying the AXIOM rule of ||- (as shown in page 54).
However, I don't see how to make (3) work :(
I think that understanding this example will be key for my understanding of
the whole system.
Anybody could point to the error in my reasoning or to places where I could
find more information?
Thanks in advance.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140226/a1051596/attachment.html>
More information about the Haskell-Cafe
mailing list