John Harrison gives the follow suite of list functions and ascribes them to Mairson (1991) in this bibliography. Consider exercise 6 of Harrison’s Chapter 3.
Here are our one character names and Harrison’s names for the given functions:
A: append_lists L: fst (λx.xK) R: snd (λx.xH) S: SUC T: tack a: append c: cons f: filter h: head l: length m: map p: pair (λxy.(x, y)) H: nil (built in) r: reverse t: tailNote the primal environ which defines K, H, P and i.
((λpLRS. ; Harrison's prerequisites (λc.(λhtamlT.(λArf. ; Mairson's functions (R (p 4 6)) ; payload ) (λL.LaH) ; A: append_lists (λl.lTH) ; r: reverse (λlt.l(λx.(tx)(cx)(λy.y))H) ; f: filter ) (λl.lKH) ; h: head (λl.R(l(λxq.p(cx(Lq))(Lq))(pHH))) ; t: tail (λkl. kcl) ; a: append (λfl.l(λx.c(fx))H) ; m: map (λl.l(λx.S)(λfx.x)) ; l: length (λxl.lc(cxH)) ; T: tack ) (λxlcn.cx(lcn)) ; c: cons ) (λxy. (λf.fxy)) ; p: pair (λp.pK) ; L: fst (λp.pH) ; R: snd (λnfx.nf(fx)) ; S: SUC )Here are successively more challenging expressions to serve as payload, and their yields. The last column is an analogous Scheme expression. Red yields are side effects of the function P.
(L (p 4 6)) | 4 | (car (cons 4 6)) |
(R (p 4 6)) | 6 | (cdr (cons 4 6)) |
((λn.ni0)(lH)) | 0 | (length '()) |
((λn.ni0)(l(c4H))) | 1 | (length '(4)) |
(P66) | B66 | (write 66) |
(mP(c65H)) | A | (map write '(65)) |
(h(c4H)) | 4 | (car (list 4)) |
(mP(c65(c66H))) | AB | (map write '(65 66)) |
(h(t(c3(c6H)))) | 6 | |
(mP(a(c65(c66H))(c67(c68H)))) | ABCD | (append '(65 66) '(67 68)) |
(mP(A(c(c65(c66H))(c(c69(c68H))H)))) | ABED | |
(mP(r(c65(c66(c67H))))) | CBA | (reverse '(65 66 67)) |
((λs.(mP(as(mis))))(c65(c66(c67H)))) | ABCBCD |
(let ((s '(65 66 67))) (append s (map (λ (x) (+ x 1)) s))) |