Top

This has been processed with:

 ocamlorn --library stdlib.mli \ --library natlist_extended.in.ml --input natlist_extended.in.ml --lifting natlist_extended.lif.ml \ > natlist_extended.out.ml

## More complex ornaments

Starting with natural numbers, we define standard lists by ornamentations, but also two variants of lists: lists with a duplicated constructor and lists that may or may not contain an element at each position. Namely, here are all the datatypes we are interested in:

 type nat = | Z | S of nat
 type 'a list = | Nil | Cons of 'a * 'a list type 'a bilist = | Nil0 | Cons1 of 'a * 'a bilist | Cons2 of 'a * 'a bilist type 'a maybelist = | NilM | ConsNone of 'a maybelist | ConsSome of 'a * 'a maybelist

We define a few functions operating on integers:

 let id = fun x -> x let zero = Z let rec add m n = match m with | Z -> n | S m' -> S(add m' n)

We can then obtain the operations on standard lists by lifting those on integers: the identity function can be lifted without any patch or extra information; a value (like nil) can be lifted by simply giving the target type

 type ornament 'a natlist : nat => 'a list with | Z => Nil | S n => Cons (_, n) when n : 'a natlist let id2 = lifting id let nil = lifting zero : _ natlist
 let id2 x = x let nil = Nil

The concatenation on lists need more information. If we only specify, the expected type

 let _append = lifting add : _ natlist -> _ natlist -> _ natlist

we get this incomplete scheleton

 let rec _append m n = match m with | Nil -> n | Cons(_, m') -> Cons(#2, _append m' n)

We can then provide the missing information as a patch:

 let append = lifting add : _ natlist -> _ natlist -> _ natlist with | #2 <- match m with Cons(a,_) -> a

and we get the expected code:

 let rec append m n = match m with | Nil -> n | Cons(a, m') -> Cons(a, append m' n)

Notice that this is exactly the code that we could have manually written, up to the choice of identifiers.

 let rec append ml nl = match ml with | Nil -> nl | Cons(a,ml') -> Cons(a, append ml' nl)

We may also lift `add`—doing nothing, which we call the identity lifting. This can be specified, as follows:

 let add2 = lifting add with | ornament * <- @id

The pattern `| * <- ``@id` means that any unspecified ornament will default to the identity. We just get another copy of `add`:

 let rec add2 m n = match m with | Z -> n | S m' -> S (add2 m' n)

Lists with two constructors are an ornament of lists with one constructor, having a choice between `Cons1` and `Cons2`:

 type ornament 'a listbilist : 'a list => 'a bilist with | Nil => Nil0 | Cons(a,l) => (Cons1(a,l) | Cons2(a,l)) when l : 'a listbilist

We can also lift lists at this type (here we choose to specify patching points rather than an ornament signature).

 let append2 = lifting append with | ornament * <- listbilist | #2 <-match ml with Cons1(_,_) -> Left(()) | Cons2(_,_) -> Right(())

We get

 let rec append2 ml nl = match ml with | Nil0 -> nl | Cons1(a, ml') -> Cons1(a, append2 ml' nl) | Cons2(a, ml') -> Cons2(a, append2 ml' nl)

The unit type (represented as `()` for syntactic reasons) is also an ornament of `nat`. The pattern `S``(``_``)` is mapped to the empty pattern `~`.

 type ornament natunit : nat => () with | Z => () | S(n) => ~ when n : natunit

The type `maybelist` is also an ornament of `nat`

 type ornament 'a natmaybelist : nat => 'a maybelist with | Z => NilM | S(x) => (ConsNone(x) | ConsSome(_,x)) when x : 'a natmaybelist

We may also lift `add` at both of these types

 let add0 = lifting add with | ornament * <- natunit let addmaybe = lifting add with | ornament * <- natmaybelist | #2 <- match m with ConsNone(_) -> Left(()) | ConsSome(a,_) -> Right(a)
 let add0 m n = match m with | () -> n let rec addmaybe m n = match m with | NilM -> n | ConsNone m' -> ConsNone (addmaybe m' n) | ConsSome(a, m') -> ConsSome(a, addmaybe m' n)
 type bool = | True | False
 let rec equal_nat m n = match (m, n) with | (Z, Z) -> True | (S m', S n') -> equal_nat m' n' | _ -> False
 let equal_length = lifting equal_nat : _ natlist -> _ natlist -> bool with | ornament * <- @id
 let rec equal_length m n = match m with | Nil -> begin match n with | Nil -> True | Cons(_, _) -> False end | Cons(_, n1) -> begin match n with | Nil -> False | Cons(_, n) -> equal_length n1 n end