Embracing and extending the Levy language

I started writing the post about the thing I really wanted to write about, but then I realized that the background was already a long post on its own. So, that's this post! It's about two things:

1. Levy, an implementation of call-by-push-value that Andrej Bauer and Matija Pretnar wrote in OCaml for the PL Zoo. I made a fork of Levy that, among other small changes, reduces the need for parentheses by making operator precedence more like it is in OCaml.
2. A more divergent fork of Levy that adds datatypes in a familiar-but-as-yet-unmotivated way. This diverges from the goals of Levy - as a PL Zoo project, Levy aims to be a clean and uncluttered language implementation, and that's not the case for this more divergent fork. I'll call this new version of Levy... let's see... Levy#. Sure, that works.

Other things have been written about Levy at Andrej's blog and LtU.

Basic concepts

The big idea of call-by-push-value, and, in turn, Levy, is that it is a programming language that is incredibly picky about the difference between code that builds data (I'll call this value code as shorthand) and code that does stuff (I'll call this computation code). Value code tends to be really boring: 3 builds an integer value and true builds a boolean value. Levy also builds in a couple of total binary operations on integers, so 3 + x and y < 12 are both viewed by Levy as value code. Variables are always value code.

Computation code is more interesting. If-statements are computation code: if v then c1 else c2 examines the value built by v and then either does the stuff described by c1 or else does the stuff described by c2. Functions are computation code: fun x: ty -> c receives a value and then does the stuff described by c, possibly using the value it received.

The computation code return v does a very simple thing: it takes the value built by v and says "look, I made you a value." If the value code v had value type ty, then the computation code return v has computation type F ty. So yeah: I hadn't talked about types yet, but pieces of value code are given value types and pieces of computation code are given computation types.¹

Which brings us to an interesting kind of value code that I didn't mention before: thunk c wraps up (and suspends) the computation code c in a value; if the computation code c had computation type ty, then the value code thunk c has value type U ty.

The typical type of a function that would be written as int -> int in ML is U (int -> F int). It has to be a value type (ML functions are values), hence the "U", and the computation code in the function wants to take a value, do some stuff, and eventually return an integer. Here's an implementation of the absolute value function:

   val abs = thunk fun n: int -> 
     if n < 0
     then return 0 - n
     else return n ;;

In order to use the absolute value function, we have to "un-thunk" the computation code inside of the value: the computation code force v does this. Where we'd write (abs 4) in ML, we write force abs 4 in Levy (force binds more tightly than anything, including application).

Evaluation order

A consequence of being persnickety about the difference between value code and computation code is that Levy is very explicit about sequencing. The SML/Haskell/OCaml code "foo(abs 4,abs 5)" means "call foo with the absolute values of 4 and 5." One occasionally hard-learned lesson for people who have programmed in both SML and OCaml is that, if abs contains effects, this code might do different things: SML has a specified left-to-right evaluation order, but OCaml's evaluation order is unspecified, and in practice it's right-to-left.

Such underspecification is impossible in Levy, since calling a function is a computation, and computations can't be included directly in values! Instead, if I have computation code c of type F ty, we expect it to do some stuff and then say "look, I made you a value (of type ty)." The computation code c1 to x in c2 does the stuff described by c1, and when that stuff involves saying "look, I made you a value", that value is bound to x and used to do the stuff described by c2. Therefore, when translate our SML/Haskell/OCaml code above to Levy, we have to explicitly write either

   force abs 4 to x1 in
   force abs 5 to x2 in
   force foo x1 x2

or

   force abs 5 to x2 in
   force abs 4 to x1 in
   force foo x1 x2

That concludes the introduction of Levy, (my slightly de-parenthesized fork of) the language implemented by Bauer and Pretnar. There are two example files here (discusses basics) and here (discusses functions).

Matching

The first new feature in Levy# is the addition of a new kind of computation code, match v with | pat1 -> c1 ... that is a generalization of both let-expressions let x be v in c and if-expressions if v then c1 else c2 from Levy. Patterns like pat1 are a refinement of value code: constants are patterns, variables are patterns (variables in patterns are binding occurrences, like in most functional languages), but addition is not a pattern, and variables can only appear once in a pattern.

The simplest new thing that we can do with this language construct is write computation code that mimics a switch statement in C:

   val f = thunk fun x: int ->
     match x with
       | 1 -> return 4
       | 2 -> return 3
       | 3 -> return 2
       | 4 -> return 1
       | 5 -> return 0
       | y -> return (x + y) ;;

