NOTE: **use Perl;** is on undef hiatus. You can read content, but you can't post it. More info will be forthcoming forthcomingly.

Monday September 19, 2005

06:10 PM

Types and Programming Languages came today! Woohoo!

I've been thinking about Perl 6's Theory theory some more. I think I have a pretty good idea how everything fits together now. If you'd like to catch up, read http://svn.openfoundry.org/pugs/docs/notes/model_theory.

I'll be going pretty fast through the ideas I've already written, so if you're lost, go read it.

A theory is the formal specification of some algebra over zero or more types; from the Perl level, it mandates some methods and provides some methods. Some examples of theories are: Storable[::T], Ord[::T] (a totally ordered set), Num[::T] (a ring), VectorSpace[::Vec,

Two-or-more-parameter theories are cool. But the one-parameter theories are algebraically more interesting; in fact, we have other names that for certain one-parameter theories.

I've always known that a Role is some kind of theory. At first, I thought that all one-parameter theories were roles. But the case of Num convinced me otherwise. You'd expect that if A is a subset of B and B is an instance of Num, that A is also an instance of Num. But Num has this method:

theory Num[::T] {

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

}

That is, if A is a numeric type, that means you can add two A's together and get an A back. So Int int is an instance of Num, but Int where { $_ < 10 } is not, since 6+6 are both in the type, but their result isn't.

I've decided that the transitivity property above is actually what *defines* a role. Formally:

*A theory R is a role if: for all types T and U, if T is an instance of R and U is a subtype of T, then U is an instance of R.*

That is, if a set obeys a role, then every **subset** of that set also obeys the role. So Ord is in fact a role (since the integers are ordered, every subset of the integers is ordered). Also, all traditional classes are roles, in that they only depend covariantly on one type (the invocant). Most roles are roles because they only depend on the parameter type covariantly (they only take the type as an argument; never return it).

There is a dual notion to the role, and that is the factory. It is so named because most factories are factories because they only depend on the parameter type contravariantly (they only return the type; never take it as a parameter). You can guess the formal definition of a factory:

*A theory F is a factory if: for all types T and U, if T is an instance of F and T is a subtype of U, then U is an instance of F.*

That is, if a set obeys a factory, then every **superset** of that set also obeys the factory. And this is quite a beautiful result, as it ties the C++-derived and pure functional OO worlds together. From C++-derived OO languages, all types (classes) are roles; they are polymorphic only covariantly. From pure functional languages, all types (data constructors) are factories; they are polymorphic only contravariantly.

Last of all, a zero-parameter theory is a module. And a class is pretty much another name for a module.

More on the practical side later. That was the cool theoretical stuff though. Happy hacking.

Stories, comments, journals, and other submissions on use Perl; are Copyright 1998-2006, their respective owners.

The Fine Print:The following comments are owned by whoever posted them. We are not responsible for them in any way.## Role & Factory >>(in) Theory[T]; Module eqv Theory 0 Comments More | Login | Reply /

Loading... please wait.