Modular Interpreters with Mutually Recursive Modules?

Learning
1

I am trying to solve the following problem. I have a language which is defined using evaluation contexts. I have two different operational semantics for this language, which share their evaluation contexts (and therefore their administrative reductions) but which differ according what they consider to be a value and what their primitive reductions are.

So,

E ::= []
     | PlusL E e
     | PlusR v E
     | If E e e
     | AppL E e
     | AppR v E
     ...

(* Semantics 1 *)
Plus(n1, n2) ~> n1 + n2
If (true, e1, e2) ~> e1
If (false, e1, e2) ~> e2
...

e1 ~> e2
------------
E[e1] -> E[e2]

(* Semantics 2 *)
Plus(n1, n2) ~> n1 + n2
If (true @ public, e1, e2) ~> e1
If (false @ public, e1, e2) ~> e2
...

e1 ~> e2
------------
E[e1] -> E[e2]

Notice that Semantics 1 represents boolean values as just boolean values and Semantics 2 represents boolean values as being paired with a label. Also, the primitive reductions ~> are different.

OK. So, now I would like to program this in OCaml, but I would not like to duplicate the implementation of the administrative forms. My only guess about how to accomplish this is using two functors that are mutually recursive somehow.

(* eval.ml *)
module Make (Semantics : Primitive.S) : Eval.S = 
struct
  type v = Semantics.t
  type t = 
         | Val of v
         | Plus of t * t
         | If of t * t * t
         | App of t * t
         | Lam of string * t
         ...

  type k =
         | Hole
         | PlusL of k * t
         | PlusR of Semantics.t * k
         ...

  (* `other` contains stuff like the runtime store -- anything not relevant to administrative evaluation *) 
  type config = { expr : t ; other : Semantics.config ; cont : k }

  (* The following has a type error, because OCaml doesn't know that the `t` type
      being emitted by this functor will be equal to the `expr` type of the functor argument. *)
  let step (c : config) : config option = ... SemanticsOne.reduce e c.other ...
end

Where step above will call the primitive reduction function of the module argument, Semantics.

Each semantics has a functor, which must also be parameterized:

(* first.ml *)
module Make (Eval : Eval.S) : Primitive.S =
struct
  type e = Eval.t
  type t = ...
         | VInt of int
         | Closure of environment * string * e
         ...

  (* I can't actually do this pattern matching, since `e` is abstract. *)
  let reduce e env =
    match e with
    | Plus (Val (VInt n1), Val (VInt n2)) -> (env, Val (VInt (n1 + n2)))
    | App (Val (VClosure (env', x, body)), Val v) -> ((Env.add x v env'), body)
    ...
end

Then, you tie the knot with recursive modules somehow:

module rec EvalOne : Eval.S = Eval.Make(SemanticsOne)
       and SemanticsOne : Primitive.S = First.Make(EvalOne)

I know this is quite complicated, but here’s hoping someone has needed to do something similar before. The three major pain points are (1) splitting up mutually recursive datatypes between modules, (2) parameterizing the datatype somehow, and (3) making the datatype visible across modules (which requires type equalities).

The types obviously don’t work out, because I need some type equalities and I don’t know how to get them.

2

You can break the cycle by using parametrization in the term datatype:

type ('v, 'p) t =
  | Prim of 'p
  | Value of 'v
  | If of ('v, 'p) t * ('v, 'p) t * ('v, 'p) t
  | ...

type ('v, 'p) k = ('v, 'p) kframe list
and ('v, 'p) kframe =
  | IfK of ('v, 'p) t * ('v, 'p) t
  | ...

module Simple = struct
  type primitive = ...
  and value = ...
  and term = (primitive, value) t
end

module Labelled = struct
  type primitive = ...
  and value = Simple.value * label
  and label = ...
  and term = (value, primitive) t
end

It should also be possible to define a generic reduction function, parametrized over a head-reduction function. One possible approach would be just as a polymorphic function

type ('s, 'v, 'p) reducer = ('s * ('v, 'p) t) -> ('s * ('v, 'p) t) option
val reduce : ('s, 'v, 'p) reducer -> 's -> ('v, 'p) t -> ('v, 'p) k -> ('v, 'p) t

another is to use a functor as you suggest.

module type ReduceBase = sig
  type primitive
  type value
  type term = (primitive, value) t

  type state
  val reduce_head : state * term -> (state * term) option
end
module Reduce(Base : ReduceBase) : sig
  open Base
  type eval_ctx = (value, primitive) k
  val reduce : state -> term -> eval_ctx -> term
end
3

This looks great! Thank you.

I considered this approach for a moment early-on, but discarded it because I somehow convinced myself that the kinding wouldn’t work out (i.e. I’d need to instantiate one of the type variables with something of kind * -> *).

I now see that it isn’t necessary. The trick of placing the reducible expressions (primitive in your example above) in their own constructor of the expression type is also a nice one.

I will try this out and follow-up if I have any confusion, but I’m confident this will work!