This function is included as an example in the "datatype" fork of Levy# on Github here; let's look at what it actually does in the interpreter:

   bash-3.2$ ./levy.byte switch.levy 
   ... snip ... 
   Levy. Press Ctrl-D to exit.
   Levy> force f 1 ;;
   comp F int = return 4
   Levy> force f 3 ;;
   comp F int = return 2
   Levy> force f 5 ;;
   comp F int = return 0
   Levy> force f 7 ;;
   comp F int = return 14

That's what I expected to happen; hopefully it's what you expected to happen too. Let's declare victory and move on.

Using datatypes

The main innovation of Levy# is the introduction of an inductive datatype mechanism, which is basically a bedrock component of every functional programming language (that isn't a Lisp) ever. This should have been a relatively small change, but parser generators are the worst and I'm bad at them so I basically had to rewrite the parser to have a new phase. Sigh.

I'll start with showing how datatypes are used, because that's a little more standard than the way I declare them. It would look exactly like the uses of ML datatypes, except that I curry them in a Haskell-ey fashion. The function sumlist, which sums up a list of integers, looks like this:

   val sumlist = thunk rec sumlist : list -> F int is 
     fun xs : list ->
       match xs with
         | Nil -> return 0
         | Cons x xs -> force sumlist xs to y in return x + y ;;

The other thing that's new in the above example is the use of Levy's fixedpoint operator, but there's nothing interesting there from the perspective of reading the code. This and other examples are in datatype.levy, by the way.

Side note: I'm lazy but still wanted a realistic execution model *and* coverage checking (redundant/non-exhaustive matches raise warnings), so I limited the current version of Levy# to depth-1 pattern matching:

   Levy> match v4 with | Cons x1 (Cons x2 xs) -> return 0 ;;
   Type error: Cons x2 xs not allowed in pattern (depth-1 pattern matching only)

If I was doing this for real I'd implement real coverage checking and pattern compilation as a code transformation, which would leave the depth-1 pattern matching interpreter unchanged.

So that's the use of datatypes; one upshot is that my pieces of value code are maybe a bit more interesting than they used to be: I can make big piece value code like Cons 4 (Cons 9 (Cons 16 (Cons (-1) Nil))) to create a big piece of data. I think that's kind of interesting, at least.

Declaring datatypes

