Top
This file has been processed with:
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(#3, _append m' n) |
We can then provide the missing information as a patch:
let append = lifting add : _ natlist -> _ natlist -> _ natlist with
patch #3[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
patch #3[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 _ => ~ |
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
patch #3[match m with ConsNone(_) -> Left(()) | ConsSome(a,_) -> Right(a)] |
let add0 m n = 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, n) with
| (Nil, Nil) -> True
| (Cons(_, n), Cons(_, n1)) -> equal_length n n1
| _ -> False |