Of Types and Men15 February 2014
A type system is a wonderful thing. I find them very helpful in weeding out bugs early on in the development process. However, I am convinced that mainstream statically typed languages are less expressive and less ergonomic than they could be. Here’s what I’d like to see in a strongly-typed programming language.
1. Invalid types as warnings
You’re a capable man or woman, and you’ve written a wonderful program. You’ve written the code, satisfied the type checker, and ironed out the bugs.
Perhaps it’s a game where characters can be armed or not, so you use
Maybe Weapon (Haskell) or a nullable
Then, requirements change. You will have characters with multiple
weapons! Your type is now
[Weapon] (Haskell) or
(Java). You are forced to go through your entire codebase making
changes: some trivial, some logic changes.
At no point in this process can you run the program to see if any of the updated code is correct. Perhaps you’d like to try to spawn an unarmed character from the shell with your updated logic. This isn’t really possible in today’s statically typed languages.
If you’re lucky, your changes might be isolated in certain files which can be run independently. If you’re unlucky, you’ll be forced to try ad-hoc commenting out to placate the type checker.
Solution 1a: Not yet typed
Haskell, interestingly, has a notion of ‘not yet typed’. If you’re
building a new program and don’t want to implement everything at once,
you can use
undefined which will pass type checking for anything.
For example, if you’re building a restaurant simulator, you might write:
chefPrepare :: [Ingredient] -> Dessert chefPrepare = undefined
You can then happily write other functions that call
the type checker won’t get in your way.
Haskell can even give you hints as to what you need, when you’re halfway through implementing a program. With the TypeHoles extension, you can leave placeholders in your functions and Haskell will tell you what type value or function you need to use.
This is helpful during the initial implementation, but doesn’t help us in our refactoring situation above.
Solution 1b: Optional typing
Some lisps, including Scheme and Clojure, provide type checkers as a library. These aren’t part of the core language, and the compiler/interpreter does not enforce type correctness. Users can use these ‘optional type checkers’ to verify some or all of their code, as they please.
This is a wonderfully pragmatic approach, and works well. However, the type systems supported by optional type checkers is not always as sophisticated as a Haskell user would be accustomed to.
There are other interesting advantages of type checking being a library. It can evolve separately to the language itself, giving users more opportunities to experiment. It also makes it much easier to call the type checker programmatically, a feature that some statically typed language do not offer at all.
Solution 1c: Dynamically typed dialects
RPython is a quirky little language. It’s a proper subset of Python, so you can run your RPython programs on the standard Python interpreter (called CPython).
This allows you to run your program at any point, regardless of how invalid the types are. You can invoke the RPython compiler and have it check your types. However, if you find the errors confusing, or type checking is simply interrupting your flow, you can just run the program anyway.
Sometimes, you may find it helpful to deal with concrete errors with concrete values. By running your RPython program in CPython, you can slap print statements everywhere until your hacky prototype is working. Afterwards, you can appease the type checker.
Pypy, an interpreter written RPython, is developed something like this. The developers typically ensure their unit tests pass first, then fix any remaining type issues. It’s a great workflow, and few languages let you do this.
2. A Universal Type
Sometimes you need a universal type. There are programs that simply
cannot be written without it. Java has this, and calls it
Object. Haskell has
Dynamic, but it’s not quite as
expressive or concise.
Some notable use cases include:
I. Flattening an arbitrarily nested list. This is easily done with recursion and inspecting the type of a value. That said, a determined Haskell hacker can flatten a nested list with typeclass abuse.
II. Applying an arbitrary length list of functions
[a -> b, b -> c, ...] to a value of type
III. Serialising or deserialising arbitrary values.
3. The Environment as an effect
Pure language languages, such as Haskell, force you to be explicit about effects that your functions may cause. However, the programming environment itself is a piece of state, and Haskell does not allow us to declare that we will interact with it.
There are many (extremely useful) functions whose behaviour we could
model if we treat the environment as an effect. Haskell provides the
State monad; let’s suppose we have an
Environment type and a
Reading Types In The Environment
Python has a
pickle module that allows you to convert arbitrary
types to strings. This is a very powerful concept. For example, it
makes memoisation for arbitrary functions straightforward (I
understand it’s possible in Haskell, but it’s extremely non-trivial).
If we model the environment as an effect, dumping and loading serialisations is simply:
serialise :: Any -> WithEnvironment String -- Assume we return Nothing if we try to deserialise -- a type that isn't present in our current environment. deserialise :: String -> WithEnvironment (Maybe Any)
Writing Types In the Environment
We gain even more expressive power if we looking at mutating the
environment. Two excellent examples of this are mocking out functions
for testing, and
Now, a purist might ask why you’d even want
eval, since it can cause
some spectacular errors. One big advantage of providing
eval is that
it allows you to write an interpreter. In many scripting languages,
the users have developed interpreters that are much friendlier and
more capable than the built-in one.
For example, Python has bpython (which provides pop-up help using a curses interface) and ipython (which provides helper syntax, shell conveniences, history and sophisticated tab completion). Ruby has pry (which provides debugging and live editing), and Common Lisp’s slime paired with swank is extraordinary for interactive development.
Given this, an
eval function would have the following type:
-- You'd probably want eval to throw various exceptions -- in the case of bad input. eval :: String -> IO (WithEnvironment Any)
There are still many forms of type systems that are little explored in programming languages. When evaluating a type system, ask yourself:
I. What bugs can this type system catch?
II. What proportion of those bugs are difficult to catch otherwise?
III. What functions are difficult to express in this type system?
IV. What functions cannot be expressed in this type system?
V. What, if any, escape hatches does type system provide?
VI. Is this type system sound?
VII. How comprehensible are its type errors? How helpful are its suggested fixes?
With those questions in mind, it’s much easier to answer that nebulous question: do I want to program with this type system?