Booleans, Church numbers, and Church lists in OCaml
---------------------------------------------------
-(These questions adapted from web materials by Umut Acar. See <http://www.mpi-sws.org/~umut/>.)
-
+These questions adapted from web materials written by some smart dude named Acar.
The idea is to get booleans, Church numbers, "Church" lists, and
binary trees working in OCaml.
Recall from class System F, or the polymorphic λ-calculus.
- τ ::= α | τ1 → τ2 | ∀α. τ
- e ::= x | λx:τ. e | e1 e2 | Λα. e | e [τ ]
+ τ ::= 'α | τ1 → τ2 | ∀'α. τ | c
+ e ::= x | λx:τ. e | e1 e2 | Λ'α. e | e [τ ]
Recall that bool may be encoded as follows:
a function s : α → α.
**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, succ, and pred.
+ It's especially useful to do a version of pred, starting with one
+ of the (untyped) versions available in the lambda library
+ accessible from the main wiki page. The point of the excercise
+ is to do these things on your own, so avoid using the built-in
+ OCaml booleans and list predicates.
Consider the following list type:
As with nats, recursion is built into the datatype.
- We can write functions like map:
+ We can write functions like head, isNil, and map:
map : (σ → τ ) → σ list → τ list
- := λ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.
-
- Consider the following simple binary tree type:
- type ’a tree = Leaf | Node of ’a tree * ’a * ’a tree
+ We've given you the type for map, you only need to give the term.
- **Excercise**
- Write a function `sumLeaves` that computes the sum of all the
- leaves in an int tree.
+ With regard to `head`, think about what value to give back if the
+ argument is the empty list. Ultimately, we might want to make use
+ of our `'a option` technique, but for this assignment, just pick a
+ strategy, no matter how clunky.
- Write a function `inOrder` : τ 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.
+ Please provide both the terms and the types for each item.