Datatypes are just a way of telling the computer that you want to work with a particular set of inductively defined structures (at least this is what strictly positive datatypes, the only ones Levy# allows, are doing). A point that I've haltingly tried to make in a previous post was that, well, if you're going to write down a particular set of inductively defined terms, a canonical-forms based logical framework like Linear LF is a perfectly good language to write that in.

So our constants look basically like the declaration of constants in a Linear LF signature, except that we make the constants uppercase, following ML conventions:

   data Nil: list
      | Cons: int -o list -o list

It's a little point, but it's kind of a big deal: we can understand all the values in Levy# as canonical forms in a simply-typed linear lambda calculus with integers and some arithmetic operations - kind of like Twelf with the integer constraint domain extension.²

The reason it's a big deal is that we can now observe that the two kinds of "function types" we have in this language are way different. There's a computational arrow ty1 -> ty2 that we inhereted from Levy, and then there's a Linear LF linear implication arrow, a value arrow ty1 -o ty2 that we use in value code to construct patterns and values. I didn't invent this idea, it's actually a subset of what Licata and Harper propose in "A Universe of Binding and Computation" (ICFP 2009). Dan Licata would call the Linear LF arrow a "representational arrow," which is probably a better name than "value arrow."

Of course, the values that we actually use are, without exception, at atomic type; if we try to even write down Cons 4, which seems like it would have type list -o list, we get a type error from Levy#: constructor Cons expects 2 arg(s), given 1. So by requiring that all the Linear LF terms (i.e. value code) be canonical (beta-normal and eta-long), I've effectively excluded any values of type ty1 -o ty2 from the syntax of the language.

What would it mean to introduce value code whose type was a linear implication to Levy#? Well, that's the thing I really wanted to write about.

---

¹ Focusing and polarization-aware readers will notice that this has something to do with focusing. In particular: positive types are value types, negative types are computation types, F is "upshift," and U is "downshift."
² Technical note: Boolean values, from the perspective of the value language, are just two defined constants, as explained here. That's important: we have Boolean constants that are values, but the elimination form for Booleans is computation code not value code. If we had an "if" statement at the level of values, all sorts of crazy (and interesting) stuff could potentially happen. At least for the moment, I'm not considering that.

Video Lecture on Constructive Provability Logic

I've previously blogged about the principles of constructive provability logic and about our paper on the topic being accepted to IMLA. Since then (in fact, since my last blog post), I've given three versions of a talk on the logic: first at CMU before I left for my internship at Microsoft Research, the second at the workshop on Intuitionistic Modal Logic and Applications in Nancy, France,¹ and the third the next day at LIX in Saclay (south of Paris) France.² After tweaking that talk three times, I decided to tweak it once more and put it on the web on my page of resources about Constructive Provability Logic.



This was actually quite a bit harder than I'd expected! It didn't seem quite as difficult when I did it for the Linear Logical Algorithms presentation a few years ago, but I guess I was forcing myself to be less perfectionist there (requiring one take instead of 4 definitely forces you to be less perfectionist). Especially in the first two videos, the number of repeated takes comes across in my rather affected tone of voice - which is what you get when you over-rehearse something, at least if "you" is a person who (like me) has forgotten anything he ever learned about the "illusion of the first time".

The effort required was such that I don't realistically see myself doing this too often again, but hopefully this will be at least moderately helpful to someone.

---

¹ While in Nancy, I took a picture out of the window of the dorm where I was staying, and thereby whittled away a few more of my 15 minutes of fame.
² Nothing famous happened there, but I did have excellent fondue.

Party like it's 1995

It is humbling but enlightening when you're struggling to figure out how to describe something and you realize someone already nailed the exposition two decades ago. That's how I felt when I stumbled across this invited paper by Dale Miller, "Observations about using logic as a specification language." Still a good paper!

I wonder if the late eighties and early nineties felt as exciting at the time as they look in retrospect for the logic community. I guess the answer is "yes" - I recall Bob Harper talking about one informal European workshop in that period where he was presenting LF, Girard was presenting linear logic, and maybe one of the uniform proofs people were presenting uniform proofs too? Maybe someone who's spending the summer in Pittsburgh can prod Bob into blogging about that meeting, it's a good story. (This reminds me, I need to add Bob's blog to the sidebar!).

Also: completeness of focusing via cut and identity

Speaking of uniform proofs: I've been fiddling for some time with this view of that the completeness of a focused sequent calculus can be proven more-or-less directly from the standard metatheory of the focused sequent calculus: cut admissibility and identity expansion. (The completeness of focusing, if you recall, is good for many reasons. It gives us logic programming, and it allows us to think in terms of synthetic inference rules in our logical frameworks.) Frank first observed this way back when, I cleaned up and Twelfed up his proof a long time ago and wrote up a version of the argument for ordered linear logic in a tech report recently. the main weakness of our strategy is that, in its current version, it doesn't deal with inversion on positive types, which is why I call it "weak focusing" instead of "focusing."

A recent MathOverflow question asked (in a slightly convoluted way) about the completeness of focusing with respect to a Prolog-like language. Since Prolog-like languages don't run into the problem with positive types, "our" strategy* works fine, so I used this as an excuse to finally write out the full argument in a setting that didn't have a lot of other extraneous stuff going on.

* I'd like to know if someone came up with this strategy before us!

Hacky post: binary, where do you live?

This is a problem that's come up various times in the past year, and I wanted to write it up quickly. Much more about hacking (Standard ML in particular, though I don't think it's a problem unique to Standard ML), I thought about putting it on my more personal blog, but it seemed out of place there too.

Problem description: oftentimes when you have a binary file, you want to distribute it along with some other resource files (think images and whatnot). You expect that some collection of files containing these images will be distributed together, but you want to be able to move them around on your own system or to a friend's system as one atomic block without breaking everything. This means, effectively, that you have to be able to have the program start with any current directory and understand how to change directories to the directory where "it lives". The easiest way of doing this in Standard ML is to change directories (OS.FileSys.chdir) to whichever directory the commandline argument that ran the program appeared to live in (OS.Path.dir (CommandLine.name ())).

So far so good

We can illustrate how this works and fails to work with a one-line test program that we compile in MLton.

structure Foo = struct val () = print ("I'm " ^ CommandLine.name () ^ "\n") end

Let's save this in /tmp, compile it, and run it:

$ cd /tmp
$ mlton foo.sml

Okay, now wherever we go, the directory part of (CommandLine.name ()) is going to be proper for getting from the current directory of the user into the directory where the binary lives:

$ ./foo
I'm ./foo
$ cd ..
$ /tmp/foo
I'm /tmp/foo
$ cd /tmp/baz
$ ../foo
I'm /tmp/baz

Symlinks and paths and lying, lying command lines

The problem's gonna come when we want to execute our file from the path or from a symlink: then, the apparent working directory given by (CommandLine.name ()) will *not* necessarily be the place where the executable itself lives.

$ pwd
/tmp/baz
$ export PATH=$PATH:/tmp
$ foo
I'm foo
$ cd /tmp
$ mkdir baz
$ cd baz
$ ln -s ../foo foo2
$ ./foo2
I'm ./foo2

The solution adopted by the group of us that wrote the C0 compiler is to notice that if you call something from a shell script it gets its path expanded. Therefore, if we have a shell script doing nothing but calling our program, the program will get called with its absolute path and therefore the program's attempts to chdir into the directory where its binary (and associated resources) live will succeed.

$ pwd
/tmp/baz
$ mv ../foo ../foo.exe
$ echo '$0.exe $*' > ../foo
$ chmod a+x ../foo
$ foo
I'm /tmp/foo.exe

However, this solution only works for things on the $PATH, not for symlinks:

$ ./foo2
./foo2:1: ./foo2.exe: No such file or directory

Wrapping up

Can anyone think of a better way to do this? The shell script is simple, but it seems unnecessary. Perhaps I really should be asking this on StackOverflow, but the Standard ML conversations on StackOverflow are depressing to say the least.

P.S. - If you're distributing your program by way of a SML/NJ heap image, (CommandLine.name ()) will always be sml. To defeat this, when you issue the command that reloads the heap image, add the argument @SMLcmdname=$0. That is, of course assuming you're reloading the heap image from within a shell script, which is the common way to make an executable using SML/NJ. So, in effect, with SML/NJ this problem is "automatically solved" because you're already redirecting through a shell script.

P.P.S. - After I wrote this post, I realized it was probably a language-independent concern. Sure enough, there's StackOverflow posts about this problem from the perspective of C and C++. Seems like it's just a hard problem; crud.

Tell me a story of logic

I have a little technical note that I'm working on, in which I tell a story about linear logic that I tried to work out a year ago and finally returned to with Bernardo Toninho and Yuxin Deng last week. But as I tried to write the introduction, the two-year-old voice in my head kept asking "why?" Why do I need to tell this story? What's the point? The resulting thoughts don't really belong in the technical note I wanted to write, but I hope they're just barely coherent enough that they're worth putting here. (Note: there is a similar discussion to this one in Section 3 of my thesis proposal.)

Big picture: before we can contemplate any discussion of the formal correctness of any system (a logic, type theory, programming language, cryptographic protocol, or self-driving car) - before we can even ask ourself what "correctness'' means - we have to have a way of formally specifying the system itself. Mathematicians do this by defining sets, category theorists by enumerating universal mapping properties. However, if you're writing down theorems to be checked by a computer, there's almost exactly one game in town: systems for mechanized mathematics have a built-in facility for directly giving (co)inductive specifications of systems.

A tool's interface for describing inductive specifications is, therefore, a matter of some importance. In most systems, the statement of an inductive specification looks something like a datatype declaration in a programming language in ML or Haskell. One system for mechanized mathematics, Twelf, takes a rather different approach. Rather than directly specifying an inductive structure, Twelf users specify a signature of type families and constants in the dependent type theory LF. If you asked someone about this while they were in a hurry to catch a plane, they'd probably respond "oh, that's what adequacy theorems are for" and run away.

A word on adequacy

In the first paper on LF, Harper, Honsell, and Plotkin discuss adequacy theorems. When we write down a bunch of type families and constants in an LF signature, that means that we can form a certain (inductively-defined!) set of terms. To use a standard example, given the LF signature

  nat: type.

  z: nat.

  s: nat -> nat.

we can create well-typed terms of type nat that look like z, (s z), (s (s z)), and ((λx. s x) (s z)). That fourth example has a β-redex that, when we reduce it, turns it into the third example. We usually say that the above LF specification is adequate because there is a one-one-correspondence between natural numbers and normal terms of type nat in this signature.¹ In general, to quote Harper and Licata's 2007 "Mechanizing metatheory in a logical framework",

An LF representation of a language is adequate iff it is isomorphic to the informal definition of the language.

I'm currently thinking that this might be the wrong slogan, because the imprecision of "informal" leads to seemingly inevitable misunderstandings. Another slogan that I might consider in its place is that an LF specification is adequate iff it is isomorphic to the inductive specification of the language. It's just really very deeply ingrained in our collective heads that when we're writing down horizontal lines on paper, that means an inductive specification. But perhaps that's not giving LF enough credit! There's no reason to cede that my scratches on a whiteboard have any special spiritual relationship with inductive definitions and not LF signatures (or sets in ZFC or constructions in category theory, for that matter).

Taking the view that adequacy relates the canonical forms of LF to some inductively defined structure ("on paper" or otherwise) has two advantages that I see. First, it turns adequacy into something that takes place entirely within formal mathematics. In fact, we have a pretty clear understanding of how to write "first-order" or "concrete" LF types that encode inductive definitions (hint: never allow left-nested arrows). But this means that we can prove adequacy theorems in Twelf. My Twelf code proving a bijection between de Bruijn lambda calculus terms and HOAS lambda calculus terms is, in this view, part of an adequacy theorem.² The second advantage, in my mind, is it clarifies why we never formally prove adequacy with respect to our "informal definitions" (a point that Daniel Lee and I poked a bit of fun in our SIGBOVIK 2007 paper Manifest Adequacy). When I've been using Adga for awhile, I think of my on-paper notation as corresponding to inductive definitions (or, occasionally, inductive-recursive definitions, the more powerful variant of inductive definitions available in Agda). When I've been using Twelf for awhile, I think of my on-paper notation as corresponding to LF signatures that use higher-order abstract synatx. It's only in the event that I want to know that these two ways of formalizing the same system coincide that I would actually think about adequacy in practice. To reempahsize, in this event adequacy is an entirely formal concept.

Why logical frameworks?

There's no contrarian impulse that lead to LF being used to encode systems. Harper, Honsell, and Plotkin made the point as well as I could hope to:

The structure of the LF type system provides for the uniform extension of the basic judgment forms to two higher-order forms introduced by Martin-Löf, the hypothetical, representing consequence, and the schematic, representing generality.

There are two important points to make about the above quote. The more obvious one is that LF, compared to "raw" inductive definitions, gives a clean notion of hypothetical reasoning and uniform substitution (the basis of what was later termed "higher-order abstract syntax"). The less obvious point is that, in the above quote, Harper, Honsell, and Plotkin are referencing Martin-Löf's "On the meaning of logical constants and the justification of the logical laws," which isn't actually about LF. Rather, it's a story about how we understand the meaning of propositions and how we establish that a logic's definition makes sense in the presence of a uniform notion of hypothetical judgments.

Martin-Löf's discussion, which Pfenning and Davies termed the "judgmental methodology" in their their judgmental reconstruction of modal logic, is important for people who write systems in Twelf because it sets up a particular world-view that maps quite well onto formalization in LF. To put it another way, the judgmental methodology is one important source of intuitions that guide the mental process of mapping between our "on-paper" notation and LF signatures. And so it's no accident that 1) we use Twelf a lot at Carnegie Mellon 2) our student reading group usually reads On the meaning of logical constants and the justification of the logical laws at least once every other year. The judgmental properties underlying LF and Martin Löf's reconstruction are the same, so understanding the judgmental methodology is a good way of understanding LF formalization.

