What does focusing tell us about language design?

This post is largely based on some conversations I've had about Polarized Logic/Focusing/Call-By-Push-Value recently, especially with Neel Krishnaswami and Wes Filardo, though it was originally prompted by Manuel Simoni some time ago.

I think that one of the key observations of focusing/CBPV is that programs are dealing with two different things - data and computation - and that we tend to get the most tripped up when we confuse the two.

• Data is classified by data types (a.k.a. positive types). Data is defined by how it is constructed, and the way you use data is by pattern-matching against it.
• Computation is classified by computation types (a.k.a. negative types). Computations are defined their eliminations - that is, by how they respond to signals/messages/pokes/arguments.

There are two things I want to talk about, and they're both recursive types: call-by-push-value has positive recursive types (which have the feel of inductive types and/or algebras and/or what we're used to as datatypes in functional languages) and negative recursive types (which have the feel of recursive, lazy records and/or "codata" whatever that is and/or coalgebras and/or what William Cook calls objects). Both positive and negative recursive types are treated by Paul Blain Levy in his thesis (section 5.3.2) and in the Call-By-Push Value book (section 4.2.2).

In particular, I want to claim that Call-By-Push-Value and focusing suggest two fundamental features that should be, and generally aren't (at least simultaneously) in modern programming languages:

1. Support for structured data with rich case analysis facilities (up to and beyond what are called views)
2. Support for recursive records and negative recursive types.

Minor addition to "core Levy"

I'll be presenting with an imaginary extension to Bauer's Levy language in this post.¹ I've mucked around Levy before, of course, and it would probably help to review that previous post before reading this one. I want to make one addition to Levy before we begin making big, interesting ones. The derived form that I want to add - e1 orelse e2 - is computation code with type F bool if e1 and e1 have type F bool as well. This is definable as syntactic sugar, where x is selected to not be free in e2:

   e1 to x in 
   if x then return true 
   else e2

One other aside - do remember that, at the cost of potential confusion, I modified Bauer's original Levy implementation to make force a prefix operator that binds more tightly than application - force g z y can be written with parentheses as (((force g) z) y).

Positive types, positive recursive types

The functional languages have the construction of positive types just about right: they're made up of sums and products. I used a special LLF-ish construction for datatypes in my exploration of Levy#, but the more traditional way of introducing datatypes is to say that they are recursive types μt.T(t). The recursive types we're used to thinking about are naturally interpreted as positive types, because they are data and are inspected by pattern matching.

There's a tendency in programming language design to shove positive recursive types together with labeled sum types to get a familiar datatype mechanism.² I will go along with this tendency and merge labeled sums and recursive types, writing them as μt.[L1: T1(t), L2: T2(t), ..., Ln: Tn(t)].

Here are datatype definitions for trees of ints and lists of ints:

   type+ tree = 
   μtree. 
   [ Leaf: int, 
     Node: tree * tree ]

   type+ list = 
   μlist. 
   [ Nil, 
     Cons: int * list ]

Note from the definition of lists that we also allow types to have no arguments: it's possible to treat the definition of Nil as syntactic sugar for Nil: unit. The associated value is Nil, which is syntactic sugar for Nil ().

There are infinitely many trees and lists as we've defined them. In fact, it's just a convention of how we have to write programs that we think of positive types as being finite sums. Even though we can't write it down as a datatype declaration, it's perfectly reasonable to think of a built-in type of infinite precision integers as being defined as follows:

   type+ int = 
   μint. 
   [ 0, 
     1,
     ~1,
     2,
     ~2,
     3,
     ... ]

The same goes for built-in strings and the like - think of built-in types being positive enumerations that were provided specially by the language since the language didn't give us the ability to write down the full declaration containing all possible constants.

Powerful views

A point that has not, in my humble opinion, been made simply enough is that the perspective of focusing says that we should think about integrating much more powerful case analysis mechanisms into our programming languages. I learned about this point from Licata, Zeilberger, and Harper's 2008 Focusing on Binding and Computation, but their setting had enough other interesting stuff going on that it probably obscured this simple point.

Standard ML (and, to the best of my knowledge, all other functional languages circa-1997) only provides a limited form of case analysis - arbitrary finite views into the outermost structure of the datatype:

   case x of
    | Leaf 9 => ...
    | Leaf y => ...
    | Node (Node (Leaf 5, y), z) => ...
    | Node (y, z) => ...

