The Geometry of Interaction, as an OCaml program

In this post, I'll show how to turn the Geometry of Interaction construction --- a model of linear logic --- into a runnable Ocaml code. . The basic idea behind this paper is that we can view higher-order behavior, as a disciplined mode of use of a first-order language with recursion --- basically, if you fix a calling convention, then you can compile first-class functions directly and compositionally into a first-order program.

This is interesting because there are a lot of combinator libraries out there which can be seen as DSLs with a natural notion of "first-order program", but which lack a good notion of "higher-order program". (For example, most Haskell libraries based on arrows qualify.) As a programming model, this is very unsatisfying, since this restriction basically says that the author of the library can build interesting abstractions, but clients of the library can't. Wouldn't it be nice if there were a systematic way to turn any first-order language (with a bit of structure) into a higher-order one?

That's exactly what the G construction (also called the Int construction) does. It says that if you have a first-order language with sequential and parallel composition, plus feedback, then you've really got a higher-order language. Stated more formally, in categorical jargon, it says that there is a way of constructing a monoidal closed category from any symmetric monoidal category with a trace operator. (Monoidal products mean parallel composition, categories give you sequential composition, and trace is how category theorists pronounce recursion.)

Instead of giving the categorical derivation, I'll work very concretely, following the same example Abramsky gave in his classic paper Retracing Some Paths in Process Algebra.

First, let's get some Ocaml preliminaries out of the way. I'm just defining function composition and empty and sum types, and their operations. These should really be in the Ocaml Pervasives environment, but they aren't. The Haskell prelude is nicer in this regard.

let ($) f g x = f (g x)

type ('a,'b) sum = Inl of 'a | Inr of 'b
let inl x = Inl x
let inr y = Inr y
let case f g = function Inl x -> f x | Inr y -> g y
let sum f g = case (inl $ f) (inr $ g)
let swap v = case inr inl v 

type zero = Void of zero
let rec abort (Void v) = abort v

Our running example will come from dataflow and visual programming languages like Simulink. These languages have a model of programming in which you have a bunch of stateful components (adders, multipliers, accumulators), which are connected together by means of wires. This is naturally a first-order formalism, in that it really only makes sense to send data over the wires --- you can't send components over the wire. One way of modeling these kinds of stateful components is by means of resumptions.

A resumption from $I$ (read "input") to $O$ (read "output") is essentially an element of the solution to the domain equation $R = I \to (O \times R)$. You can think of a gadget of this type as something which takes an input, and then gives you an output, plus a new resumption to use on the next input. So it's a bit like a state machine, but formulated in such a way that you don't have to give an explicit state set. It's easy to turn this domain equation into a recursive ML type:

module Resumption =
struct 

  type ('i,'o) r = R of ('i -> 'o * ('i,'o) r)

The identity resumption just echoes its input as its output.

  (* val id : ('a, 'a) r *)
  let rec id = R(fun x -> (x, id))

