[Haskell-cafe] Re: Type-level arithmetic

[Tim Chevalier]

On 10/12/07, Steve Schafer <steve at fenestra.com> wrote:
> On Fri, 12 Oct 2007 18:24:38 +0100, you wrote:
>
> >I was actually thinking more along the lines of a programming language
> >where you can just write
> >
> >  head :: (n > 1) => List n x -> x
> >
> >  tail :: List n x -> List (n-1) x
> >
> >  (++) :: List n x -> List m x -> List (n+m) x
> >
> >and so forth.
>
> How, then, is that any different from a general-purpose programming
> language?

It's different because the property that (for example) head requires a
nonempty list is checked at compile time instead of run time.

> You're just drawing the "line in the sand" in a different
> place. You end up with a programming system where compilation is a "side
> effect" of executing the "real" program.
>

I'm not sure exactly what you mean by that, but a lot of people are
spending time thinking about ways for programmers to express more of
their knowledge about programs in a way that's accessible to and
checkable by compilers and other automated tools, and while you might
see it as "just drawing the line in the sand in a different place",
you could say the same thing about programming in a language with a
Haskell-like type system instead of a Lisp-like type system.

Cheers,
Tim

-- 
Tim Chevalier * catamorphism.org * Often in error, never in doubt
"Yeah. Okay. Yeah. Basically, swingers meet ISO 9000." -- DF, on cuddle parties