チャーチペア
from
Church encoding
チャーチブール値
を用いると、2つの値の組を項として表現できる
型注釈は
System F
によるもの
(m, n) = λb.b m n
b
に
チャーチブール値
を入れることで
m
または
n
が得られる
数値型のタプルの場合
(m, n): PairNat
型注釈
数値型のタプルの場合
PairNat = ∀X. (CNat -> CNat -> X) -> X
fst = λx.x tru
fst (m, n) = m
数値型のタプルの場合
fst: PairNat -> CNat
snd = λx.x fls
snd (m, n) = n
数値型のタプルの場合
snd: PairNat -> CNat