Type Classes in Idris

My goal for Idris is to make it a practical dependently typed programming language – suitable for general purpose, systems programming, with precise types when you need them for increasing confidence in correctness of your program. One thing that a modern, practical language really needs, however, is a sane, safe, general way of overloading functions. Haskell‘s solution to this, type classes, is by far the neatest I’ve seen, so in the new implementation of Idris, that’s what I’ve done. They work much as you’d expect if you’re used to Haskell. For example, the Show class could look a bit like this:

class Show a where {
    show : a -> String;

This generates a function show : Show a => a -> String, i.e. a function which will display any a under the constraint that a is an instance of Show. We can declare instances…

instance Show Nat where {
    show O = "O";
    show (S k) = "s" ++ show k;

…and instances can themselves have constraints (and, indeed, be instances for dependent types):

instance Show a => Show (Vect a n) where {
    show xs = "[" ++ show' xs ++ "]" where {
        show' : Show a => Vect a n -> String;
        show' VNil = "";
        show' (x :: VNil) = show x;
        show' (x :: xs) = show x ++ ", " ++ show' xs;

As you’d expect, classes can have constraints too:

class Monad (m : Set -> Set) where {
    return : a -> m a;
    (>>=)  : m a -> (a -> m b) -> m b;

class Monad m => MonadPlus (m : Set -> Set) where {
    mplus : m a -> m a -> m a;
    mzero : m a;

Note that, in this case, we have to give an explicit kind for the parameter m. If you don’t give this, Idris will assume that the parameter is of kind Set.

The prelude and builtins modules now have a couple of the more obviously useful type classes. However, I’m not going to rush into extending this – we should probably think carefully about what classes we need and how they relate to each other, rather than do things “just because Haskell did it that way”!

How it works

Type classes classify types according to which operations can be overloaded for them. Internally, therefore, we can represent type classes as a record of functions. For example, for show:

data Show : Set -> Set where
    instanceShow : (show : a -> String) -> Show a;

show : Show a -> a -> String;
show (instanceShow s) x = s x;

An instance for a type a is then a value of type Show a; for example for Nat:

showNat : Show Nat;
showNat = instanceShow show' where {
    show' O = "O";
    show' (S k) = "s" ++ show' k;

All the elaborator has to do on seeing a class declaration is to generate the appropriate data type, and on seeing an instance declaration generate the appropriate instance function.

Class constraints are a special kind of implicit argument (much like Agda’s instance arguments). On seeing a function call show x, the elaborator will attempt to resolve the implicit argument first by looking in the local context, then attempting to refine by any global class instances which match, recursively.

Still to do…

Default definitions of class methods will be very useful, as will a deriving mechanism. The former is easy, and so likely to happen soon. The latter is hard, and so isn’t.

Note also that this mechanism is intended entirely for a safe general overloading mechanism, and many of the type class tricks which are possible in Haskell are unlikely to work (though, at least, Idris classes can have more than one parameter). Such tricks, I believe, ought to be unnecessary anyway since the dependent type system is very flexible. It will, however, be interesting to see what can be done that I haven’t thought of…

Posted November 9, 2011 by edwinb in Dependent Types, Idris

%d bloggers like this: