What you should know about type systems
I read today, a really good essay on type systems. It covers what they can be used for and the differences between dynamic and static systems (although the word ‘type’ is used in both, it doesn’t mean the same thing at all.)
Even though I have not used Haskell, ML, or any of the other languages which make a compelling case for strong, static typing; I have been favoring such systems for a long time. I’m reaching the point in my education about programming practice, where I want the computer to do as much reasoning as possible about my programs. So any system of logic, which the computer can use to reason about my program, seems to me of enormous benefit. Especially so, when I can extend that system (by creating my own types) to prove properties of my programs that I’m worried about.
The article gives some really good examples, that serve to show how powerful a computer reasoning system can be, how much it can help you to know:
- http://wiki.di.uminho.pt/twiki/pub/Personal/Xana/WebHome/report.pdf. Uses types to ensure that the correct kinds of data are gotten out of a relational database. Via the type system, the compiler ends up understanding how to work with concepts like functional dependencies and normal forms, and can statically prove levels of normalization.
- http://www.cs.bu.edu/~hwxi/academic/papers/pldi98.pdf. Uses an extension to ML’s type system to prove that arrays are never accessed out of bounds. This is an unusually hard problem to solve without making the languages that solve it unusable, but it’s a popular one to work on.
- http://www.cis.upenn.edu/~stevez/papers/LZ06a.pdf. This is great. This example uses Haskell’s type system to let someone define a security policy for a Haskell program, in Haskell, and then proves that the program properly implements that security. If a programmer gets security wrong, the compiler will complain rather than opening up a potential security bug in the system.
- http://www.brics.dk/RS/01/16/BRICS-RS-01-16.pdf. Just in case you thought type systems only solved easy problems, this bit of Haskell gets the type system to prove two central theorems about the simply typed lambda calculus, a branch of computation theory!
And just like any good research paper, it ends with a series of open questions:
- For what interesting properties of programs can we build static type systems?
- How close can we bring those type systems to the unattainable ideal of never rejecting a correct program?
- How easy can it be made to program in a language with such a static type system?
- What is the cost associated with accidentally rejecting a correct computer program?
- For what interesting properties of programs can we build test suites via dynamic typing?
- How close can we bring those test suites to the unattainable ideal of never accepting a broken program?
- How easy can it be made to write and execute test suites for programs?
- What is the cost associated with accidentally accepting an incorrect computer program?