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.