代数データ型とラムダ式

代数データ型(バリアント)をラムダ式で表現する方法の備忘録。ラムダ式を表現するのに、実行可能な Haskell の無名関数を使う。間違いの指摘を歓迎します。

こんな感じ：

\x y z ... f g h ... -> 引数をうまく組み合わせる

• x y z ... の部分が、直積を表す
• f g h ... の部分が、構成子で直和を表す

Unit

コンストラクタが1つ。

data Unit = Unit

unit = \u -> u

Bool(直和)

一般的な Bool のラムダ式表現に合わせて、True を先に書いておく。

data Bool = True | False

true  = \t f -> t
false = \t f -> f

組(直積)

data Pair x y = Pair x y

pair = \x y p -> p x y

fst = \c -> c true
snd = \c -> c false

fst $ pair 1 2
→ 1

Either(直和)

data Either l r = Left l | Right r

left  = \x l r -> l x
right = \x l r -> r x

自然数

data Nat = Succ Nat | Zero

succ = \n s z -> s (n s z)
zero = \s z -> z

リスト

data List a = Cons a (List a) | Nil

cons  = \x xs c n -> c x (xs c n)
nil   = \c n -> n

参考文献

• ラムダ計算で代数的データ型を表現する方法