チャーチリスト
型注釈
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はtail
ex. [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 TaPL.icon 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 TaPL.icon pp.276-277
foldr
foldr = λ n c l. l c n
参考