Subtypable Trees

This is a report of my attempts to design subtypable tree data structures in OCaml. The original need was the following: Kindergarten shall be a program to describe simple algebraic laws and to apply them on terms just like algebraic computation—while obtaining all intermediate steps for example for L^AT_EX output.

So I need a data type for the abstract syntax tree of arithmetic terms and a data type for patterns on those terms. To share the constructors (i.e. every term is a pattern, too) and the interface (e.g. mapping of terms and patterns), and furthermore for efficiency and for a orthogonal implementation, it is preferable to have real subtyping between the two, i.e. term :> pattern.

Luckily OCaml provides the right tools for that: Polymorphic variants. I realized subtypable tree structures by detaching constructor definition and recursion in its core:

type ’self pre_term =
[ ‵Number of float (∗ 12.34 ∗)
∣ ‵Negate of ’self ] (∗ -(2.3) ∗)
type ’self pre_pattern =
[ ’self pre_term (∗ A term ∗)
∣ ‵Any (∗ A wildcard ∗)
∣ ‵Contains of ’self ] (∗ Another pattern is contained, e.g. ... 0.0 ... ∗)

This offers the possibility to define the type of the subnodes seperatly from the type of the subnodes. This is necessary to use the pre_term constructors for patterns (as ’pattern pre_term).

The actual types term and pattern are defined as closures in a second step:

type term = term pre_term
type pattern = pattern pre_pattern

Now a value of type pattern is a made of a constructor from pre_pattern—that is, also from pre_term—and every subnode is a pattern, too. Accordingly, a value of type term is is made of a constructor from pre_term where every subtree is a term and can easily be coerced to a value of type pattern.

let t : term = ‵Negate (‵Number 10.0)
let p1 = (t : term :> pattern)
let p2 : pattern = ‵Negate ‵Any
(∗ but not let p3 : term = ‵Negate p2 ∗)

The next step is to define mapping functions for terms and patterns. The function applied to the nodes of the particular trees returns either Some x where x is the new node or None where mapping recurs on the node. To define these mapping functions, a similar trick of detaching function definition and recursion is necessary:

let pre_map_term self : (α pre_term → α option) → α pre_term → α =
fun f x →
match f x with
∣ Some y → y
∣ None →
match x with
∣ ‵Number f → ‵Number f
∣ ‵Negate z → ‵Negate (self z)

let pre_map_pattern self : (α pre_pattern → α option) → α pre_pattern → α =
fun f x →
match f x with
∣ Some y → y
∣ None →
match x with
∣ ‵Any → ‵Any
∣ ‵Contains z → ‵Contains (self z)
∣ #pre_term as term →
pre_map_term self (f :> α pre_term → α option) term

The use of self here is the following: It is not possible to use the mapping function itself to map the subnodes (subnodes in pre_map_term can be terms or patterns). In fact self is a pre-applied version of the resulting mapping function (to circumvent the monomorphity of function arguments) and finally puts recursion into play:

let rec map_term : (term → term option) → term → term =
fun f x → pre_map_term (map_term f) f x
let rec map_pattern : (pattern → pattern option) → pattern → pattern =
fun f x → pre_map_pattern (map_pattern f) f x

Now the algebraic rule for extinction of two negation is given in the following way (take a look into the Kindergarten program for more complex pattern matching with variable binding and unification):

map_pattern (fun ‘Negate (‵Negate x) → x)

And it is possible to easily map terms on patterns likewise:

map_pattern (fun ‘Negate _ → Some ‵Any ∣ _ → None) (t : term :> pattern)

That’s the solution I came up with to have subtyping between different tree datums without any redundancy—I am very interested if this is possible in a easier way, so please don’t hesitate to comment …

PS: I have just noticed that this is just the same as Jacque Garrigue's "Code reuse through
polymorphic variants".