Fergus Henderson:
> 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.
>..
> 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.
>..
> 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.
Meanwhile, I had a look at the paper. For those interested: it is available
from the HAL home page page at:
http://www.csse.monash.edu.au/~mbanda/hal/index.html#publications
Unfortunately, it does not discuss the ideas we were talking about
(type class system as logic programming language). It discusses a
translation of Mercury-style programs with type definitions (`data' in
Haskell) and optional predicate type declarations into a logic program
that is used both for type checking and for type inference (where type
declarations have been omitted). The type system is an extension of
Hindley-Milner with ad-hoc polymorphism (overloading).
As a guess, the expressiveness of the overloading seems to correspond
to Haskell's instance declarations, without type classes or type class
contexts: several variants of a predicate/function can be given with
different, not necessarily related types, and the type of the collection
of definitions is a disjunction of the individual types. These disjunctions
are propagated through the type inference/type checking.
Using Prolog-style meta-programming facilities, it shouldn't be too
difficult to extend the system to handle some form of type classes,
too, and the feature is listed on the project page as "currently
under development".
Nevertheless, I recommend that those interested in type systems
and their implementations have a look at the paper (I'll come back
to it in a minute).
But first, my point was exactly about this missing part, because the
type class instances and type constraints give programmers the
chance to define their own logic program in a language of type
predicates (for the HAL system, this would imply that programmers
could add predicate rules and facts to the generated logic program,
and that these rules, in addition to defining possible proofs of type
predicates, would also need to accumulate programs in the, not
necessarily logic, source language; the latter programs would, in
case of successful proofs, be re-embedded into the source program).
>From the execution of such programmer-defined logic
programs, functional programs are extracted, offering Haskell
programmers a logic-based, type-directed meta-programming
facility. There have been various example applications putting
this scheme to good use, one of the latest is Ralf Hinze's and
Simon Peyton-Jones' integration of generic programming into
type classes (http://research.microsoft.com/~simonpj/#derive).
Unsurprisingly, most of the advanced uses of Haskell's type
classes involve authors who also had to think a lot about type
class semantics and implementation (*). Some two years ago,
on the occasion of joining Mark Jones' group (then in
Nottingham), I used the occasion to take a more detailed look
into type classes and Mark's semantics for them, based on
qualified types (see Mark's PhD thesis, published/hardcopy
only, or his online publications at http://www.cse.ogi.edu/~mpj).
I had the feeling that qualified types were much nicer than
the language features they explained, meaning that (a) it helps
a lot to think about type classes in terms of a user-defined
entailment relation between type predicates, and that (b)
there has to be a better design of a system related to type
classes that would give us a handle to more of the flexibility
of qualified types (most of the type class extensions follow
naturally from variations of the underlying system of qualified
types, often just a change of the entailment relation).
[My conjecture was, and still is, that this design is sitting
burried under the current type class system, just waiting to
be discovered..]
But back to the paper about constraint logic programs for
type checking. There are several points in there that should
be of interest to type system implementers, here are a few:
- generating a logic program corresponds roughly to partial
evaluation of type inference: there is a translator that knows
about the general type system and produces for each source
program a logic program that "specializes" all type-checking
and type-inference tasks for this particular program. This
leaves implementation of standard logic features to those
specializing in logic language implementations and would
allow type system implementers to focus on the type-system-
specific translation - more modular implementation, easier
to experiment with?
- There is no direct performance benefit from reuse of the
translation because typing across modules uses (inferred)
declarations. Surprizingly, though, there seems to be a
performance benefit even for individual runs!?
I can't say how good or bad type inference in Mercury is,
or whether I'm misreading the measurements, but the sum (!)
of times needed for specialization and execution of the
generated logic programs (for type inference) seems to be
consistently lower than the time for direct type inference on
the source programs by the Mercury system (for complete
inference, no declarations; unfortunately, time for i/o is omitted,
which would have been relevant in this case; the paper also
makes some caveats about differences in the type inference
processes, in addition to a funny comment on intended
semantics..).
- The generation of a separate logic program representing
the typing aspects of the source program opens possibities
that are not discussed in the paper: it should be possible to
get almost for free the interactive dialogues about program
types that various authors have proposed for purposes of
type debugging and program comprehension.
Just query the logic program about types, or use standard
logic program debugging techniques (e.g. algorithmic
debugging) to find out how the types of program parts
relate to the type of the whole. I say almost for free because
it would be necessary to generate a (partial) translation,
including as much type information as possible, even for
type-incorrect programs.
Mostly advantages, as it seems. Of course, GHC-users, say,
wouldn't be happy if installing GHC would require a Prolog
executable (in addition to Perl, gmp, cygwin, ....;-), but if this
would help to simplify and speed up the compilation and help
with type debugging, too, perhaps it is the way to go? What
other disadvantages are there to this scheme?
In any case, Fergus and the authors of the constraint logic
typing paper have already confirmed what I had hoped for:
that many of the problems Haskell's type classes are fighting
with (in semantics, design and implementations) have counterparts,
perhaps even solutions, in the logic programming community.
Fergus (and others): how about compiling a summary of the
relationships (a kind of dictionary of terminologies) ? In
particular, what is the state of the art in logic programming
wrt determinism and termination analysis? Can you
recommend any recent surveys, or can anyone offhand
propose "nicer" constraints to ensure termination and
determinism (of executions, not results), compared to
those currently used for type classes?
Claus
(*) Thinking about it, it isn't surprizing that Hugs has always
come with a particular example program (Mini Prolog engines),
by a particular contributor. Just check your Classic Hugs
demos directory for its history!-)
