Here’s a great quote from Yaron Minsky about the use of types in functional programs.
[…] most of the advantage of types in a language like ML comes from completely vanilla uses of the type system. One of our programming maxims at Jane Street is to “make illegal states unrepresentable”. Algebraic datatypes, parametric polymorphism and abstraction can be used to great effect in this regard.
I think that people who are new to ML think of the type system as merely a constraint, that is to say, you write code as you did before, and then you see whether the compiler accepts it. As people get more experienced, they start to use the type system as a tool in its own right, and one of the things that is constantly on one’s mind is how to pass off as much of the proof burden as possible to the compiler. Most of this work can and should be done using boring old vanilla ML types.
This is a wonderful point. From the outside, the type systems of languages like Haskell and ML tend to look like a sort of archaic ecstatic religious rite. The bleeding mendicants pause as they shuffle past, sing a verse in praise of the purifying pain of strong typing, then prod themselves with pointy sticks and progress along their lonely road.
In practice, though, the type system is a powerful tool that helps to prevent mistakes, by forcing you to do some thinking up front. It’s not something you put up with; it’s something you value, albeit after a while.
One of the difficulties of crossing the Rubicon from type system outsider to insider is that it’s hard to find motivating examples in small, easily understood chunks of code, the sort of code that one writes as a beginner. The value doesn’t really begin to accrue until you’re either writing something moderately complex or refactoring existing code.
Fine one, there. :o)
I’ve always liked strong typing, because it won’t let the errors happen. In a case like a database, for example, when you put constraints (like the PostgreSQL REFERENCES and UNIQUE constraints), you are sure that an error will be thrown, and data will stay valid for your assumptions (i.e., that every value in this column has an identical in the other column or that every value in this column only occurs once).
But because this is not static (it is evaluated at runtime, by its nature), it becomes more a source of errors (however good) than a prevention of them. Static is better, of course.
Then in cometh the ML-style type system. If we could have it for things like databases…
Imagine, for example, that, in OCaml, you can’t pass a file handle that was not opened for reading into a function that will read from it. That is an error that is stopped statically. Needless to say it is a common runtime error, in the cases where the file handle type is enforced dynamically (reading from a write-only handle).
All these cases of types can be expressed well in an ML-style type system, statically, so that with a little thinking upfront, as you say in this post, many errors can be simply eliminated, using the rich type system to do the work.
We haven’t even got to using the Maybe data type (in Haskell, or the option data type in the MLs) to prevent cases of blind faith, like when one doesn’t check for the NULL result of a call to malloc(3) or fopen(3). In Haskell/ML, you can’t not check. This is not necessarily a constraint – it is a buglessness guide. Little wonder once you compile in ML-esque languages, you’re probably on the right track. Can’t be said for Java. NullPointerException.
I wish we used these nice type systems (the Haskell/ML kind, which even infer a lot, and save us code redundancy, which can’t be said of nearly all other polymorphic alternatives) as programming tools/aids, and not just as constraints, whole classes of problems would disappear.
And nice, well-written paragraph there (right after the quote). Very rich play on words … almost Haskellesque! :o)
Indeed, static typing suffers from a lack of powerful context-free examples, simply because any code fragment that can be grokked completely doesn’t really need static typing; it almost seems like only an idiot would need the help.
Another big advantage of a type system is that it’s much easier to quickly figure out what’s happening with an unfamiliar function. Does that ‘getUsers’ method return a list of usernames, or a list of user objects, or something else entirely? With static type systems (explicit or implicit), an IDE can tell you.
Another important point: “compile-time” is the wrong term. The right term is “write-time”. In that a good editor will silently compile/check anything you write and give you instant feedback.
A shame, really, that the most powerful type systems are employed by relatively ‘niche’ languages.
Re: Java’s NullPointerException – there’s an as yet unconfirmed plan to add some sort of annotation to mark any given type declaration as needing compile-time enforced checking that it couldn’t possibly hold a null value. A small but useful step.
Revence: no, really clever would’ve been to work in Haskellers wearing hairshirts so as to get a reference to the (relatively) famous retrospective SPJ did, ‘Wearing the hairshirt’.
The point is well-taken. However, typeful programming isn’t tied to static type systems. Encoding statements about a program into the types (or, if you adhere to the types-are-inherently-static terminology, whatever it’s called in your neighborhood) is at least as possible and just as common in latently-typed languages. Moreover, type systems aren’t the only sources of proofs about program properties.