Importing mutually recursive types from OCaml to Coq

September 28, 2019

In order to make coq-of-ocaml usable on a maximum of OCaml programs, we should handle mutually recursive types. We show how we import these types to Coq and the main differences between the two languages. As a result, more OCaml programming patterns should be supported by coq-of-ocaml.

This work was financed by Nomadic Labs with the aim to verify the OCaml implementation of the Tezos blockchain.

Example

Take the following mutually recursive definition of a tree in OCaml:

type 'a tree = Tree of 'a node list

and 'a node =
  | Leaf of 'a leaf
  | Node of 'a tree

and 'content leaf = string * 'content

By applying coq-of-ocaml on this code we get:

Reserved Notation "'leaf".

Inductive tree (a : Type) : Type :=
| Tree : (list (node a)) -> tree a

with node (a : Type) : Type :=
| Leaf : ('leaf a) -> node a
| Node : (tree a) -> node a

where "'leaf" := (fun (content : Type) => string * content).

Definition leaf := 'leaf.

Arguments Tree {_}.
Arguments Leaf {_}.
Arguments Node {_}.

We transform algebraic data types to Coq’s inductive types. We use a notation to implement the type synonym leaf. This is a trick because Coq only supports inductive types in mutual definitions. See the documentation on notations for more information. We rename the leaf type parameter 'content instead of 'a to avoid a name collision in Coq. The type parameters of the constructors are set implicit with the command Arguments to keep the behavior of OCaml.

General mechanism

We handle type ... and ... definitions with algebraic data types (including GADTs, “Generalized Algebraic Data Types”) and type synonyms. We do not handle abstract types. For records in mutual definitions, one can use a type synonym to a more generic record. For example:

type expression =
  | Number of int
  | Operation of operation

and operation = {
  name : string;
  parameters : expression list }

can be rewritten as:

type 'a operation_skeleton = {
  name : string;
  parameters : 'a list }

type expression =
  | Number of int
  | Operation of operation

and operation = expression operation_skeleton

in order to be imported into Coq.

In Coq, there is a distinction between type variables on the left (type parameters) and on the right of the : (type indices):

Inductive t (A1 A2 ... : Type) : forall (B1 B2 ... : Type), Type :=
| Constr1 : ... -> t A1 A2 ... C1 C2 ...
| ...

The variables Ai do not behave the same as the variables Bi. Type parameters have the constraint of being the same for each constructor. When used, they simplify the typing of the pattern matching. Typically, in GADTs, type variables are type indices while in non-generalized algebraic data types they are type parameters. In mutually recursive inductive types there is one more constraint: the type parameters must be the same for each type. We consider a type variable to be a parameter if it appears with the same name in each OCaml constructor and in the type definition. For example:

type ('a, 'b) arith =
  | Int : 'a * int -> ('a, int) arith
  | Eq : 'a * ('a, int) arith * ('a, int) arith -> ('a, bool) arith
  | Plus : 'a * ('a, int) arith * ('a, int) arith -> ('a, int) arith

is imported to:

Inductive arith (a : Type) : forall (b : Type), Type :=
| Int : a -> Z -> arith a Z
| Eq : a -> (arith a Z) -> (arith a Z) -> arith a bool
| Plus : a -> (arith a Z) -> (arith a Z) -> arith a Z.

Arguments Int {_}.
Arguments Eq {_}.
Arguments Plus {_}.

Here we transform 'a to a type parameter and 'b to a type index.

Limitations

Many OCaml programs define all types as mutually recursive by default. In Coq this is usually very difficult as:

only algebraic and synonym types can be mutual;
all type parameters must be the same;
the “strictly positive” constraint in Coq prevents some constructions (such as having a type as a type parameter for another);
the proofs or the definition of recursive functions on mutually recursive types is more complicated than with simple recursive types.

In practice, I would recommend to find a way to avoid mutually recursive types when possible. For cases they are used, I hope this import mechanism to be useful.