Top

This file has been processed with:

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

See also this variant

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,'abioption. 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 patch #3[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 patch #3[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 patch #3[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