This continues to be the case in the Linear LF extension to LF, where linear hypothetical assumptions are understood to be resources that will be consumed in the service of building a goal. The underlying story here, which Wikipedia originally attributes to Lafont, is called the resource interpretation, and it allows us to understand how to do things like represent programming languages with state conveniently, because "a bunch of memory" is a concept that can be represented as "a bunch of resources." The story that we tell about linear logic - the resource interpretation - is important in part because it gives us intuitions for understanding LLF formalizations.

I don't know that I can speak for where my intuitions about inductive definitions come from - as I've said before, computer scientists tend to treat them as pretty foundational. On the other hand, it's difficult to really use the "raw" inductive definitions provided natively by most non-Twelf provers to reason about programming languages, which is why there has been much recent (and, from an outside perspective, seemingly quite successful) work aimed at providing the right tool support for specifying and reasoning about programming languages in highly-developed proof assistants like Coq. The only danger here is, as soon as you start adding layers of interface between yourself and inductive definitions, the question of adequacy (the informal version, at least) again raises its head: there's not necessarily the same Martin-Löfian story guiding you, so where are your intuitions about the correctness of your system coming from? How would you actually prove that it corresponds to an ostensibly equivalent LF signature?

This, in turn, is one reason why two-level approach have been recently popularized by Felty's Hybrid system and Gacek's Abella. In these systems, there's a specially supported logical layer where one can use the same kind of intuitions we use in LF encodings. LF or LLF could, in fact be used for this logical layer, though these two systems use different variations on that theme. The second layer is a separate facility for reasoning about these encodings.

