Steve said:
How, then, is that any different from a general-purpose programming language? You're just drawing the "line in the sand" in a different place.
In a way it is like drawing a line in sand. But that's a useful thing to do for a bunch of reasons. (1) When developing code, you'd like to test as much of the code as possible for reliability. But you don't necessarily know what data your code is going to run on in the future. It'd be cool if you could somehow run as much of your code as possible even without yet having the data. By having a declaration like
(++) :: List n x -> List m x -> List (n+m) x
it's almost as if the compiler gets to run a 'reduced' version of your application. You don't actually know what the elements of the list are (or even their types), and yet you can still test to see if your code handles the lists of the lengths correctly. (2) Sometimes you want to solve a problem incrementally. It's often helpful to reason first to the type we want, and then the implementation, rather than just to the implementation - it gives a way to factor the problem into two stages. By allowing some computation to take place at compile time you can be flexible about where the boundaries between your stages lie allowing you much more freedom in how you incrementally arrive at your solution. (3) In theory you can get very efficient code out of a type system where the compiler knows, for example, how long the lists are in advance. I guess you could say it's a form of partial evaluation. -- Dan