On Fri, 12 Oct 2007 21:51:46 +0100 (GMT Daylight Time), you wrote:
Which is nevertheless the kind of power you need in order to also be able to prove precise properties.
We're not talking about POWER, we're talking about SYNTAX. That the Instant Insanity problem _was_ solved using Haskell's type system is obviously proof that the power to solve that kind of problem, at least, is already there. However, the solution is convoluted and less than clear at first glance. The question is whether or not there is a way to allow such solutions to be expressed in a more "natural" way. To which my rejoinder is, "To what end?" To extend the _syntax_ of the type system in a way that allows such "natural" expression turns it into yet another programming language. So what have we gained? Steve Schafer Fenestra Technologies Corp. http://www.fenestra.com/