No monotypes

Perl 6 has a very rich type system, even though it’s not done. As far as my knowledge goes (which in this area is not very far compared to some of the lambdacamels), it makes the fewest assumptions and restrictions of any type system of any other language. I’ll be writing today about a statement that seems obvious, but has some very interesting consequences (much like “the speed of light is constant in all reference frames”). That statement is “types are just sets”.

I used that statement when arguing with Damian about multimethod semantics. The argument was against derivation metrics, in how it is possible to measure with a finite number how much one infinite set differs from another (assuming that they both have the same infinite cardinality). However, in my argument, I was claiming that types have nothing special over sets, otherwise they might have some information in them that allows you to measure distance. So, let’s look at what that means.

For one, you can no longer talk about the “type of” a certain value. When you ask that question, you’re asking “what set does this value belong to?”. And of course there are infinitely many of them. So the best you can do is ask “does this value belong to this set?”1.

(For the following example, assume that Perl 6 is pure-functional: that is, no side-effects allowed. We’ll incorporate those later.)

Consider this function:

    sub foo (::T --> ::T) {...}

In Perl 6, that means that foo is a function that takes a value of type T and returns a value of type T, for any type T. Let’s look inside that definition more mathematically: for every set T, x ∈ T ⇒ foo(x) ∈ T. You might as well not write the body of the function, for the only function that this could possibly be is the identity! (Note that the only function in Haskell with this signature is, in fact, id.)

If we are to write expressive type signatures, it’s pretty clear that we need to steal Haskell’s type classes. A type class is just a set of types, or a set of sets. It itself is a type. For instance, Numeric could be a type class that says that its member types obey closure under addition, multiplication, etc., along with things that Perl can’t prove, like associativity under addition and multiplication. This is why you have to declare type class instances. Then we can declare (pseudosyntax):

    sub double (::T --> ::T | ::T (in) Numeric) {...}

And have it mean something other than the identity. It probably adds the argument to itself and returns it. Since ::T obeys the laws of Numeric you’re allowed to add it to itself and get the same thing back.

How do we define such type classes, then? How about like this:

    role Numeric ::T {
        multi infix:<+> (::T, ::T --> ::T) {...}

(Incidentally, that implies that you might define normal classes like so:

    class Dog $fido {
        method bark () { say "$ says 'woof'" }
        method name () { "Fido" }

Which is an interesting, er, “solution” to the $self problem.)

And of course, this implies that you can probably have type-class classes, whatever those are.

1You might think about asking “what is the smallest set that this value belongs to?”, but then you’d quickly realize that the answer you’d get would be the singleton set of that value :-).


Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s