Okay, here's an update on my current thinking for theory.pod version 2. For those of you who read, understood, and were comfortable with theory.pod version 1, prepare to be surprised. I'm completely turning it on its ear. However, I think there won't be a big acceptance issue, since nobody (including me) understood and was comfortable with version 1.
Version 1 gave Perl a (broken) type system with tagged union types and type classes. The system, had it not been broken, would have been turing-complete, and thus you could do all the fancy stuff you wanted, but you'd have to encode it in the language of the type system. For instance, if you wanted to make a vector class that would only allow you to add vectors of the same length, you could do that, but it would be a major pain to implement Peano naturals to encode numbers in the type system.
But that's so stupid. We have a great language, Perl 6, which knows all about numbers (among other things ;-), and we're forced to recreate them for the type system. The number one goal of version 2 is to get rid of this stupidity, and let you talk about the types of your Perl program in Perl. Here are the features I'm trying to support (in rough order of importance; i.e. rough order of required elegance):
* Type metaprogramming; i.e. talk about types in Perl, not some weird type language
* Roles and Classes with mandatory allomorphism (a property of version 1: types are only interfaces)
* Type classes and parametric polymorphism
* Inferrable
* Tagged unions with allomorphism
* Union types [1]
At the moment, I'm doing a lot of research out of TaPL and ATTaPL. It's hard to get a concrete grasp on what those books are saying sometimes, so I'm going to implement a little syntaxless language (not unlike Blondie) with the hard parts of the above points: in particular, an inferrable, metaprogrammable type system.
Incidentally, I think that an inferrable metaprogrammable system needs a logic engine. Cool. I also think that embedding a logic engine in Perl 6 can be done in a unintrusive and easy-to-implement way, providing (and this is the hard part, but it is already specced) support for hypotheticals.
[1] Which happen to screw over inference algorithms. That's why it's way at the bottom of the list. If it doesn't fit, I'll even consider trying to argue us out of supporting them.
