[Haskell] Re: indirectly recursive dictionaries

[Martin Sulzmann]

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
> to
> | > be here that GHC alternates exhaustive phases of constraint reduction
> and
> | > functional dependency improvement. The problem is that in your example
> you
> | > 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
http://portal.acm.org/citation.cfm?id=182459

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.

Recursive dictionaries are formalized here

Martin Sulzmann: Extracting programs from type class proofs
http://portal.acm.org/citation.cfm?id=1140348

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.

-Martin


>
> 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].
>
> 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.
>
> Simon
>
> [1] http://research.microsoft.com/~simonpj/papers/assoc-types/index.htm<http://research.microsoft.com/%7Esimonpj/papers/assoc-types/index.htm>
> [2] 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
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20090319/1f29e4ba/attachment.htm