Top

This has been processed with:

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`

`,'`

`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 |