Lambda the Ultimate

(This is my first post on LtU, so please tell me if I do anything wrong!)

I've been chewing on this question for a while: How did Glasgow Haskell's type system get so complex? Miranda had a relatively simple Hindley-Milner-style type system. It could do a lot, so people started applying it to more complex tasks, and eventually bumped up against limitations. Haskell added type classes, and they overcame many of these limitations. After a few more iterations of this, we have multi-parameter type classes with functional dependencies. Similar extensions have occured across the language, though few as dramatic as the type class situation.

Haskell's extended type system is Turing-complete. This is rather disturbing, because now Haskell is not one language, but two; one on each side of the :: sign.

Would adding basic data types like lists and integers to the type system be a useful extension? Probably; it would assist with doing compile-time computation, something that many Haskellers have been (ab)using their type system for. How about adding I/O capabilities to the type system? Could come in handy. Who's to say what you can and can't do with types?

The conclusion, chillingly, is that carrying the type system idea to its logical conclusion would leave us with two languages, each with the same capabilities. Each time you added something to one language, you would want to add it to the other. You would have to update the compiler in two places. Any language design effort would be doubled.

This is an extreme example of what could happen, of course, but it definitely makes you ask: Is there a better way? Lisp has shown us that preprocessing code with code in the same language is a big win, both in terms of simplicity and expressive power. I propose that we do the same thing with the type system, and, in fact, that a type system will not be satisfactory until it is the same as the language it types.

I wish I had a paper to present on this; I don't. It just hit me an hour or so ago, and I need feedback on the idea before I can write a paper. So: What do you think? I am I totally off-target? Have you been thinking on the same lines, and, if so, have you got any more specific ideas?

The Alloy Analyzer is a tool developed by the Software Design Group for analyzing models written in Alloy, a simple structural modeling language based on first-order logic. The tool can generate instances of invariants, simulate the execution of operations (even those defined implicitly), and check user-specified properties of a model. Alloy and its analyzer have been used primarily to explore abstract software designs. Its use in analyzing code for conformance to a specification and as an automatic test case generator are being investigated in ongoing research projects.

Alloy has been mentioned before, but with the recent discussions revolving around IDEs and questions about whether some kinds of checking belong in the language or in the tools surrounding the language, I thought it might be worth revisiting. In fact, it's tempting to suggest that we at LtU adopt a new category for stories: "Lightweight Formal Methods," and that we editors attempt to establish a continuum with respect to stories that fit the category. For example, Pierce makes the observation in TAPL that type systems are a particular kind of lightweight formal method, and that one of their benefits is that they're the only kind that are guaranteed to be used. Alloy falls in the "outside the language proper, but still incremental" category, and somewhere else on the spectrum you have full-blown theorem provers like Twelf, Coq, MetaPRL, et al. Does it make sense to try to unify some of the discussions about the boundary between languages and external tools under this umbrella?