[Haskell-cafe] Re: Type-level arithmetic

Steve Schafer steve at fenestra.com
Fri Oct 12 17:04:52 EDT 2007

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.

More information about the Haskell-Cafe mailing list