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, ::Field], and just about every other abstraction that you start with a capital letter in OO design.
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.