This limitation comes with a nice tradeoff, in that we can pretty effectively estimate how much work compiled code needs to do to handle a pattern match. However, the structure of focusing suggests that any mathematical function from a value's structure to computation is fair game. One well-studied modernization of pattern matching is views, which allows us to group computations in other ways. One use case would be allowing us to take an integer variable x and say that it is even or odd:

   case x of
    | 0 => return true
    | x is even => return false
    | ~1 => return false
    | x is odd => return true

The focusing-aware view of pattern matching suggests that what a pattern match is actually doing is defining a case individually for each value structure - if we could write a countably-infinite-sized program, then we could expand the view-based program above to the no-longer-view-based, but infinitely long, program below:

   case x of
    | 0 => return true
    | 1 => return true
    | ~1 => return false
    | 2 => return false
    | ~2 => return false
    | 3 => return true
    | ...

So: the focusing perspective says that any effect-free (effects include nontermination!) mathematical function we can write from value structure to computations is fair game for case analysis; views are just one known way of doing this in an interesting way. In principle, however, we can consider much richer case-analysis machinery to be fair game. For instance, there is a mathematical function \(f\) from integer values int to computation code of type F bool with the variable coll free:

• If the integer is 1, the result is return true
• If the integer is less than 1, the result is return false
• Otherwise, if the integer is divisible by 2 and the result of dividing the integer by 2 is i, then the result is force coll i
• Otherwise, let j be 3 times the integer, plus one. Then the result is force coll j

Given this mathematical function, we have the core case analysis at the heart of the Collatz function. If we expand out this case analysis into an infinitely-long mapping as before, it would look like this:

   rec coll: int -> F bool is
     fn x: int =>
       case x of
        | 0 => return false
        | 1 => return true
        | ~1 => return false
        | 2 => force coll 1
        | ~2 => return false
        | 3 => force coll 10
        | ~3 => return false
        | 4 => force coll 2
        | ~4 => return false
        | 5 => force coll 16
        | ...

The important question here is: what is the right way to think about how we write down total functions from value structures? Are views about right, or do we need something different, clearer/more/less powerful? I don't have a sense for the answers, but I'm pretty confident that's the right question.

Views are only over the structure of values

One critical caveat: I used the phrase value structure in the previous discussion repeatedly on purpose. Because computations can always contain effects, we cannot poke at the computations at all when we think about views - the value structure is just the part of the value that we can inspect without traversing a thunk. Therefore, if we have this definition...

   type+ somefn = 
   μsomefn. 
   [ BoolFn: U (bool -> F bool), 
     IntFn: U (int -> F int) ]

...then a case analysis on a value of type somefn can have at most two branches - one for the BoolFn case and one for the IntFn case. We can't pattern-match into computations, so even though it would be reasonable to say that there are many, many values of type somefn, there are only two value structures that can be inspected by case analysis.

Negative types, negative recursive types

In call-by-push-value, the computation types (a.k.a. the negative types of polarized logic/focusing) are defined by the way we use them. Computation code of computation type does stuff in response to being used - a function does stuff in response to getting an argument, and so the most well-understood negative type is implication.

