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 |