I'm feeling conflicted about theory.pod. While I'm very proud of it for being a great object model and giving precise semantics to things we've been handwaving over for ages, it just isn't Perl. It's too formal and static for Perl; you can't talk it into checking something a different way.
However, it is not possible to add a pure hook system that's reasonable for the everyday user to use. Type inference can't deal with arbitrary code, because it needs to go forwards and backwards and sideways through the annotations to figure things out, whereas arbitrary code can only go forwards. If we had a logic subsystem, we could give them arbitrary code (within that subsystem) because logic programming has the nice property that you can execute a function backwards:
:- append(X, Y, [1,2,3,4,5]).
I wonder if you mean "too formal" as "requiring too much explicit annotation from the user", as in forcing people to think about it too much. If so, maybe it needs yet more ergonomic engineering, also known as sugar...
Re:"Too formal and rigid for Perl"
luqui on 2005-10-12T08:12:07
The "too formal" comment came from talking with Stevan about the metamodel and remembering Smalltalk. But "formal" was the wrong word[1]. However, I'm convincing myself that theory.pod is a level above the "bless" semantics that we know and love, and can in fact cooperate nicely with it. theory.pod defines a type system, not an object system.
See my reply to Ovids comment for a more rambly version of this answer.
[1] Certainly. The whole reason I study mathematics is because of its incredible ability to squash ambiguous or incomplete thought, and that's all due to its formal treatment. Whenever I describe a problem to my mathematical side, I redefine and redefine my terms until I am in precise, unambiguous mathematical language. And many times, once I state the problem that way, the solution becomes obvious. This is the beauty of formalism.
If we had a logic subsystem, we could give them arbitrary code (within that subsystem) because logic programming has the nice property that you can execute a function backwards.
Not knowing exactly what you're trying to accomplish, the following off the cuff statement could be totally meaningless.
Passing arbitrary code to a logic subsystem does not necessarily mean that you can still run the function backwards. You would have to have some way of noting side-effects (it's difficult to "unwrite" a file or unread database tuples) and math in logic programming is frequently a "one-way" affair unless constraints are specified.
Unless, of course, you're talking about passing purely logical code to something else
Re:Arbitrary code in logic subsystems
luqui on 2005-10-12T08:02:29
> Passing arbitrary code to a logic subsystem does
> not necessarily mean that you can still run the
> function backwards. You would have to have some
> way of noting side-effects (it's difficult to
> "unwrite" a file or unread database tuples) and
> math in logic programming is frequently a
> "one-way" affair unless constraints are specified.
Oh, of course. I'm just saying that, as cool as theory theory is, making it the One True model is a bit presumptuous for Perl. I feel that the research that CPAN has done has been incredibly important (note all modules in the Class:: namespace), and the reason that that research can take place is because of the extremely simple and basic "bless" object-orientation.
Of course, all that stuff can carry over to Perl 6, because at it's very very core, its object-orientation is also just "bless". However, I think that it's important to let such research go on with type annotations as well; let a module writer really screw with what it means when you say "my Int $x".
The example that got me was when I set out (and failed) to implement compile-time physical unit checking in Haskell as I had done in C++. Turns out that I had to implement Peano naturals in order to do it. I don't want Perl to work that way. It should be possible to embed our regular numbers "under the covers" of the theory theory; not have to construct them in the language of the type system.
So I was just pondering a way that you could go about extending a type-inferencing compiler. If you gave your extension in the language of logic programming, then it should be possible. Still, completely arbitrary code would have to be hidden under the covers of the logic paradigm, which we both know how to do:-)