any type 'a, as long as you have a base element z : 'a and a function s : 'a → 'a.
**Excercise**: get booleans and Church numbers working in OCaml,
-including OCaml versions of bool, true, false, zero, succ, add.
+including OCaml versions of bool, true, false, zero, iszero, succ, and **pred**.
Consider the following list type:
We can encode τ lists, lists of elements of type τ as follows:
τ list := ∀'a. 'a → (τ → 'a → 'a) → 'a
- nilτ := Λ'a. λn:'a. λc:τ → 'a → 'a. n
- makeListτ := λh:τ. λt:τ list. Λ'a. λn:'a. λc:τ → 'a → 'a. c h (t ['a] n c)
+ nil τ := Λ'a. λn:'a. λc:τ → 'a → 'a. n
+ make_list τ := λh:τ. λt:τ list. Λ'a. λn:'a. λc:τ → 'a → 'a. c h (t ['a] n c)
As with nats, recursion is built into the datatype.
= λf :σ → τ. λl:σ list. l [τ list] nilτ (λx:σ. λy:τ list. consτ (f x) y
**Excercise** convert this function to OCaml. Also write an `append` function.
-Test with simple lists.
+Also write a **head** function. Test with simple lists.
+
Consider the following simple binary tree type:
type 'a tree = Leaf | Node of 'a tree * 'a * 'a tree
**Excercise**
-Write a function `sumLeaves` that computes the sum of all the
+Write a function `sum_leaves` that computes the sum of all the
leaves in an int tree.
-Write a function `inOrder` : τ tree → τ list that computes the in-order traversal of a binary tree. You
+Write a function `in_order` : τ tree → τ list that computes the in-order traversal of a binary tree. You
may assume the above encoding of lists; define any auxiliary functions you need.
Baby monads