Luke's half-complete notion of type-classes for Perl, called "theories":

=======================================================

First run, describing the problem, and then abandoning.

=head1 TITLE

Model Theory - models and theories generalizing classes and roles

=head1 DESCRIPTION

An important problem in programming languages is the expressibility of
B<union types> and B<visitors>.  Together, it is possible to express an
abstract tree in language constructs and process it neatly.  Usually,
such an abstract tree has a data representation (a set of node types)
and a set of processors that act on those node types.  Few modern
languages struggle with these.

However, most modern languages begin to break down when you want to
I<extend> the abstract representation.  Functional languages tend to be
good at adding new processors, whereas object-oriented languages tend to
be good at adding new node types.  However, when you wish to add a new
node type in a functional language, all your processors must be updated.
When you wish to add a new processor in a procedural language, all your
node implementations must be updated.  We would like to be able to
extend either of these in a code-local and type-safe way.

There is a solution in the language Scala[1].  It collects the data
types and the processors together in a parent trait (role), where it can
store an abstract type (virtual type) that is consistent with all the
data types and processors therein.  Then to extend either the data or
the processors, you extend the I<entire system>, all the while making
sure it is consistent.  This solves the problem in the sort of way that,
instead of adding a convenience feature or relaxation, forces you to
think clearly about the problem.

Taken from [1] (with comments added):

    // The base system
    trait Base {
        type exp <: Exp; // An abstract type representing the type of a
                         // tree node.
        trait Exp {
            def eval: int;
        }
        class Num(v: int) extends Exp {
            val value = v;
            def eval = value;
        }
    }

    // Extend the system to incorporate a new node type
    trait BasePlus extends Base {
        class Plus(l: exp, r: exp) extends Exp {
            val left = l;  val right = r;
            def eval = left.eval + right.eval;
        }
    }

    // Extend the original system to incorporate a new processor
    trait Show extends Base {
        type exp <: Exp;    // redefine what it means to be a node
        trait Exp extends super.Exp {
            def show: String;
        }
        // define Num in the new system so so that it can support show
        class Num(v: int) extends super.Num(v) with Exp {
            def show = value.toString();
        }
    }

The details aren't important.  The general technique is what is
interesting here.  We extend the whole algebra -- the whole B<model> --
at once, including the base type of nodes.  Other than that, the
techniques are standard object-oriented visitor techniques.  ([1] also
shows a dual technique to the one above, functional decomposition, which
allows us to define visitors without extending C<exp>, but defining new
node types requires extending C<exp>).

However, a problem shows its head when we have a processor that returns
nodes.  Consider an extension to the C<BasePlus> system above, whereby
we add a transform that doubles every C<Num> node.

    trait DblePlus extends BasePlus {
        type exp <: Exp;
        trait Exp extends super.Exp {
            def dble: exp;
        }
        def Num(v: int): exp;         // XXX factory constructors
        def Plus(l: exp, r: exp): exp;
        class Num(v: int) extends super.Num(v) with Exp {
            def dble = Num(v * 2);
        }
        class Plus(l: exp, r: exp) extends super.Num(v) with Exp {
            def dble = Plus(left.dble, right.dble);
        }
    }

We cannot explicitly construct new nodes inside the body of the new
C<dble> function because C<Num> is a subtype of C<Base.Exp>, not of
C<DblePlus.Exp> (which is what C<exp> is in this system).  You may think
that this is just a fault of the type checker and that we can relax this
away, but in fact there is a fundamental problem in the logic (always
have faith in your type checker):  What is keeping C<Base> from defining
a private subtype of C<Base.Exp> that does not support C<dble> and
returning it, say, as a special private optimization?  

In order to solve this problem, we define abstract factories for each
node type.  This must be done at the final level when the system is
actually used, otherwise such type difficulties arise.  But we don't
want to require anything special at the final level, because then it is
being "locked in" type-wise, and code that follows from that cannot be
extended (it turns into a concretely-typed factory just as in classic,
non-virtual OO type systems).  

There is a way to solve this: to keep a system extensible and type-safe
forever, without requiring a "lock in" stage.  For the rest of this
paper, I will focus on code in (my proposed extension to) Perl 6.

=head2 Union Types

