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...
