[Haskell-cafe] OutsideIn(X) question

[Charles-Pierre Astolfi]

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
<trupill at gmail.com>wrote:

> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140227/b37f0cf8/attachment.html>