Lambda the Ultimate

Compositional type systems for stack-based low-level languages
by Ando Saabas and Tarmo Uustalu, appearing in Proceedings of the 12th Computing: The Australasian Theroy Symposium - 2006.

It is widely believed that low-level languages with jumps must be difficult to reason about by being inherently non-modular. We have recently argued that this in untrue and proposed a novel method for developing compositional natural semantics and Hoare logics for low-level languages and demonstrated its viability on the example of a simple low-level language with expressions (Saabas & Uustalu 2005). The central idea is to use the implicit structure of finite disjoint unions present in low-level code as an (ambiguous) phrase structure. Here we apply our method to a stack-based language and develop it further. We define a compositional natural semantics and Hoare logic for this language and go then on to show that, in addition to Hoare logics, one can also derive compositional type systems as weaker specification languages with the same method. We describe type systems for stack-error freedom and secure information flow.

I encountered the article while researching compositional type systems. I would like to hear people's thoughts about this article and compositional type-systems in general (are they interesting, esoteric, mundane?).

I wonder whether the following extension to the type inference mechanisms of languages like Haskell, ML, etc. would be possible, and, if so, desirable.

Today we write functions like

head (a:_) = a

and get warning messages concerning patterns not covering all possibilities. This is fine. However, I am not being warned when the compiler sees code like

head []

(even when head were defined like above, without a default clause that raises a runtime error.)

In principle, though, the type inference could collect for each value of algebraic datatype by which constructor this value could possibly have been created.

For example, the type of
unJust (Just x) = x
would not be (Maybe a -> a), but something like
(Maybe{Just} a) -> a
Consequently, the type of Nothing would be (Maybe{Nothing} a) and the type checker could flag occurences of
unJust x where (x::Maybe{Nothing} a)
or
head y where (y::[a]{[]})
as type error.

The consequence would be that it would be no longer worth a warning when writing functions with incomplete patterns. Rather, at the place where the function is used the compiler would be able to diagnose one of three outcomes:
- this will fail (when the intersection of the constructor sets is empty)
- it may succeed (when the intersection is not empty)
- it will succeed as far as pattern matching is concerned (when the constructor set of the type of the argument is a subset of the constructor set of the function argument type)

Case 1 could be treated like just another type error. Case 2 could provoke a warning. Case 3 is ok, of course.

To be sure, that would also encourage a different style. Instead of writing dozens of meanigless default cases like
foo _ = error "can't happen"
one could leave that out and let the compiler prove that indeed it can't happen.

(I hope I could express my thoughts clear enough despite english not being my native language.)

Rich Jones writes: I wanted to understand how FORTH is implemented, so I implemented it and wrote a step-by-step tutorial on what every bit does.

The tutorial is inside a (literate) code file you can download and run.

I've been told recently by people I trust that it is about time I learned Forth. This may be just what I was waiting for...