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.
+ We've given you the type for map, you only need to give the term.
- Consider the following simple binary tree type:
+ 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.
- type ’a tree = Leaf | Node of ’a tree * ’a * ’a tree
-
- **Excercise**
- Write a function `sumLeaves` 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
- may assume the above encoding of lists; define any auxiliary functions you need.
+ Please provide both the terms and the types for each item.