[Haskell-cafe] Re: Type-level arithmetic

[Steve Schafer]

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/