OutsideIn(X) question
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.
On Wed, Feb 26, 2014 at 10:07 AM, Alejandro Serrano Mena
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 :)
If you don't get an answer, consider the glasgow-haskell-users list. -- brandon s allbery kf8nh sine nomine associates allbery.b@gmail.com ballbery@sinenomine.net unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net
Hi Alejandro,
This is definitely a question for the Types forum: types-list@
lists.seas.upenn.edu
This list is research oriented, low traffic, and mostly read by people
working on type theory. Threads are usually about questions in type theory
papers just like yours.
Cheers,
--
Cp
On Wed, Feb 26, 2014 at 4:07 PM, Alejandro Serrano Mena
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.
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
participants (3)
-
Alejandro Serrano Mena -
Brandon Allbery -
Charles-Pierre Astolfi