To compose two resumptions $f$ and $g$, we just feed an input into $f$, and take $f$'s output as the input into $g$.

  (* val ( >> ) : ('a, 'b) r -> ('b, 'c) r -> ('a, 'c) r *)
  let rec (>>) (R f) (R g) = R(fun x ->
    let (y, f') = f x in
    let (z, g') = g y in
    (z, f' >> g'))

Note that with composition, we have a category $R$, the category of resumptions. The objects are types, a morphisms $f : I \to O$ is a resumption taking $I$ inputs and producing $O$ outputs.

This category is also "monoidal closed", with the tensor product $A \otimes C$ getting defined as the sum type $A + C$. The intuition is that if we think of $A$ and $C$ as message types, we may want to consider how to react to $A$ and $C$ messages simultaneously. In particular, if we have two machines $f : A \to B$ and $g : C \to D$, we can combine them by taking an $A+C$ message and dispatching to either $f$ or $g$ respectively.

  (* val ( ** ) : ('a, 'b) r -> ('c, 'd) r -> (('a, 'c) sum, ('b, 'd) sum) r *)
  let rec ( ** ) (R f) (R g) = R(function
    | Inl x -> let (y, f') = f x in (inl y, f' ** (R g))
    | Inr x -> let (y, g') = g x in (inr y, (R f) ** g'))

We can also implement feedback --- if we have an $f : A \otimes B \to C \otimes B$, then we can construct a map $A \to C$ by feeding $f$ the $A$, and repeatedly sending the output back into the input until $f$ coughs up a $C$ rather than a $B$:

  (* val trace : (('a, 'b) sum, ('c, 'b) sum) r -> ('a, 'c) r *)
  let rec trace f = R(fun a ->
    let rec loop (R f) v =
      match f v with
      | (Inl c, f') -> (c, trace f')
      | (Inr b, f') -> loop f' (inr b)
    in
    loop f (inl a))

Now, we can also implement various associativity and commutativity properties. The names are not particularly great (they are just the standard names for the natural transformations associated with a tensor product in category theory), but all the real action is in the types.

  (* val sym : (('a, 'b) sum, ('b, 'a) sum) r *)
  let rec sym = R(fun v -> (swap v, sym))
  
  (* val rho : (('a, zero) sum, 'a) r *)
  let rec rho : (('a,zero) sum, 'a) r = R(function
    | Inl a -> (a, rho)
    | Inr z -> abort z)

  (* val rho' : ('a, ('a, zero) sum) r *)
  let rec rho' : ('a, ('a, zero) sum) r = R(fun a -> (inl a, rho'))

  (* val lambda : ((zero, 'a) sum, 'a) r *)
  let rec lambda : ((zero,'a) sum, 'a) r = R(function
    | Inl z -> abort z
    | Inr a -> (a, lambda))

  (* val lambda' : ('a, (zero, 'a) sum) r *)
  let rec lambda' : ('a, (zero, 'a) sum) r = R(fun a -> (inr a, lambda'))

  (* val alpha : ((('a, 'b) sum, 'c) sum, ('a, ('b, 'c) sum) sum) r *)
  let rec alpha : ((('a,'b) sum, 'c) sum, ('a, ('b,'c) sum) sum) r = R(function
    | Inl (Inl a) -> (inl a, alpha)
    | Inl (Inr b) -> (inr (inl b), alpha)
    | Inr c       -> (inr (inr c), alpha))
 
  (* val alpha' : (('a, ('b, 'c) sum) sum, (('a, 'b) sum, 'c) sum) r *)
  let rec alpha' : (('a, ('b,'c) sum) sum, (('a,'b) sum, 'c) sum) r = R(function
    | Inl a       -> (inl (inl a), alpha')
    | Inr (Inl b) -> (inl (inr b), alpha')
    | Inr (Inr c) -> (inr c, alpha'))
end 

Now, we give the G construction in terms of the resumption module we've just defined. In the G construction, we build a new category $G(R)$ from the old one we've just defined. The basic idea here is to talk about bidirectional communication, and so for objects in our new category $G$ will be pairs of objects from our old one.

Objects of $G$ will be pairs $(A^+, A^-)$, where you can think of $A^+$ as a type of messages sent out, and the type $A^-$ as the type of messages that are accepted.

A morphisms of $G$, $f : (A^+,A^-) \to (B^+, B^-)$ will be resumption of type $A^+ \otimes B^- \to A^- \otimes B^+$. Note that the polarities of $A$ and $B$ are flipped in this mapping -- we are transforming $A$ messages out to $B$ messages out, and we need to accept $B$ messages in order to transform them into $A$ messages in.

module G =
struct
  open Resumption

Now, let's define the type of morphisms in $G(R)$. Since we don't have type-level pairing in ML, we end up having four type parameters. We use a dummy G constructor to get the type system to produce more useful inferred types.

  type ('aplus, 'aminus, 'bplus, 'bminus) map =
      G of (('aplus, 'bminus) sum, ('aminus, 'bplus) sum) r

The identity map in $G(R)$ is just the symmetry map in $R$.

  let gid = G sym 

Composition is trickier. If we have a map $f : (A^+,A^-) \to (B^+, B^-)$ and $g : (B^+,B^-) \to (C^+,C^-)$, we can compose it by feeding $f$'s $B$-output into $g$'s input, and vice-versa, using the trace operator. It's best visualized with the following diagram:

Actually doing so requires applying the associativity and commutativity properties of sum types $A + B \simeq B + A$ and $(A + B) + C \simeq A + (B + C)$.

  let rec assoc : ((('aplus,'cminus) sum, ('bminus,'bplus) sum) sum,
                  (('aplus, 'bminus) sum, ('bplus, 'cminus) sum) sum) r =
    R(function
      | Inl (Inl aplus)  -> (inl (inl aplus), assoc)
      | Inl (Inr cminus) -> (inr (inr cminus), assoc)
      | Inr (Inl bminus) -> (inl (inr bminus), assoc)
      | Inr (Inr bplus)  -> (inr (inl bplus), assoc))

  let rec assoc2 : ((('aminus, 'bplus) sum, ('bminus, 'cplus) sum) sum,
                   (('aminus, 'cplus) sum, ('bminus, 'bplus) sum) sum) r  =
    R(function
      | Inl (Inl aminus) -> (inl (inl aminus), assoc2)
      | Inr (Inr cplus)  -> (inl (inr cplus), assoc2)
      | Inl (Inr bplus)  -> (inr (inr bplus), assoc2)
      | Inr (Inl bminus) -> (inr (inl bminus), assoc2))

  (* val gcompose :
      ('a, 'b, 'c, 'd) map -> ('c, 'd, 'e, 'f) map -> ('a, 'b, 'e, 'f) map *)
  let gcompose (G f) (G g) = G (trace (assoc >> (f ** g) >> assoc2))

Once we have composition, we can define a tensor product on the $G(R)$ category as well, so that $(A^+,A^-) \oplus (B^+,B^-) = (A^+ + B^+, A^- + B^-)$. Again, implementing the functorial action requires implementing the associativity maps.

  (* (A+, A-) * (X+, X-) = (A+ + X+, A- + A-) 
     f : A+ + B- -> A- + B+
     g : X+ + Y- -> X- + Y+
     f ** g : (A+ + B-) + (X+ + Y-) -> (A- + B+) + (X- + Y+)
     r  : (A+ + X+) + (B- + Y-) -> (A+ + B-) + (X+ + Y-)
     r' : (A- + B+) + (X- + Y+) -> (A- + X-) + (B+ + Y+)

  *)

  (* val ( + ) :
      ('a, 'b, 'c, 'd) map ->
      ('e, 'f, 'g, 'h) map ->
      (('a, 'e) sum, ('b, 'f) sum, ('c, 'g) sum, ('d, 'h) sum) map *)
  let (+) (G f) (G g) =
    let rec r = R(function
      | Inl (Inl aplus)  -> (inl (inl aplus), r)
      | Inl (Inr xplus)  -> (inr (inl xplus), r)
      | Inr (Inl bminus) -> (inl (inr bminus), r)
      | Inr (Inr yminus) -> (inr (inr yminus), r))
    in
    let rec r' = R(function
      | Inl (Inl aminus) -> (inl (inl aminus), r')
      | Inl (Inr bplus)  -> (inr (inl bplus),  r')
      | Inr (Inl xminus) -> (inl (inr xminus), r')
      | Inr (Inr yplus)  -> (inr (inr yplus),  r'))
    in
    G (r >> f ** g >> r')

One cool thing about this category (which leads to the coolest fact about it) is that it naturally supports a dualization, which sends $(A^+,A^-)^\ast \triangleq (A^-,A^+)$. This also has an action on morphisms, which flips around the direction, so that from $f : (A^+,A^-) \to (B^+,B^-)$ we can get $f^\ast : (B^+,B^-)^\ast \to (A^+,A^-)^\ast$.

  (* val dualize : ('a, 'b, 'c, 'd) map -> ('d, 'c, 'b, 'a) map *)
  let dualize (G (R f)) =
    let rec dual f = R(fun v ->
      let (v', f') = f (swap v) in
      (swap v', dual f))
    in
    G (dual f)

Now, here's what I consider the neatest fact about the Int construction -- it turns a traced monoidal category into a monoidal closed category. So we can define the linear exponential $(A^+,A^-) \multimap (B^+,B^-) \triangleq (A^+,A^-)^\ast \otimes (B^+,B^-)$.

 (* Here's a bit of unrolling type definitions to make things easier to grok. 

    (A+, A-) -o (B+, B-) = (A+, A-)* * (B+, B-)
                         = (A-, A+) * (B+, B-)
                         = (A- + B+, A+ + B-)
    
    Hom((A+,A-) * (B+,B-), (C+, C-)) 
        = Hom((A+ + B+, A- + B-), (C+, C-))
        = ((A+, B+) sum, (A- + B-) sum, C+, C-) map 
        = (((A+, B+) sum, C+) sum, ((A- + B-) sum, C-) sum) r

    Hom((A+,A-), (B+,B-) -o (C+,C-)) 
        = Hom((A+,A-), (B- + C+, B+ + C-))
        = (A+, A-, (B-, C+) sum, (B+, C-) sum) map 
        = ((A+, (B+, C-) sum) sum, (A-, (B-, C+) sum) sum) r 
 *)

  (* val curry :
      (('a, 'b) sum, ('c, 'd) sum, 'e, 'f) map ->
      ('a, 'c, ('d, 'e) sum, ('b, 'f) sum) map *)
  let curry (G f) =
    let rec curry (R f) = R(fun v ->
      let (v', f') = f (case (inl $ inl) (case (inl $ inr) inr) v) in
      let v'' = case (case inl (inr $ inl)) (inr $ inr) v' in
      (v'', curry f'))
    in
    G(curry f)

  (* val uncurry :
      ('a, 'b, ('c, 'd) sum, ('e, 'f) sum) map ->
      (('a, 'e) sum, ('b, 'c) sum, 'd, 'f) map *)
  let uncurry (G f) =
    let rec uncurry (R f) = R(fun v ->
      let (v', f') = f (case (case inl (inr $ inl)) (inr $ inr) v) in
      let v'' = case (inl $ inl) (case (inl $ inr) inr) v' in
      (v'', uncurry f'))
    in
    G (uncurry f)
end

The ML types for curry and uncurry somewhat obscure the fact that they implement the isomorphism $$\mathrm{Hom}((A^+,A^-) \otimes (B^+,B^-), (C^+,C^-)) \simeq \mathrm{Hom}((A^+,A^-), (B^+,B^-) \multimap (C^+,C^-))$$

However, now that we have this isomorphism, it's possible to compile arbitrary lambda-terms in multiplicative linear logic down into compositions of resumptions. But that's a story for another post!

In the meantime, if this intrigues you, you can play with the Verity compiler by Dan Ghica and his students, as well as the IntML compiler by Ulrich Schöpp and Ugo Dal Lago, both of which are compilers using the GoI interpretation. Verity is aimed at distributed computing, and IntML is a programming language whose type system allows you to write only (and all) the LOGSPACE programs. As you can see, there are a lot of potential applications...

Polymorphism and limit-colimit coincidence in reactive languages

In my previous post, I mentioned limit-colimit coincidence, and how the ability to define fixed points makes that possible. It turns out there's a very pretty way of using parametricity to encode this. Now, inductive and coinductive types are definable in System F as follows:

μα. F(α) = ∀α. (F(α) → α) → α
νβ. F(β) = ∃β. β × (β → F(β))

It's possible to show using parametricity that these type definitions are actually the inductive and coinductive types we expect, whenever F is a positive type. That is, a type constructor F is positive whenever we have a function:

  map : ∀α,β. (α → β) → F(α) → F(β)

with the expected properties that:

1. map [A] [A] id = id
2. (map [A] [B] f); (map [B] [C] g) = map [A] [C] (f; g)

In lattice theory, you can apply the Knaster-Tarski theorem to get a fixed point of a function f : L → L when L is a complete lattice and f is monotone. Intuitively, you can see map as the proof that the functor F is monotone (really, functorial) in the lattice (really, category) of types.

It turns out that in a temporal setting, we also need to specify that we can invoke the algebra/coalgebra operations at multiple times, which we can specify using the modal stability connective □A, which changes the definitions to:

μα. F(α) = ∀α. □(F(α) → α) → α
νβ. F(β) = ∃β. β × □(β → F(β))

Now, suppose we have a Nakano style recursive type μ̂α.F(•α), where every occurrence of the recursive type occurs beneath a delay modality. Then, assuming that F is positive, we can show how to embed elements of νβ. F(•β) into elements of μα. F(•α) as follows:

embed : να. F(a) → μα. F(α)
embed pack(β, (seed, h₁)) =           // seed : β, h₁ : □(β → F(•β))
  let stable(f) = h₁ in               // f : β → F(•β) at all times
  Λα. λh₂.                            // h₂ : □(F(•α) → α)
    let stable(g) = h₂ in             // g : F(•α) → α at all times
    let loop : β → α = 
      fix loop = λb:β.               // in body, loop can only be used later
        g(map [•α] 
              [•β] 
              (λd:•β. let •b' = d in •(loop b'))    // has type •β → •α
              (f b))                                // has type F(•β)
    in
    loop seed 

This suggests that guarded term-level recursion is enough to make certain least and greatest fixed points collapse. I say "suggests", since proving that these types are equivalent requires a parametric model, which I haven't actually constructed yet. It also means that just polymorphism and the stability modality □A are enough to construct an interesting reactive language, even without a term-level fixed point fix x. e.

This function, minus the temporal staging, should also work for F plus ordinary general recursion. I had just never thought about how the coincidence plays out syntactically when you don't take recursive types as a primitive!

When it rains, it pours

Having written a new paper on FRP of my own, I've just discovered that lots of other people have been hard at work in this area.

• Alan Jeffrey has a new paper for PLPV 2013, entitled Causality For Free!: Parametricity Implies Causality for Functional Reactive Programs.

  This looks very interesting, since it looks like he's found a different way of enforcing causality than the one Nick and I hit on. We formalized the order structure of time (this happens before that), and required functions to respect that order. Alan has a discrete model of time (i.e., he doesn't bake temporal order into his category of times), and instead he uses parametricity to prove that all the definable functions (of the appropriate type) are inherently causal.

• Wolfgang Jeltsch also has a new paper for PLPV 2013, entitled Temporal Logic with “Until”, Functional Reactive Programming with Processes, and Concrete Process Categories.

  He's also been looking at using full temporal logic for typing reactive programs. This paper looks especially focused on the distinction between strong (must eventually happen) and weak eventually (may eventually happen) operators.

• Brigitte Pientka visited us here at MPI last week, and she told me about some work that some of her students (Francisco Ferreira and someone whose name I unfortunately cannot recall -- Andrew Cave?) have been doing with her and Prakash Panangaden, on giving a proof theory for the modal mu-calculus. At a high level, their calculus looks very similar to the system I just wrote up, but there are some very intriguing semantic differences.

  I use a Nakano-style guarded recursive type, which allows negative occurences. This permits defining general fixed points $(\bullet{A} \to A) \to A$, which collapses greatest and least fixed points. They use strict positivity instead, and so they can distinguish them, at the cost of more restrictive typing of recursive definitions. (This ties into Jeltsch's work on strong/weak eventually, which correspond to inductive versus coinductive definitions of the eventually type.)

  Limit-colimit coincidence is one of the most striking features of categories of pointed domains, and it's (a) interesting that it can be induced already with guarded recursion, and (b) it might be easier to study in this setting.

• Marc Bagnol and Adrien Guatto have written a draft paper, Synchronous Machines: a Traced Category.

  The basic idea, roughly speaking, is to start with Mealy automata as a model of reactive programs. These automata lack a notion of higher-order behavior, but if you hit them with the Geometry of Interaction construction, you can get out a higher-order (linearly-typed) programming language, which is still implementable with finite state. This is a very nice idea, and reminiscent of Dan Ghica's work on synthesizing circuits.

New Draft: Simple and Efficient Higher-Order Reactive Programming

I've got a new draft out Simple and Efficient Higher-Order Reactive Programming. Here's the abstract:

Functional reactive programming (FRP) is an elegant approach to declaratively specify reactive systems. However, the powerful abstractions of FRP have historically made it difficult to predict and control the resource usage of programs written in this style.

In this paper we give a simple type theory for higher-order functional reactive programming, as well as a natural implementation strategy for it. Our type theory simplifies and generalizes prior type systems for reactive programming. At the same time, we give a an efficient implementation strategy which eagerly deallocates old values, ruling out space and time leaks, two notorious sources of inefficiency in reactive programs. Our language neither restricts the expressive power of the FRP model, nor does it require a complex substructural type system to track the resource usage of programs.

We also show that for programs well-typed under our type system, our implementation strategy of eager deallocation is safe: we show the soundness of our type system under our implementation strategy, using a novel step-indexed Kripke logical relation.

Last year, Nick Benton, Jan Hoffmann, and I worked out how to control the space usage of FRP programs. Our techniques worked, but it required a rather complicated linear type discipline to make everything work. In this paper, I've worked out how to dramatically simplify the type system, make the language more expressive, use simpler implementation strategies, which also make it more efficient.

This is also basically the implementation strategy I am using in my AdjS compiler, which should see a release as soon as I add support for a few more type system features, and squash the soundness bugs the correctness proof in this paper revealed.