Top

This has been processed with:

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

## Folds

We can define addition on naturals through fold and lift it to lists too.

 type nat = | Z | S of nat type 'a natlike = | Z_ | S_ of 'a
 let natlike n = match n with | Z -> Z_ | S x -> S_ x let rec fold_nat f n = match n with | Z -> f Z_ | S(x) -> f (S_ (fold_nat f x)) let add n m = fold_nat (fun z -> match z with Z_ -> m | S_ y -> S y) n

We now define lists

 type 'a list = | Nil | Cons of 'a * 'a list type ('a,'b) listlike = | Nil_ | Cons_ of 'a * 'b
 type ornament 'a natlist : nat => 'a list with | Z => Nil | S n => Cons(_,n) when n : 'a natlist type ornament ('a,'b) natlistlike : 'b natlike => ('a,'b) listlike with | Z_ => Nil_ | S_ x => Cons_ (_,x) when x : 'b

Natural numbers are the fixed point of `'``a`` ``option` and lists of `(``elem``,'``a``) ``bioption`. We get an ornament from `option` to `bioption` that is an unfolded version of the ornament from `nat` to `list`, as witnessed by the fact that `unroll_list` is an ornament of `unroll_nat`

 let listlike = lifting natlike : _ natlist -> _ natlistlike with #2 <- (match n with Cons(x,_) -> x)
 let listlike n = match n with | Nil -> Nil_ | Cons(x, x1) -> Cons_(x, x1)

We can also write fold on nats and derive fold on lists:

 let fold_list = lifting fold_nat : (_ natlistlike -> _) -> _ natlist -> _ with #2 <- (match n with Cons(x,_) -> x)
 let rec fold_list f n = match n with | Nil -> f Nil_ | Cons(x, x1) -> f (Cons_(x, fold_list f x1))

From this, we recover append-as-a-fold from add-as-a-fold. An ornamentation annotation is necessary because the type option/bioption is used inside the term but not apparent in the type. So we need to tell the system we want to use the ornament `onetwoopt`

 let append = lifting add : _ natlist -> _ natlist -> _ natlist with | #2 <- (match z with Cons_ (x,_) -> x)

And we get the code of append:

 let append n m = fold_list (fun z -> match z with | Nil_ -> m | Cons_(x, n) -> Cons(x, n)) n