I'll stop here, though one argument I might be interested in trying to make in the future is that Twelf itself is actually the original two-level approach. There's an even stronger argument to be made in the case of HLF, Jason Reed's implementation of meta-reasoning for LLF on top of Twelf. However

¹ We usually say canonical terms or canonical forms, not normal terms. The canonical forms are the β-normal η-long terms. However, η-expansion doesn't mean anything for this example.

² It would be a full adequacy theorem if I'd shown that the bijection was compositional - that substitution on the de Bruijn terms means the same thing as substitution that LF gives us for free - but I didn't prove that part. Perhaps I should.

Request for Typestate, Part 2: Linear Types, Now!

Part 2 in a series. Part 1 began with a discussion hypothetical discussion of a ML-like language with linear types.

So in my previous post, I used the REPL loop of an "Imaginary Future Linear ML." In the following month, I've learned that there are no less than three different proposals of Imaginary Future Linear ML. Two of them, Alms and LinearML, are implemented systems that you can presumably download and run onto the device that you're using to read this very blog post!¹ The third, F-Pop by Mazurak et al, is, I believe, less seriously implemented but is formalized in Coq (which is also awesome: three cheers for mechanized metatheory!).

I was actually pleased with how much I "guessed correctly" in my discussion. For instance, Alms is a serious implementation of a language with affine, not linear, types: if you recall, affine functions can't use their arguments twice, but they can avoid using them at all. One argument from the Alms designers, which I had not considered, is that requiring a linear type discipline - where all variables get used exactly once along every "control path" - can make it rather difficult to work with handled exceptions.

