Are Common Lisp's type annotations for consistency checking or just to improve performance? Haskell and ML have types, Pascal and C also have types, but they serve very different purposes.
And types can also help you prototype and then polish rough ideas. For example, I'm exploring a programming style where no unreachable code paths are allowed: in a circumstance where you'd throw an exception or return an error sentinel, I'd refactor the code to eliminate the unreachable branch. This means that abstractions must have the “right shape” (that is, not leak), and types are fundamental to make this work.
When I start adding type annotations, I'm usually aiming for a speed-up but more often it leads to reorganization and rationalization of the code. The code becomes more streamlined and beautiful.
The post below resonates with me. He calls it 'programming by teaching', where you gradually shape a program to solve your problem. I think of it as 'programming by learning', where the Lisp way of developing helps me learn about my problem. It's only when you have the final version of your code that you fully understand the problem by seeing its solution in front of you.
What I do can also be called “programming by learning”, but it has a fundamentally different flavor than what Lispers do. I present my ideas to the Poly/ML REPL as a hopefully coherent argument, and it tells me whether, at the very least, the argument is internally consistent. ML doesn't “know” about my specific problem domain, but it does know logic, and it's very good at nit-picking, which makes up for my human inability to exhaustively pay attention to an ever-growing number of tricky details. Furthermore, ML has all of nominal, structural and abstract types, which lets me “steer the reasoning” in the desired direction:
(0) Nominal types correspond to primitive domain entities.
(1) Structural types correspond to compound entities, built from simpler ones.
(2) Abstract types regulate the interaction between different subdomains of a larger domain.
The net result is that the REPL's feedback helps me identify those parts of the problem domain where my understanding is weak. Not only the REPL's feedback, of course. For instance, if my program contains unreachable code paths, it means that I haven't yet found the right abstractions.
The philosophy behind this methodology is that:
(0) The cost of having a wrong program is actually larger than that of having no program, because it takes too much effort to identify the wrong parts so that one can fix them.
(1) When the size a program exceeds a certain threshold, it becomes impossible for ordinary human reasoning to determine with full certainty that a program contains no errors. Only formal logic can help, and only machines can do formal logic at a large scale.
(2) It isn't practical to tackle large problems without a properly enforced separation of concerns.
---
By the way, ironically, I never make an explicit type annotation, except perhaps, perhaaaps, at module boundaries. Figuring out the boring details of how to connect the pieces of a puzzle is a job for computers (type inference), not humans.
And types can also help you prototype and then polish rough ideas. For example, I'm exploring a programming style where no unreachable code paths are allowed: in a circumstance where you'd throw an exception or return an error sentinel, I'd refactor the code to eliminate the unreachable branch. This means that abstractions must have the “right shape” (that is, not leak), and types are fundamental to make this work.