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, nat_fold_left makes it easier to implement "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, 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

Polymorphic specifications

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 e = nat_foldl f z n in
  match e with
  | Some Zero => True
  | _ => False
  end

Fibonacci numbers

let fib = fun (n : Nat) =>
  let iter_fun =
    fun (n: Nat) => fun (res : Product Int Int) =>
      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 res = nat_foldr iter_fun init_val n in
  match res with
	| Pair x y => x
  end