Superficially Substructural Types at ICFP 2012!

My paper with Aaron Turon, Derek Dreyer, and Deepak Garg, Superficially Substructural Types, was accepted for publication at ICFP 2012! We'll be revising it (and possibly changing its title) in the next few weeks, to take the reviewers' comments into account.

Djikstra's Shunting Yard Algorithm

If you want to understand bottom-up parsing, one of the best places to start is Djikstra's shunting yard algorithm for parsing arithmetic expressions. Unlike general LR parsing, it maintains separate stacks for the intermediate parse trees and the parsing problems to be done. It's simple enough, in fact, that for simple problems my go-to parsing method is to use a recursive descent which makes subroutine calls to Djikstra's algorithm. (For more complicated problems, I use yacc and profanity.)

Recently, I read Danvy and Millikin's Refunctionalization at Work, which included as an example of refunctionalization Djikstra's shunting yard algorithm. What's really elegant about their presentation of this algorithm is that they show how to encode the control structure into the call stack (the way functions are supposed to work).

type token = LIT of int | PLUS | TIMES | LPAREN | RPAREN
type exp = Int of int | Add of exp * exp | Mul of exp * exp

let rec exp = function
  | ([],           [e]) -> e
  | (LIT n :: ts,  es)  -> exp (ts, Int n :: es)
  | (PLUS :: ts,   es)  -> exp (add (ts, es))
  | (TIMES :: ts,  es)  -> exp (mul (ts, es))
  | (LPAREN :: ts, es)  -> exp (par (ts, es))
  | (ts,           es)  -> failwith "nil: no parse"    

and add = function
  | ([],                  e2 :: e1 :: es) -> ([], Add(e1, e2) :: es)
  | (LIT n :: ts,         es)             -> add (ts, Int n :: es)
  | ((PLUS :: _) as ts,   e2 :: e1 :: es) -> (ts, Add(e1, e2) :: es)
  | (TIMES :: ts,         es)             -> add (mul (ts, es))
  | (LPAREN :: ts,        es)             -> add (par (ts, es))
  | ((RPAREN :: _) as ts, e2 :: e1 :: es) -> (ts, Add(e1, e2) :: es)
  | (ts,                  es)             -> failwith "add: no parse"

and mul = function 
  | ([],                  e2 :: e1 :: es) -> ([], Mul(e1, e2) :: es)
  | (LIT n :: ts,         es)             -> mul (ts, Int n :: es)
  | ((PLUS :: _) as ts,   e2 :: e1 :: es) -> (ts, Mul(e1, e2) :: es)
  | ((TIMES :: _) as ts,  e2 :: e1 :: es) -> (ts, Mul(e1, e2) :: es)
  | (LPAREN :: ts,        es)             -> add (par (ts, es))
  | ((RPAREN :: _) as ts, e2 :: e1 :: es) -> (ts, Mul(e1, e2) :: es)
  | (ts,                  es)             -> failwith "mul: no parse"

and par = function
  | (LIT n :: ts,  es) -> par (ts, Int n :: es)
  | (PLUS   :: ts, es) -> par (add (ts, es))
  | (TIMES  :: ts, es) -> par (mul (ts, es))
  | (LPAREN :: ts, es) -> par (par (ts, es))
  | (RPAREN :: ts, es) -> (ts, es)
  | (ts,           es) -> failwith "par: no parse"

let parse ts = exp (ts, [])

This is really very nice, and make some of the more opaque features of bottom-up parsing much more comprehensible. In particular, shift actions correspond to tail calls in the parsing procedures, and uses of the goto table correspond precisely to non-tail calls. For example, in the fourth line of add, we recursively call the mul procedure, and then resume parsing in the add mode once mul returns.

One natural question is whether we could profit by making the partial parse stack es implicit (eg, by switching to monadic style). (Eg, are there any equational derivations that this would simplify?) Another is whether this style works for general LR(k) parsing. If so, it could yield a significantly better exposition of LR parsing than the standard automata-theoretic accounts.

Superficially Substructural Logic

Together with Aaron Turon, Derek Dreyer, and Deepak Garg as coauthors, we have a new draft paper out: Superificially Substructural Types.

Many substructural type systems have been proposed for controlling access to shared state in higher-order languages. Central to these systems is the notion of a resource, which may be split into disjoint pieces that different parts of a program can manipulate independently without worrying about interfering with one another. Some systems support a logical notion of resource (such as permissions), under which two resources may be considered disjoint even if they govern the same piece of state. However, in nearly all existing systems, the notions of resource and disjointness are fixed at the outset, baked into the model of the language, and fairly coarsegrained in the kinds of sharing they enable.

In this paper, inspired by recent work on “fictional disjointness” in separation logic, we propose a simple and flexible way of enabling any module in a program to create its own custom type of splittable resource (represented as a commutative monoid), thus providing fine-grained control over how the module’s private state is shared with its clients. This functionality can be incorporated into an otherwise standard substructural type system by means of a new typing rule we call the sharing rule, whose soundness we prove semantically via a novel resource-oriented Kripke logical relation.

I'm very excited by this work, since this paper represents a big step towards a longstanding research goal of mine: generalizing separation logic so that resource abstractions can be defined by the programmer on a per-module basis.

Michael Dummett

The British philosopher Michael Dummett's books The Logical Basis of Metaphysics and Frege: Philosophy of Language were some of the most useful books I read during my degree. His analysis of Frege's sense-reference distinction has been very helpful to my understanding of dependent type theory, and his explanation of intuitionism was quite helpful in understanding the relationship between the structural-proof-theoretic view of types and the realizability interpretation of types.

So I was disappointed to learn that he died last week, but pleased  to read the reminiscences of him by his colleagues posted on the New York Times.

Adding Equations to System F, at ESOP 2012

Our paper on adding equations to system F was accepted to ESOP 2012!

The reviewers suggested rather a lot of improvements to the paper, so I'm taking the draft down while we incorporate their suggestions. It will go up again in a few weeks, after the revisions are done, and undoubtedly in a much-improved state. 

Updata

The final version of our POPL paper on space-bounded FRP is available now -- we bought two extra pages from the ACM, and used them to add a lot more detail to the examples. With luck the paper will be a lot clearer now.

Also, Bob Atkey has a new blog post on using delay operators to model guarded definitions in type theory. He takes advantage of the fact that delay is a strong lax monoidal functor (with respect to the monoidal structure of products) to use the syntax of applicative functors.

This is a very elegant way of embedding these things into Haskell. Unfortunately, I have never liked the typing rules for the idiom syntax, since they don't work solely on the outermost type constructor. This means type-theoretic properties like normalization are messier to prove. (Bob evades this problem with semantic techniques, though.)


All his other posts are very good, too.

Adding Equations to System F

Nick and I have a new draft out, on adding types for term-level equations to System F. Contrary to the experience of dependent types, this is not a very hairy extension -- in fact, I would not even hesitate to call it simple.

However, it does open the door to all sorts of exciting things, such as many peoples' long-standing goal of putting semantic properties of modules into the module interfaces. This is good for documentation, and also (I would hope) good for compilers --- imagine Haskell, if the Monad typeclass definition also told you (and ghc!)  all the equational rewriting that it was supposed to do.