=head1 TITLE

Perl 6 Type Metatheory

=head1 SYNOPSIS

Perl 6 has no single, canonical, static type system.

=head1 DESCRIPTION

My research into type systems and type inference has shown me that there
are systems with many desirable properties, and some of those properties
are mutually exclusive.  For example, the F(<:) system has most of the
expressive power that Perl 6 would need, but it is not inferrable.  The
Hindley-Milner system and the Colored F(<:) are inferrable, but the
former lacks subtyping and the latter lacks bounded quantification.

People are going to want to do all sorts of things with types.  They're
going to want certain well-typed programs to fail intentionally, for
example:

    my $width = get_width;
    my $height = 1 + get_height;
    say ($width + $height);

Where $width and $height are just integers, with the property that they
are incompatible with each other.  This is not a type system that a
reasonable type calculus would allow (because you can convert to an
integer and then to the other type to get around it), but like hungarian
notation, it catches stupid logic errors.

People are also going to want very rich static systems: ones that will
let you type vectors and disallow adding of vectors of different sizes.
This either requires the construction of Peano numerals within a
complete type system (a royal pain) or a simple theory of dependent
types.

But the moral of the story is, this is one of those places where we
cannot have our cake and eat it too.  Once the type system becomes too
rich, its inference (and even its well-typedness, for a larger bound)
becomes undecidable.

Here is my proposed solution:  Perl 6 is untyped, but provides hooks to
attach most any sort of type system implemented directly in Perl.  This
sweeps the problem under somebody else's rug.  Most notably, though, it
sweeps it under CPAN's rug, if CPAN wants it.  

We should take a lesson from Perl 5's bless semantics here.  Bless was
so orthogonal, so simple, and yet so powerful, that many authors built
strange, experimental object systems on top of it.  When Perl 5 came
out, the notions of classless systems, inside-out objects, even plain
delegation were hardly mainstream.  But Perl 5 provided the hooks so
that they could be built anyway.

We should take another lesson from Perl 5's bless semantics here.  Even
though there were many very cool object systems on the CPAN, nobody used
them.  Any programmer who has written Perl 5 OO code has this pattern
memorized:

    sub new {
        my $class = shift;
        bless { ... } => ref $class || $class;
    }

And everyone whines about it when they are learning, and even after they
have been doing it for years, although there exist better alternatives.

So I propose that there should be no minimal default!  Perl 6 in the
absence of pragmata is statically untyped.  If there is a standard
"static typing" pragma, it should begin with a capital letter, so that
it doesn't feel any more "blessed" than any other, and we encourage
people to experiment.

But in order to proceed, we must define something.  In fact, one of the
hinges of Perl 6 seems to be lost at sea without a type system:
multimethods.  The other things that need defining are:  the hook
system, which is going to be closely related to the fundamental
metamodel concepts; and the way in which two modules using different
static calculi interact with each other.

=head2 Notes

I plan to propose a runtime-only multimethod system (which is statically
hookable like the rest of the language).  This implies that invocants to
multimethods I<must> be strict.  This is no longer allowed:

    proto infix:<||> ($cond, $otherwise is lazy) {...}

For we have to know the type of $otherwise to dispatch correctly, but
we're not supposed to execute it yet.  Therefore it may not be an
invocant   (another way of saying this is that the core language does
not depend on any inference capability, since the core language has no
idea what a type is).

=head1 AUTHORS

Luke Palmer <lrpalmer gmail com>