[TYPES] OutsideIn(X) question

[Dimitrios Vytiniotis]

Dear Alejandro, thanks for your notice!

You are right, the entailment relation in the JFP paper is too weak for type classes. As we formulated it, the simplifier can take a type class reduction step but there is no way to show that the new set of constraints is equivalent to the original class constraint. 

There is nothing very deep going on, it's an oversight in the definition of entailment. The fix -- at least in the case of non-overlapping instances and vanilla multi-parameter type classes -- is to ensure that all axioms for type class instances form bi-implications. In fact in the constraint handling rules formulation of type classes, class instances always gave rise to such bi-implications. 

I will post the correction to the article on my web page in the next couple of weeks and let you know, but I thought I should send an update. 

Best regards, 
Dimitrios


-----Original Message-----
From: Types-list [mailto:types-list-bounces at lists.seas.upenn.edu] On Behalf Of Alejandro Serrano Mena
Sent: Thursday, February 27, 2014 10:18 AM
To: types-list at lists.seas.upenn.edu
Subject: [TYPES] OutsideIn(X) question

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Dear Types List,
I have a small question related to the "OutsideIn(X): Modular type inference with local assumptions" and was hoping that you could help me a bit.
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.