> On 27-Jul-2000, Claus Reinke <[EMAIL PROTECTED]> wrote:
> > Does anyone else agree that Haskell's type classes are a logic
> > programming language in disguise, and that this interpretation makes
> > it easier to understand what is going on?
>
> Yes, I find this interpretation useful.
>
> Here's some other example of correspondance between type systems
> and logic programs:
>
> - existentially quantified types and type class constraints
> on functions (as supported by Mercury, although not yet
> by any Haskell implementation) are the type-system analogy
> of output modes
>
> - the recent Hugs extensions to support functional dependencies
> in type classes can be seen as similar to the mode/determinism
> declarations in Mercury (or similar features in other logic
> languages such as PDC Prolog and TEL).
>
> Actually the view of type checking/inference as constraint
> solving is a very general one that encompasses a lot of type systems,
> not just Haskell's. So I think generalizing just a little further
> to thinking about it as constraint programming (rather than just
> logic programming) helps too. For example, in type systems with
> subtypes, the type checker needs to solve subtype constraints
> as well as unification constraints.
>
> I think you explained it very clearly. But the first person to
> explain this correspondence to me was Peter Stuckey <[EMAIL PROTECTED]>.
> A few (about five?) years ago, I read a draft of a paper he was
> writing on using constraints for type inference to give you ad-hoc
> overloading, Haskell-style type classes, etc. I think this draft
> was eventually published as the following paper:
>
> * B. Demoen, M. Garcia de la Banda, and P.J. Stuckey. Type
> constraint solving for parametric and ad-hoc polymorphism. In
> J. Edwards, editor, Proceedings of the 22nd Australian
> Computer Science Conference, pages 217--228.
> Springer-Verlag, January 1999.
>
> > the restrictions we use to ensure determinism and termination are
> > mostly brute force approximations
The paper that Fergus mentions does give a constraint solving perspective
on type inference/checking. It doesnt mention type classes though.
See http://arXiv.org/abs/cs.PL/0006034
for a recent workshop paper on type classes and constraint solving
Peter