Conjunction (the product or pair type) is a bit slippery, says the CBPV/focusing methodology. We've already used conjunction as a positive type (t1 * t2), but we can also think of conjunction as being a negative type. This is because it's equally valid to think of a pair being positively defined by its construction (give me two values, that's a pair) and negatively as a suspended computation that awaits you asking it for its first or second component.

CPBV/focusing makes us choose: we can have either type of conjunction, or we can have both of them, but they are different. It will be convenient if we keep the normal tuples as positive types, and associate negative types with records - that is, with named products. Records are defined by how you project from them, and just as we tie labeled sums in with positive recursive types, we'll tie labeled products in with negative recursive types.

Negative recursive types are naturally codata in the same way that positive recursive types are naturally data: the canonical example is the infinite stream.

   type- stream = 
   μstream. 
   { head: F int, 
     tail: stream }

It's natural to define particular streams with fixedpoints:

   val Ones = thunk rec this: stream is
   { head = return 1, 
     tail = force this }

   val CountUp = thunk rec this: int -> stream is
   fn x: int =>
   { head = return x, 
     tail = 
       force plus x 1 to y in
       force this y }

Say I wanted to get the fourth element of an infinite stream str of type U stream. The ML-ish way of projecting from records would write this as #tail (#head (#head (#head (force str)))), but I will pointedly not use that notation in favor of a different record notation: (force str).head.head.head.tail. It nests better, and works better in the case that record elements are functions. (Because functions are negative types, like records, it is very natural to have functions be the arguments to records.)

Negative recursive types as Cook's objects

Here's a bit of a case study to conclude. The entities that William Cook names "Objects" in his paper On Understanding Data Abstraction, Revisited are recognizably negative recursive types in the sense above.³ Cook's examples can be coded in Standard ML (see here), but the language gets in the way of this encoding in a number of places.⁴ To see what this would look like in a language with better support, I'll encode the examples from Cook's paper in my imaginary CBPV implementation. The recursive negative type looks much like a stream, and encodes the interface for these set objects.

   type- iset = 
   μiset. 
   { isEmpty: F bool, 
     contains: int -> F bool, 
     insert: int -> iset, 
     union: U iset -> iset }

One difficulty: the Insert and Union operations that Cook uses involve mutual recursion. I don't have mutual recursion, so rather than pretending to have it (I've abused my imaginary language extension enough already) I'll code it up using records. The record type insertunion I define isn't actually recursive, it's just a record - this is analogous to using ML's datatype mechanism (which, as we've discussed, makes positive recursive types) to define a simple enumeration.

   type- insertunion = 
   μinsertunion.
   { Insert: U iset * int -> iset,
     Union: U iset * U iset -> iset }

   val InsertUnion = thunk
     rec x: insertunion is
     { Insert = fn (s, n) =>
       (force s).contains n to b in
       if b then force s else 
       rec self: iset is
       { isEmpty = return false,
         contains = fn i => (force equal i n) orelse (force s).contains i,
         insert = fn i => (force x).Insert (self, i),
         union = fn s' => (force x).Union (self, s') },

       Union = fn (s1, s2) => 
       rec self: iset is
       { isEmpty = (force s1).isEmpty orelse (force s2).isEmpty,
         contains = fn i => (force s1).contains i orelse (force s2).contains i,
         insert = fn i => (force x).Insert (self, i),
         union = fn s' => (force x).Union (self, s') } }

   val Insert: U (U iset * int -> iset) = thunk ((force InsertUnion).Insert)

   val Union: U (U iset * U iset -> iset) = thunk ((force InsertUnion).Union)

We've defined union of sets and insertion into a set, but we haven't actually defined any sets yet! Once we give the implementation of an empty set, however, we can manipulate these sets with a Java-esque method invocation style:

   val Empty = thunk rec self: iset is
   { isEmpty = return true,
     contains = fn x => return false,
     insert = fn i => force Insert (self, i),
     union = fn s' => force s' }

   val JustOne = thunk (force Empty).insert 1
   (force Empty).insert(3).union(JustOne).insert(5).contains(4)

As Cook noted, it's also very natural to talk about infinite sets in this style, such as the set of all even numbers and the set of all integers:

   val Evens = thunk rec self: iset is 
   { isEmpty = return false,
     contains = fn i => 
       force mod i 2 to x in
       (case x of 
         | 0 => return true
         | _ => return false),
     insert = fn i => force Insert (self, i),
     union = fn s' => force Union (self, s') }

   val Full = thunk rec self: iset is
   { isEmpty = return false,
     contains = fn i => return true,
     insert = fn i => force self,
     union = fn s' => force self }

---

¹ If anyone is interested in helping me implement a toy language along these lines, I'm all ears. Also, the disclaimer that since I don't have an implementation there are surely bugs bugs bugs everywhere is strongly in effect.

² As a practical matter, this makes it easier for the language to know where to put implicit roll/unroll annotations, so that programmers doesn't have to write these explicitly, which would be a pain.

³ Cook does give the disclaimer that this definition is "recognized as valid by experts in the field, although there certainly are other valid models." I carefully call these things "Cook objects" rather than "objects" - my claim is that negative recursive types correspond to what William Cook names objects, not that they correspond to what you call objects. Note, furthermore, that I could be wrong about what William Cook calls objects! I only have his paper to go on and I have been known to be a few cookies short of a haystack.

⁴ There are two issues with the encoding in SML. The most basic is that we have to encode the recursive types using SML's recursive type mechanism, which is biased towards the positive encoding of recursive types as finite sums. The other issue is that the way SML ties together (mutual) recursion with closures gets in the way - the standard way of writing a "thunk" as a function from unit is all over the place, and it wan't possible to define EmptySet so that it was mutually recursive with the definition of Insert and Union as a result. So, I'm certainly not arguing that SML facilities programming in (what Cook calls) an object-oriented style in a strong sense - it's unnecessarily painful to code in that style - but the minimal semantic building blocks of what Cook presented and named Object are present and accounted for. [Update:] As gasche discusses in the comments, Ocaml's records, and the way it deals with laziness, make it quite a bit better at encoding the example, but it's still not ideal.

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.