チャーチリスト
from Church encoding
型注釈はSystem Fによるもの
型注釈
List X = ∀R. (X->R->R) -> R -> R Cons
cons = λ h t c n. c h (t c n) cons: ΛX. λh:X. λt:List X. (ΛR. λc:X->R->R. λn:R. c h (t[R] c n)) as List X cons: ∀X. X -> List X -> List X h: X はhead t: List X はtailex.
[x,y,z] = λ c n.c x (λ c' n'. c' y (λ c'' n''. c'' z n'')) Nil
nil = λ c n.n nil = ΛX. (ΛR. λc:(X->R->R). λn:R. n) as List X nil: ∀X. List X isNil
isNil = λl.l (λh.λt.fls) tru isNil = ΛX. λl:List X. l[CBool] (λh:X. λt:Bool. fls) tru isNil: ∀X. List X -> CBool head
head = λl.l(λh.λt.h) fls head: ∀X. List X -> X headへの型付けは少し難しい ref 
p.276
tail
tail = λl c n. l (λ h t g. g h (t c))(λt.n)(λh.λt.t) tail = λl.l(λ x xs.xs) nil tail: ∀X. List X -> List X tailへの型付けはかなり複雑 ref pp.276-277
foldr
foldr = λ n c l. l c n 参考