The first piece of machinery we need above the status quo is the B<union
type>.  This is taken from ML-family languages, and is sometimes
referred to as I<tagged types>.  A union type is a closed type, made
up of a set of disjoint B<constructors>.  The concept of a union type is
helpful because if you write a function that handles each constructor,
you are sure you have covered every case in the type.

Here is a union type that defines a tree with C<Num> and C<Plus> as
above:

    data Exp (
        ENum[ Num --> Exp ],
        EPlus[ Exp, Exp --> Exp ],
    );

(Keep in mind that I am not proposing syntax; all that is required is
the concept of a union type, whatever syntax it has.)

You may extend union types to create new types:

    data NegExp extends Exp (
        ENeg[ Num --> Exp ],
    );

There is something going on here that may be a little strange to people
who have seen C<extends> before in a language.  For instance, in Java,
when a class C<B> C<extends> a class C<A>, the C<extends> denotes that
the I<behavior> is extended, and therefore that C<B> is a subset of
C<A>.  Here, however, the C<extends> denotes that the I<set> is
extended, and therefore C<Exp> is a subset of C<NegExp>.  That is, when
you extend a union type, you make it bigger, more general.  Anywhere a
C<NegExp> can be used, an C<Exp> can be used.

I'll also adopt a syntax for unifying against union type constructors:

    multi run (Exp --> Num) {...}
    multi run (ENum[$num]) { $num }
    multi run (EPlus[$left, $right]) { run($left) + run($right) }


=head1 REFERENCES

[1] http://icwww.epfl.ch/publications/documents/IC_TECH_REPORT_200433.pdf

=======================================================

Larry currently thinks that matching against data constructors will look
something like this:

    multi run (ENum ($num)) { $num }
    multi run (EPlus ($left, $right)) { run($left) + run($right) }

Where you can also have Haskell-like node@... syntax with:

    multi run (ENum $node ($num)) { $num }

Who knows how he thinks we will declare data constructors...

=======================================================

Second run, a brain-dump to the design team.

A theory is a generalization of a role.  If you think of a role as a
contract that says "if you implement these methods for me, I'll
implement these methods for you"  (where either of the "these methods"
can be empty).  Correspondingly, a theory is a contract that says "if
you implement these multis for me, I'll implement these multis for
you".  That's the first level view, i.e., what we put in the intro
docs.  More abstractly, a role specifies an interface while a theory
specifies an algebra.

In order to solve the expression problem, "trait Base" in the Scala
paper becomes "theory Base".  In it we put the abstract specification
of the data structure and the visitors.  Let's try it out with a
simple expression grammar (which doesn't look all that different from
PIL):

   theory Base {
       data Exp[::t] = (
           Zero[           --> Exp[Int]],
           Pred[Exp[Int]   --> Exp[Int]],   # n + 1
           Succ[Exp[Int]   --> Exp[Int]],   # n - 1
           IsZero[Exp[Int] --> Exp[Bool]],
           Cond[Exp[Bool], Exp[::t], Exp[::t] --> Exp[::t]],
       );

       sub run (Exp[::t] --> ::t) {...}
       # that was trying to specify a general type signature for the
       # set of multis
       multi run (Zero[])     { 0 }
       multi run (Pred[$x])   { run($x) - 1 }
       multi run (Succ[$x])   { run($x) + 1 }
       multi run (IsZero[$x]) {
           run($x) == 0 ?? Bool::True !! Bool::False;
       }
       multi run (Cond[$cond, $true, $false]) {
           if run($cond) {
               run($true);
           }
           else {
               run($false);
           }
       }
   }

Mmm, the runtime of language right there :-)

Now let's add a node:

   theory BaseWithNot extends Base {
       data Exp[::t] extends Base::Exp[::t] (
           Not[Exp[Bool] --> Exp[Bool]],
       );

Now if we leave it at that, it's okay.  But you can't put a
BaseWithNot::Exp into run, because when you extend a union type, you
make it bigger.  Base::Exp is a subtype of BaseWithNot::Exp.  So we
have to specify a new type for run():

       sub run(Exp[::t] --> ::t) {...}

I'm not sure if the old run()s will automatically kick in, or if you
need something like:

       multi run(Base::Exp[::t] $exp) { Base::run($exp) }

If you do specify that, then there's really no difference (yet, see
below) between a theory and a module.  But maybe that "extends Base"
does something for you.

