projects
/
lambda.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
ass5: tweaks
[lambda.git]
/
assignment5.mdwn
diff --git
a/assignment5.mdwn
b/assignment5.mdwn
index
fab21e4
..
a79df5f
100644
(file)
--- a/
assignment5.mdwn
+++ b/
assignment5.mdwn
@@
-165,7
+165,7
@@
times. In the polymorphic encoding above, the result of that iteration can be
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,
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:
Consider the following list type:
@@
-174,8
+174,8
@@
Consider the following list type:
We can encode τ lists, lists of elements of type τ as follows:
τ list := ∀'a. 'a → (τ → 'a → 'a) → 'a
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
- make
List
τ := λ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.
As with nats, recursion is built into the datatype.
@@
-185,17
+185,18
@@
We can write functions like map:
= λf :σ → τ. λl:σ list. l [τ list] nilτ (λx:σ. λy:τ list. consτ (f x) y
**Excercise** convert this function to OCaml. Also write an `append` function.
= λ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. Also write nil??? Test with simple lists.
+
Consider the following simple binary tree type:
type 'a tree = Leaf | Node of 'a tree * 'a * 'a tree
**Excercise**
Consider the following simple binary tree type:
type 'a tree = Leaf | Node of 'a tree * 'a * 'a tree
**Excercise**
-Write a function `sum
L
eaves` that computes the sum of all the
+Write a function `sum
_l
eaves` that computes the sum of all the
leaves in an int tree.
leaves in an int tree.
-Write a function `in
O
rder` : τ tree → τ list that computes the in-order traversal of a binary tree. You
+Write a function `in
_o
rder` : τ 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
may assume the above encoding of lists; define any auxiliary functions you need.
Baby monads