<br><br><div class="gmail_quote">On Wed, Mar 18, 2009 at 9:45 AM, Simon Peyton-Jones <span dir="ltr"><<a href="mailto:simonpj@microsoft.com">simonpj@microsoft.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
[Redirecting to GHC users.]<br>
<div class="im"><br>
| Tom Schrijvers wrote:<br>
| > The cyclic dictionaries approach is a bit fragile. The problem appears to<br>
| > be here that GHC alternates exhaustive phases of constraint reduction and<br>
| > functional dependency improvement. The problem is that in your example you<br>
| > need both for detecting a cycle.<br>
<br>
</div>The whole thing relies on "spotting a loop", and that's inherently a bit fragile. I don't know of any formal work on the subject, although I bet there is some.</blockquote><div><br>Satish R. Thatte:
Semantics of Type Classes Revisited <br></div><a href="http://portal.acm.org/citation.cfm?id=182459">http://portal.acm.org/citation.cfm?id=182459</a><br><br>The first reference I'm aware of which discusses co-induction in the type class context. There are no recursive dictionaries because Thatte's type class semantics uses run-time type passing (plus method lookup) instead of dictionary-passing.<br>
<br>Recursive dictionaries are formalized here<br><br>Martin Sulzmann:
Extracting programs from type class proofs<br><a href="http://portal.acm.org/citation.cfm?id=1140348">http://portal.acm.org/citation.cfm?id=1140348</a><br><br>There's no work I know of which discusses type inference in the presence of co-inductive type classes (and its subtle consequences as pointed out by Tom's earlier email). Chameleon has supported them using the strategy to apply first improvement before considering co-induction.<br>
<br>-Martin<br><br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;"><br>
<br>
GHC's current algorithm does not run functional dependencies sufficiently aggressively, because it treats fundeps a different kind of thing to class constraints. Our new solver, long promised but still in the works, fully integrates type classes with type equalities (fundeps, type functions etc), and so should do a better job here. Roughly speaking, the idea is to combine our ICFP'08 paper [1] with a type-class solver. Since writing the ICFP'08 paper we have found some very useful simplifications; and we also have a new plan for the solving strategy "OutsideIn" [2].<br>
<br>
That said, solving recursive problems is not our primary focus right now -- getting it working is -- so I can't promise that it'll do a better job, but I think it will.<br>
<div class="im"><br>
| It seems we can convince GHC to do constraint reduction and<br>
| improvement in the order we desire. The key is to use the<br>
| continuation-passing style -- which forces things to happen in the<br>
| right order, both at the run-time and at the compile time.<br>
<br>
</div>Oleg you are a master at persuading GHC's somewhat ad-hoc implementation to dance to your tune. But it'd be better just to make the implementation more complete in the solutions it finds. That's what we are working on now.<br>
<br>
Simon<br>
<br>
[1] <a href="http://research.microsoft.com/%7Esimonpj/papers/assoc-types/index.htm" target="_blank">http://research.microsoft.com/~simonpj/papers/assoc-types/index.htm</a><br>
[2] <a href="http://research.microsoft.com/%7Esimonpj/papers/gadt" target="_blank">http://research.microsoft.com/~simonpj/papers/gadt</a><br>
_______________________________________________<br>
Glasgow-haskell-users mailing list<br>
<a href="mailto:Glasgow-haskell-users@haskell.org">Glasgow-haskell-users@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/glasgow-haskell-users" target="_blank">http://www.haskell.org/mailman/listinfo/glasgow-haskell-users</a><br>
</blockquote></div><br>