But after we added that new type signature, it won't compile (if we
have strict types on), since we forgot to implement the Not case:

       multi run(Not[$x]) { !run($x) }
   }

It should be pretty obvious how you add a visitor.  Extend the theory
and then add the visitor.  Let's say we did that with a theory called
BaseWithConstantFolding (deal with the names; they'd probably be
shorter in practice, because things would be namespaced about and
whatnot).  Then we can combine the two theories:

   theory BaseWithNotCF extends BaseWithConstantFolding
                        extends BaseWithNot
   {

Again, this is okay, but it shouldn't typecheck if you try to
constant_fold an Exp from this theory, because constant_fold was
defined in terms of the data defined in Base.  So we need to implement
the constant folding case for not.  Let's just have it do nothing:

       sub constant_fold(Exp[::t] --> Exp[::t]) {...}
       multi constant_fold(Not[$x]) { Not[constant_fold($x)] }
   }

Note that, unlike in the Scala paper, we can return new nodes without
needing to define factories.  That's because in the Scala paper, they
were creating new *subtypes* (meaning subclasses, not necessarily
constrained types) of the original exp, whereas we are making
*supertypes*.  This is why I think the union type model fits this kind
of problem a lot better than the base class/subclass model.

Up until now, a theory seems like a glorified module.  That's because
it had zero parameters; that is, it had already been instantiated
right when we created it.  Maybe in that sense it should have been a
model.  And maybe a model is just a module anyway.  Uh, see below.

Theories really get cool when you start parameterizing them.  Here's a
theory that specifies a group:

   theory Ord[::T] {   # T is ordered
       # required methods
       multi infix:{'<='} (T, T --> Bool) {...}
       # provided methods
       multi infix:<==> (T $x, T $y --> Bool) { $x <= $y && $y <= $x }
       multi infix:<!=> (T $x, T $y --> Bool) { not $x == $y }
       multi infix:{'>'} (T $x, T $y --> Bool) { not $x <= $y }
       ...
   }

Then to say that Int is ordered, you "model" the theory (this vocab is
incidentally from model theory :-) :

   model Ord[Int] {
       multi infix:{'<='} (Int $x, Int $y --> Bool) {
           # uh, well... builtin
       }
   }  # a whole bunch of useful multis are now defined for you

This shows a nice feature of theories already.  All that operator
magic that Perl 5 done now gets put into theories, and you get it if
you ask for it.  That is, the presence of a < operator no longer
implies that you're ordered (for instance, IO::All wasn't ordered, but
it used <).  Saying that you're ordered by modeling the theory also
implies that you obey the laws that this theory represents.  For
instance, Junction couldn't model Ord (well it could if it wanted to,
because Perl can't check that kind of thing, but it shouldn't).

Then to write a function that only accepts types in a certain theory,
you use a constraint.  Since we have | available in signatures now,
I'll use that (but I'm not attached to it by any means):

   sub min(::T *@values --> ::T | Ord[::T]) {
       die "Null list given to min()" unless @values;
       my $min = @values[0];
       for @values[1...] {
           $min = $_ if $_ < $min;
       }
       return $min;
   }

The reason it's specified with a constraint instead of just saying
"Ord *@values", is because theories can have more than one parameter,
specifying an algebra over multiple types.  For instance, you might
define a vector space over a field, and then both the vector type and
the field would be parameters to that theory.  However, I'm sure "Ord
$foo" could be shorthand for "::T $foo | Ord[::T]" for
single-parameter theories.  Incidentally, single-parameter theories
are just roles. :-)

=======================================================

That last statement wasn't quite true.  Consider the theory Num, which
is single-parameter.  This theory mandates that if you add two As
together, and A is a Num, then you get back another A (closure under
addition).  Clearly Int is a Num.  However, the subtype Int where { $_ <
10 } is not, since 8+8 == 16, and 16 isn't in that type.

However, if you have a type that does a role, you want every subtype
also to do that role (of course, my parent supplies these methods so I
do too).  That is, roles are more like interfaces than algebras.  So in
Theory theory, the formal definition of a role is:

    A theory R is a role if: for all types T and U, U is an instance of
    R and T does U implies that T is an instance of R.

Programmatically, this I<usually> means that all operations in the
theory depend covariantly on the type.  That is, you can't specify that
a method returns the parameter type of the theory, only that the methods
accept the type as a parameter.