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

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.

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.

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.

blog comments powered by Disqus