[Haskell-cafe] Re: Type-level arithmetic

[Dan Piponi]

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