[Haskell] Re: indirectly recursive dictionaries
martin.sulzmann.haskell at googlemail.com
Thu Mar 19 15:45:41 EDT 2009
On Wed, Mar 18, 2009 at 9:45 AM, Simon Peyton-Jones
<simonpj at microsoft.com>wrote:
> [Redirecting to GHC users.]
> | Tom Schrijvers wrote:
> | > The cyclic dictionaries approach is a bit fragile. The problem appears
> | > be here that GHC alternates exhaustive phases of constraint reduction
> | > functional dependency improvement. The problem is that in your example
> | > need both for detecting a cycle.
> 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.
Satish R. Thatte: Semantics of Type Classes Revisited
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
Recursive dictionaries are formalized here
Martin Sulzmann: Extracting programs from type class proofs
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.
> 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  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" .
> 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.
> | It seems we can convince GHC to do constraint reduction and
> | improvement in the order we desire. The key is to use the
> | continuation-passing style -- which forces things to happen in the
> | right order, both at the run-time and at the compile time.
> 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.
>  http://research.microsoft.com/~simonpj/papers/assoc-types/index.htm<http://research.microsoft.com/%7Esimonpj/papers/assoc-types/index.htm>
>  http://research.microsoft.com/~simonpj/papers/gadt<http://research.microsoft.com/%7Esimonpj/papers/gadt>
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Glasgow-haskell-users