Another thing that I "guessed" was in Take 3, when I suggested that we might want some syntactic sugar to make code look more like "methods" - the print method takes a string and a linear reference to a string and returns a new linear reference to that string, so why don't we have syntax that supports writing (print "Hello World" outstream) instead of (let outstream = print "Hello World" outstream). The F-Pop paper explicitly discusses this kind of notation in Section 5.2. I like that this is something they considered, though I'm still a little unsure how I feel about it "in practice." What it's doing is capturing a common intuition, that an argument, passed by reference, is both an input and an output. But how much of this intuition is fundamental, and how much is it based on path dependence - we happened to start out with languages like C and Java that force functions to have only one "official" output, so are we just used to being forced into using this unnatural design pattern?

¹ Caveat 1: well, as long as you're not using iOS. (I just got an iPad. I am not proud of this but yes, it is shiny.) Caveat 2: I couldn't get either Alms or LinearML to run on my laptop.

Request for Typestate, Part 1

Part 1 of a series. If you're interested in Imaginary Future ML, a number of proposals exist: see Part 2.

Recently I have been trying to understand typestate, since a lot of my friends, hallmates, and fellow distance runners have written implementations, papers, Ph.D. theses, and SIGBOVIK presentations on the topic. A conversation with Ron Garcia helped me get the first idea of what is going on and how it relates to linear type systems, a topic I do feel like I understand.

Some background, as I understand it. The word "typestate" was introduced by Strom and Yemini way back a long time ago in 1984 in a paper entitled "Typestate: A Programming Language Concept for Enhancing Software Reliability" (Jonathan Aldritch has posted the PDF here). It was an attempt to capture the fact that function calls often have a "do this, then do that, then don't do that anymore" kind of flavor. The most obvious and simple example is one that most every programmer has encountered, thanks to C's ubiquity:



In other words, we create a pointer by mallocing it, and then we can use that pointer as long as we want to, but if we free it we can't use that pointer anymore. (Well, we can, but we're not supposed to, C sucks, whatever.) Okay, but now you're scratching your head thinking that this is basically why modern humans use garbage collection. Well, sure, but while this solves a particular problem, the problem is really a pattern of problems, and the pattern just re-asserts itself in different ways. For instance, take this interaction with SML/NJ's toplevel:

  $ sml
  Standard ML of New Jersey v110.70 [built: Wed Jun 17 16:24:00 2009]
  - val FILE = TextIO.openOut("foo.txt");
  val FILE = - : TextIO.outstream
  - TextIO.output(FILE, "Hello world\n");
  val it = () : unit
  - TextIO.closeOut(FILE);
  val it = () : unit
  - TextIO.output(FILE, "I've got a bad feeling about this\n");

  uncaught exception Io [Io: output failed on "foo.txt", closed stream]
    raised at: Basis/Implementation/IO/text-io-fn.sml:443.14-443.56

