a Mr. Fleming wishes to study bugs in smelly cheese; a Polish woman wishes to sift through tons of Central African ore to find minute quantities of a substance she says will glow in the dark; a Mr. Kepler wants to hear the songs the planets sing.

Tuesday, March 20, 2012

Optimization is just a side benefit.

A corrolary to our previous definition of type systems as principally ways to prove correctness: many discussions programmers have about type systems seem to focus on the runtime cost of type checking, as if that were the primary issue. Common Lisp has a great answer to that in its optional type declaration system¹ and the powerful inference and inlining done by compilers such as CMU Python.²

To a typeful programmer, runtime optimizations are an interesting side-effect of types, but ultimately beside the point. The correctness-proving features have a much greater impact on how you think about data structure, algorithm, and API design, approaches to testing, etc.

Common Lisp's type declarations are very nice, but they are little help in broadly proving program correctness, which is mostly the point of typeful programming.

① The special form the offers a glimpse into this system.

② See the CMUCL FAQ question on Python for explanation.

No comments:

About Me

My photo

I am S11001001, s11 for short.  Programmer and Free Software enthusiast.

Search for my name to see more stuff about me; no one shares my real name, and no one shares my username, though I can't understand why.