APPSEM '98

Program Structuring in Haskell

Mark P Jones

Slide 14

Here is another example, this time based on some work that I've been doing recently to formalize the meaning of bytecode verification for Java. The basic idea here is to model bytecode instructions as functions with detailed types that capture the constraints of verification.

This slide shows simplified versions of the types for two instructions: "iadd" for integer addition, and "idiv" for integer division. Both instructions work by popping two integer values from the top of the Java virtual machine's stack, performing the appropriate operation on them, and then pushing the resulting integer back on to the stack. This is what the portion of the type to the right of the => symbol indicates in each case. (The triangle operator is used to describe the shape of stacks; you should read it as a right associative operator that is pronounced "pushed onto".)

Of course, many Java virtual machine instructions make use of computational effects such as exceptions, global state, and so on, so it should not be too surprising to see a monad in the types of these instructions. It would, perhaps, be possible to construct a single JVM monad that supported all of the effects that we were interested in ... but that would not be very modular. Instead, we can use type classes to identify particular classes of monads. In the example shown here, we can see the fundamental difference between "iadd" and "idiv". The former has no external computational effect, and hence will work with any monad. The latter, however, may raise an exception if the divisor is zero, and hence requires a monad that supports this additional feature; we use a "DivZero" class here, a sublass of "Monad", to reflect this.

There isn't time to explain it here, but the same ideas can be used to partition state according to class and package visibility rules, which again gives more flexible and accurate types for bytecode instructions than a unified state monad would allow.

Let us emphasize the key features from these two examples: (1) effects are inferred automatically as part of the type inference process; (2) the descriptions are more modular because we don't need to know all the possible effects that a program may require, just the effects used by the small fragment of code that we are interested in.

Next...