What's happened here is that we've run afoul of exactly the same pattern that we know from C.



Because we're in a safe language, the results are less dire; a dynamic exception gets thrown rather than memory being silently corrupted. However, the problem remains: it seems like this is the sort of thing we should be able to statically preclude (using a type system), or at least warn programmers about ahead of time (using a static analysis).

Typestate-oriented programming

Both of these approaches (type systems and static analyses) have been investigated thoroughly by my friends in Jonathan Aldrich's group, such as Kevin Bierhoff, Nels Beckman, Ciera Jaspan, Karl Naden, Roger Wolff, and Ron Garcia. The following example is a way of taking that doomed ML snippet above and making it a piece of typestate-checked code; it's mostly copied from Typestate Oriented Programming by Jonathan Aldrich, Joshua Sunshine, Darpan Saini, and Zachary Sparks and was presented at ONWARD 2009.

  state File {
    public final String filename;
  }

  state OpenFile extends File {
    private CFilePtr filePtr;
    public void write(str : String) { ... }
    public void close() [OpenFile>>ClosedFile]
    { ... }
  }

  state ClosedFile extends File {
    public void open() [ClosedFile>>OpenFile]
  }

The idea here is that a File is a file that might be open or closed; you can only read from an OpenFile, which is a subtype of File. That annotation on the close() and open() methods is telling us that those functions actually change the type of the object they're acting upon; the typesystem has to work accordingly to make sure you only close or read from an OpenFile, even if though, after you close it, the object has "become" exactly the thing - a ClosedFile - that you were making sure it wasn't before.

I have some particular questions about the nature of the thing called "subtyping" in typestate oriented programming that I hope to get to in a separate post, but I hope this gives a decent overview of how typestate intuitively works even if it doesn't give much intuition as to how the typing rules "actually" work. As it turns out, the type theory behind typestate-oriented programming uses ideas from linear logic, which can also be used to directly solve the motivating problem. What I really hope to explore in this series of posts is the way in which typestate - which is mostly being investigated in object oriented settings - can (or can't) be understood as a linear type discipline in a functional programming language.

Linear Types

From a programmer's perspective, linear logic is a functional programming language where all variables only get to be mentioned once. There's an additional requirement, which is that every variable must be used once, but sometimes people ignore this requirement: the system where variables are mentioned no more than once is technically an "affine" system and not a "linear" one, but it's common to call affine systems linear anyway, because the more general term is "substructural" and "substructural" is for some reason a word that people get scared by. (This turns out to be pretty problematic for me, but that's a different blog post.)

So, nothing to be scared of, can't use variables twice. Let's see what happens with our interaction with SML:

  $ smlinear
  Imaginary Future Linear ML [built: IN THE FUTURE]
  - val FILE = TextIO.openOut("foo.txt");
  val FILE = - : TextIO.outstream
  - TextIO.output(FILE, "Hello world\n");
  val it = () : unit
  - TextIO.closeOut(FILE);
  stdIn:1.17-1.21 Error: unbound variable or constructor: FILE
  Variable "FILE" was previously in scope as a linear resource,
    but that resource already consumed

Oh dear, that doesn't work at all - we can't close the file or even write to it twice! This is our fault; when we ported the SML Basis Library from SML/NJ to Imaginary Future Linear ML, we needed to make some changes to the way we deal with TextIO. Here's (part of) the old signature for TextIO, with the arrows -> turned into lollipops -o to emphasize that we're in linear logic now. (Again, nothing scary, it just means that variables can only be mentioned once.)

  signature OLD_TEXT_IO = sig
    type outstream
    val openOut : string -o outstream
    val output : outstream * string -o unit
    val close : outstream -o unit
  end

This signature had just the right type when we could reuse the variable FILE that we got from openOut, but now, in Imaginary Future Linear ML, we can't.

Take 1: Restoring the old behavior

It's ridiculous, however, to make the output stream go away forever whenever we write to it! So what do we do? Well, all we need is for the functions that currently return unit to give us back a new object of type outstream, and then we can use it again!

  signature NEW_TEXT_IO_1 = sig
    type outstream
    val openOut : string -o outstream
    val output : outstream * string -o outstream
    val close : outstream -o outstream
  end

