On 10/12/07, Steve Schafer <[EMAIL PROTECTED]> 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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe