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