With this new signature for TextIO, we could have exactly the same (failed) interaction with the toplevel that we had before, the difference is that, now, we always bind a new variable when we run a function so that we have an outstream object to use in the future.

  $ smlinear
  Imaginary Future Linear ML [built: IN THE FUTURE]
  - val FILE1 = TextIO.openOut("foo.txt");
  val FILE1 = - : TextIO.outstream
  - val FILE2 = TextIO.output(FILE1, "Hello world\n");
  val FILE2 = - : TextIO.outstream
  - val FILE3 = TextIO.closeOut(FILE2);
  val FILE3 = - : TextIO.outstream
  - TextIO.output(FILE3, "I've got a bad feeling about this\n");

  uncaught exception Io [Io: output failed on "foo.txt", closed stream]
    raised at: Basis/Implementation/IO/text-io-fn.sml:443.14-443.56

Okay, well, why did I show an example that didn't solve the problem at all? Because it's important to realize that we haven't really lost any expressiveness in the language: even though we have a more restrictive system that prevents us from using variables twice, we can still express most of the things we could before.

(Side note: in the case of the strictly-linear variant of Gödel’s System T, it's actually been proven that we lose exactly nothing in terms of mathematical expressiveness by using the more restrictive type system, which is neat.)

Take 2: Actually fixing the problem

So, intuitively, we know what to do here: once we've closed an outstream we shouldn't be able to re-close it or output to it. The easiest solution is to make the function close have the type outstream -o unit - that way, closing an outstream consumes the variable representing the output stream and leaves us with no way to even mention it.

  signature NEW_TEXT_IO_1 = sig
    type outstream
    val openOut : string -o outstream
    val output : outstream * string -o outstream
    val close : outstream -o unit
  end

This suffices to turn our original dynamic exception into a static type error like the Variable...already consumed error I made up earlier.

Take 3: Matching the typestate example

For the sake of completeness, let's think about how our example looks different from the typestate example. The big difference is that all the functions in the typestate example are void: they don't output anything, they just change the type of their argument. But I believe that this is actually something that it would be reasonable to mimic in a linear system like "Imaginary Future Linear ML." The first step is to say: well, when I consumed FILE there was no longer a FILE hanging around, so why don't I just reuse that variable name?

  $ smlinear
  Imaginary Future Linear ML [built: IN THE FUTURE]
  - val FILE = TextIO.openOut("foo.txt");
  val FILE = - : TextIO.outstream
  - val FILE = TextIO.output(FILE, "Hello world\n");
  val FILE = - : TextIO.outstream
  - val FILE = TextIO.closeOut(FILE);
  val FILE = - : TextIO.outstream
  - TextIO.output(FILE, "I've got a bad feeling about this\n");
  stdIn:1.17-1.21 Error: unbound variable or constructor: FILE
  Variable "FILE" was previously in scope as a linear resource,
    but that resource already consumed

The second step is to consider that the typestate-oriented examples really do have "outputs" - their outputs are the new states of the this object. This would be easy syntactic sugar to whip up, just let val output : [outOpen >> outOpen] * string -o unit mean val output : outOpen * string -o outOpen and give the following signature

  signature NEW_TEXT_IO_2 = sig
    openOut : string -o outOpen
    output : [outOpen >> outOpen] * string -o unit
    closeOut : [outOpen >> outClosed] -o unit
    reopenOut : [outClosed >> outOpen] -o unit
  end

With this use of syntactic sugar, we could support the following interaction with our pretend ML:

  $ smlinear
  Imaginary Future Linear ML [built: IN THE FUTURE]
  - val FILE = TextIO.openOut("foo.txt");
  val FILE = - : TextIO.outOpen
  - TextIO.output(FILE, "Hello world\n");
  val it = () : unit
  - TextIO.closeOut(FILE);
  val it = () : unit
  - TextIO.output(FILE, "I've got a bad feeling about this\n");
  stdIn:6.1-6.59 Error: operator and operand don't agree [tycon mismatch]
    operator domain: TextIO.openOut * string
    operand:         TextIO.closeOut * string
    in expression:
      TextIO.output (FILE,"I've got a bad feeling about this\n")

I think that's pretty nice.

Conclusion

I think the lesson of this first discussion is that, when relating linear functional programming languages to imperative programming languages, it's useful to think of object passed to functions as being "lost" to that function and then automatically "re-bound" with the same name when the function returns. Once we make this step, the notion that the re-bound variable can have a different type - which is one key insight of typestate-oriented programming - seems quite natural.

It's important to note that none of the stuff I said about linearity and state is at all novel; for further reading see Wadler's paper Linear Types Can Change The World! (warning: .ps) or David Walker's chapter "Substructural Type Systems" in Advanced Topics in Types and Programming Languages. Those two sources just about cover the background reading; if anyone has other suggestions please feel free to put them in the comments.