-
Notifications
You must be signed in to change notification settings - Fork 79
Folds
Structural Recursion and Folds in Scilla
Recursion in Scilla is presented by means of "folds" -- structural traversals. To see how they are expressed, let us take a look at some OCaml code, which we will later translate to Scilla verbatim.
Let us define natural numbers:
type nat = Zero | Succ of nat
The following two OCaml functions perform left/right folding over a natural number, with an "accumulator" z and an iterator f:
let rec nat_fold_left f z n =
match n with
| Zero -> z
| Succ n' ->
let res = f z n' in
nat_fold_left f res n'
let rec nat_fold_right f z n =
match n with
| Zero -> z
| Succ n' ->
let res = nat_fold_right f z n' in
f n' res
Even though they are equivalent modulo the order of formals in f, (see the works by Danvy), nat_fold_left makes it easier to map the intuition "forward" iteration, which passes a modified accumulator further (i.e., the combination is performed on the forward step of the recursion), while nat_fold_right is better for "backwards" iteration, when the result is assembled based on what's accumulated in the later calls (i.e., the combination is performed on the backwards step of the recursion).
We can now define the general fixpoint combinator in OCaml:
(* val fix : (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b *)
let rec fix f x = f (fix f) x
and use it to re-implement our functions, without relying on OCaml's let rec syntactic sugar:
let nat_fold_left' f z n =
let h = fix (fun g ->
(fun f z n -> match n with
| Zero -> z
| Succ n' ->
let res = f z n' in
g f res n')) in
h f z n
let nat_fold_right' f z n =
let h = fix (fun g ->
(fun f z n -> match n with
| Zero -> z
| Succ n' ->
let res = g f z n' in
f n' res )) in
h f z n
These implementations are now ported to Scilla as a single uniform fold (since they are equivalent, fold_left is adopted), which is extended with the Fixpoint operator (not accessible for client programs). While Fixpoint allows to implement general recursion, we only use it to implement structurally-recursive traversals (that provably terminate), provided in the library.
Nat comes with two folds: nat_foldl and nat_foldr, which are identical in semantics to the OCaml examples above.
For lists the two folds are not equivalent in general (it is only the case if the function f is associative).
TODO: describe implementation
Notice that folds are polymorphic functions, as they can be instantiated with iterators of multiple different types. For instance, the type of nat_fold is forall 'T, ('T -> Nat -> 'T) -> 'T -> Nat -> 'T, where the type variable 'T accounts for the type of the accumulator and the final results. Therefore, before being applied to arguments, folds need to be instantiated with argument types (those might themselves be type variables, if a fold is used within a body of a polymorphically-typed function, binding another type variable). For instance, in one of the examples below, nat_fold is instantiated before it is applied as follows:
let typed_folder = @nat_fold (Product Int Int) in
let folder = typed_folder iter_fun init_val in
(* Using folder as a function of type nat -> (Product Int Int) *)
Similarly, the types for folds over the lists are as follows:
list_foldl: forall 'A . forall 'B . ('B -> 'A -> 'B) -> 'B -> (List 'A) -> 'B
list_foldr: forall 'A . forall 'B . ('A -> 'B -> 'B) -> 'B -> (List 'A) -> 'B
let nat_prev = fun (n: Nat) =>
match n with
| Succ n1 => Some {Nat} n1
| Zero => None {Nat}
end in
let is_some_zero = fun (n: Nat) =>
match n with
| Some Zero => True
| _ => False
end in
let nat_eq = fun (n : Nat) => fun (m : Nat) =>
let z = Some {Nat} m in
let f = fun (res : Option Nat) => fun (n : Nat) =>
match res with
| None => None
| Some m1 => nat_prev m1
end in
let folder = @nat_fold (Option Nat) in
let e = folder f z n in
match e with
| Some Zero => True
| _ => False
end
let fib = fun (n : Nat) =>
let iter_fun =
fun (res : Product Int Int) => fun (n: Nat) =>
match res with
| Pair x y => let z = builtin add x y in Pair {Int Int} z x
end
in
let zero = 0 in
let one = 1 in
let init_val = Pair {Int Int} one zero in
let typed_folder = @nat_fold (Product Int Int) in
let folder = typed_folder iter_fun init_val in
let res = folder n in
match res with | Pair x y => x end
let list_map = tfun 'A => tfun 'B =>
fun (f : 'A -> 'B) => fun (l : List 'A) =>
let folder = @list_foldl 'A 'B in
let init = Nil {'A} in
let iter = fun (z : 'B) => fun (h : 'A) =>
let h1 = f h in
Cons {'B} h1 z
in folder iter init l
in
let int_map = @list_map Int Int in
let f = fun (i : Int) =>
let five = 5 in
builtin mul i five in
let one = 1 in
let two = 2 in
let three = 3 in
let nil = Nil in
let l1 = Cons {Int} three nil in
let l2 = Cons {Int} two l1 in
let l3 = Cons {Int} one l2 in
int_map f l3
Notice, though, that the resulting value is not type-correct:
(ADTValue Cons((TypeVar 'B))((IntLit 5)(ADTValue Cons((TypeVar 'B))((IntLit 10)(ADTValue Cons((TypeVar 'B))((IntLit 15)(ADTValue Nil((TypeVar 'B))()))))))),
This is due to the fact that the substitution of type variables is yet to be implemented, so the value features an unbound type variable 'b. Once the type substitution is implemented, the runtime value will become:
(ADTValue Cons((TypeVar Int))((IntLit 5)(ADTValue Cons((TypeVar 'B))((IntLit 10)(ADTValue Cons((TypeVar Int))((IntLit 15)(ADTValue Nil((TypeVar Int))()))))))),
let list_product =
fun (ls : List Int) => fun (acc : Int) =>
let iter =
fun (h : Int) => fun (res : Int) =>
let zero = 0 in
let b = builtin eq h zero in
match b with
| True => 0
| False => builtin mul h res
end
in
let rec_nat = @list_foldr Int Int in
rec_nat iter acc ls
in
let one = 1 in
let two = 2 in
let three = 3 in
let nil = Nil in
let l1 = Cons {Int} three nil in
let l2 = Cons {Int} two l1 in
let l3 = Cons {Int} one l2 in
list_product l3 one