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
...
> 1. Invoking the class mechanism to resolve a type constraint
> will never instantiate variables in the original qualified type.
> The mechanism will try to find instance declarations whose
> head *matches* the constraints in the qualified type (which
> may lead to new constraints, etc..), so the substitutions will
> be one-way only (giving up one of the advantages of logic
> programming..).
Hmm, the Mercury type class system has the same restriction. A
couple of people have suggested that we allow two-way binding in such
situations, but I've never found the argument very compelling;
however, your description does make this argument more convincing.
One potential difficulty here, I think, is that if there are multiple
matching instance declarations, this would lead to nondeterminism, and
if you're not careful, this can lead to exponential performance in the
type checker. And I think there would be problems ensuring termination.
> 2. As you noticed, there is no way to get the equivalent of
> Prolog's closed-world assumption - we can't tell the class
> mechanism that the instances currently in sight are all the
> instances that will ever be available.
One of the ways that I would like to extend Mercury in the future is
with support for dynamic type class constraint checks -- similar to
checked downcasts in OO languages. But this relies on a closed-world
assumption. In order to make this possible, even in the presence of
features like dynamic loading, we impose some restrictions on type
class instance declarations: the type in a (single-parameter) type
class instance declaration must contain exactly one type constructor,
i.e. it must be either a type with no arguments, or a polymorphic
type constructor whose arguments are all type variables. (For example
`int', `list(T)' and `bintree(K,V)' are allowed, but `T' and
`list(int)' are not.) With this restriction, and since we don't allow
overlapping instance declarations, we know that there will be at most
one instance declaration for each type constructor. This gives us
a closed world property for each given type constructor,
while still remaining open to extension for new type constructors.
However, the type checker does not exploit this closed world property.
> So your example can be reduced further:
>
> ----------------------------------
> module Class where
>
> class C t
> instance C Double
>
> f :: C a => a
> f = 1
>
> g :: C Int => Int
> g = 2
> ----------------------------------
>
> Even if we intend never to create any other instances of C, we can't
> express this intention, so instead of a type error complaining about a
> wrong type in g's signature, we'll get a complaint about a missing
> instance. And even if we could express our intention, f's type would
> still not be instantiated to match the only instance of C [Hugs says
> "cannot justify constraints" when trying to load f, and "unresolved
> overloading" when I try to use g after commenting out f; what do
> batch-compilers say, and do they change messages when we rename
> the module to Main and include some definition of main?].
I translated this example to Mercury:
:- module example.
:- interface.
:- typeclass c(T) where [].
:- instance c(float) where [].
:- func f = A <= c(A).
:- func g = int <= c(int).
:- implementation.
f = 1.
g = 2.
The current Mercury compiler (like Haskell 98) does not support
constraints of the form `c(int)'; it reports a "sorry, not implemented"
error for the type declaration for `g'.
If you comment out the declaration and clause for `g', then
the Mercury compiler reports
example.m:013: In clause for function `example:f/0':
example.m:013: in function result term of clause head:
example.m:013: type error in unification of variable `HeadVar__1'
example.m:013: and constant `1'.
example.m:013: variable `HeadVar__1' has type `A',
example.m:013: constant `1' has type `int'.
Note that even if you remove the type class constraint, `f' still has
a type error. That's why the error message doesn't mention type class
constraints. This error message could be improved, by explaining why
it is that the type variable `A' can't be bound. The reason is that
`A' is universally quantified.
If you use an existential quantifier,
:- some [A] func f = A => c(A).
then you get a different error message, more like the one that I think
you were expecting:
example2.m:013: In clause for function `example2:f/0':
example2.m:013: unsatisfiable typeclass constraint(s):
example2.m:013: `example2:c(int)'.
> > What I can't tell the compiler is "there will not be any other instances
> > FA [foo] [bar], so if you need one, you may assume that foo == bar".
>
> Both seem reasonable from a logic-programming perspective, as well
> as a few other modifications, but with the current lack of control over
> the scope of instance declarations, it is hard to define "these" in "these
> are the only instances of class C".
If a type class is not exported from a module, then only that
module can contain instances of that type class. So the type
checker could perhaps handle that case specially. On the other
hand, it would be problematic if simply exporting some previously
private entity could change whether the module is type-correct.
--
Fergus Henderson <[EMAIL PROTECTED]> | "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh> | of excellence is a lethal habit"
PGP: finger [EMAIL PROTECTED] | -- the last words of T. S. Garp.
