Please read Chapter 23-25 in your textbook.
The programming questions should be done using the
fullomega type checker, and you should copy in the
church-numeral encoding of pairs and lists from test.f in the
fullomega checker directory.
sum : (List Nat)You will find this helpful when testing problems below.Nat
filter :X. (X
Bool)
(List X)
List X
map
using the Church encoding of lists. It should have the same
type as on page 346. List type defined on page 351 exposes the internal
representation. For example, we couldn't substitute an implementation
using recursive types. The following definition fixes this problem
OOList = lambda X.
{Some R,{state:R, nil:R,
isnil: R->Bool,
cons: X->R->R,
head: R->X,
tail: R->R}};
oonil that has type
ooisnil, oocons, oohead,
ootail so that they have the following types:
ooisnil :X. (OOList X)
Bool oocons :
X. X
(OOList X)
(OOList X) oohead :
X. (OOList X)
X ootail :
X. (OOList X)
(OOList X)
oomap to use these primitives
(you may assume fix). Test your program by running
oohead[Bool]
(oomap[Int][Bool] iseven
(oocons[Nat] 1 (oocons[Nat] 2 (oonil[Nat]))))