Folds

Structural Recursion and Folds in Scilla

Introduction

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).

Implementation of Fixpoints

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.

Folds for built-in ADTs

Natural numbers

Nat comes with two folds: nat_foldl and nat_foldr, which are identical in semantics to the OCaml examples above.

Lists

For lists the two folds are not equivalent in general (it is only the case if the function f is associative).

TODO: describe implementation

Polymorphic specifications for folds

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

Examples and Case Studies

Examples with Nat

Equality

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

Fibonacci numbers

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

List examples

Mapping a function over a list

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

Product of integer numbers in a list

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