Top
This file 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
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 |