型付きラムダ計算で四則演算を実装します
こちらのQ&Aを参考にしています
以下のコードはローカルのghcで動作確認済みです
プログラムを複製して実行すればサンプルコード下部の実行結果が得られます
ただし全ての実行環境で動作する保障はありません
実際にオンライン上の仮想コンパイラによってはエラーが返されます
サンプルコード
{-# LANGUAGE RankNTypes #-}
import Data.Monoid
main::IO ()
main =printNum>>printStr
toNum::Num a=>Nat->a
toNum n=n (1+) 0
toStr::Monoid a=>Nat->a->a
toStr n a=n (a<>) a
printNum::IO ()
printNum=print $ toNum $ dvs (add four four) $ three
printStr::IO ()
printStr=print.toStr (sub (mul four two) three) $ "a"
type Id a=a->a
type Nat=forall a.(a->a)->a->a
type Suc a=Id a
type Pair a=(a->a->a)->a
type If a b c=a->b->c
f::(a->a)->a
f y=y $ f y
zero::Nat
zero f x=x
one::Nat
one f x=f x
suc::Suc Nat
suc a b c=b.a b $ c
two::Nat
two=suc one
true::If a b a
true a b=a
false::If a b b
false a b=b
bool::Id (If a b c)
bool f a b=f a b
md::Nat->Nat->Nat
md=f $ \ f n m->bool (le m n) (f (sub n m) m) n
dvs::Nat->Nat->Nat
dvs=f $ \ f n m->le m n (suc (f (sub n m) m)) zero
cond::(If a b a->If a b b->c)->c
cond n=bool n true false
eqz::((a->If b c c)->If d e d->f)->f
eqz n=n (\ x->false) true
le::Nat->Nat->If c c c
le x y=eqz $ sub x y
toBool::Nat->Nat->Nat
toBool n m=cond (le n m) zero one
add::Nat->Nat->Nat
add a b c d=a c $ b c d
three::Nat
three=add one two
cons::Nat->Nat->Pair Nat
cons a b f=f a b
first::Pair Nat->Nat
first p=p $ \ a b->a
second::Pair Nat->Nat
second p=p $ \ a b->b
next::Id (Pair Nat)
next p=cons (add (first p) one) $ first p
pre::Id (Pair Nat)
pre n=(second n) next $ cons zero zero
sub::Nat->Nat->Nat
sub a b=first $ b pre $ a next $ cons zero zero
mul::Nat->Nat->Nat
mul a b c=a (b c)
four::Nat
four=add two two
eight::Nat
eight=add four four
threeTwo::Nat
threeTwo=mul four eight
five::Nat
five=add two three
2
"aaaaaa"
型推論や明示的型付けではpre(前者関数)以降の演算でエラーが発生します
これはsub(減算)の実行時に再帰的なpreの簡約によって引数と戻り値の型が変化し続けることが原因のようです
そのためチャーチ数の型付けにforallを用いています
これにより型推論の過程で型がある種の戻り値扱いとなり、実装の文脈から最終的な型が類推される仕組みのようです
なお、ghcでは実行不可ながら、特定のサイトでは動作したプログラムもあります
サブコード
import Data.Monoid
main::IO ()
main=makeStr>>makeNum
toStr::Monoid a=>Nat a->a->a
toStr n s=n (s<>) s
makeStr::IO ()
makeStr=print.toStr (mul (sub four two) $ add three two) $ "a"
toNum::Num a=>Nat a->a
toNum n=n (1+) 0
makeNum::IO ()
makeNum=print.toNum $ dvs (add four four) three
type Id a=a->a
type Nat a=Id (Id a)
type Suc a=Id (Nat a)
type Pair a=(a->a->a)->a
type If a b c=a->b->c
f::(a->a)->a
f y=y $ f y
zero::Nat a
zero f x=x
--one::Id (a->b)
one::Nat a
one f x=f x
suc::Suc a
suc a b c=b.a b $ c
two::Nat a
two=suc one
true::If a b a
true a b=a
false::If a b b
false a b=b
bool::Id (If a b c)
bool f a b=f a b
md::Nat a->Nat (Nat a->Nat a->Nat a)->Nat a
md=f $ \ f n m->bool (le m n) (f (sub n m) m) n
dvs::Nat a->Nat (Nat a->Nat a->Nat a)->Nat a
dvs=f $ \ f n m->le m n (suc (f (sub n m) m)) zero
cond::(If a b a->If a b b->c)->c
cond n=bool n true false
eqz::((a->If b c c)->If d e d->f)->f
eqz n=n (\ x->false) true
le::Nat (If c c c)->Nat b->If c c c
le x y=eqz $ sub x y
toBool::Nat (If (If (Nat c) (Nat c) (Nat c)) (If (Nat c) (Nat c) (Nat c)) (If (Nat c) (Nat c) (Nat c)))->Nat b->Nat c
toBool n m=cond (le n m) zero one
add::Nat a->Nat a->Nat a
add a b c d=a c $ b c d
--add::Nat (Nat a)->Nat a->Nat a
--add a b=a suc b
three::Nat a
three=add one two
cons::Nat a->Nat a->Pair (Nat a)
cons a b f=f a b
first::Pair (Nat a)->Nat a
first p=p true
second::Pair (Nat a)->Nat a
second p=p false
next::Id (Pair (Nat a))
next p=cons (add (first p) one) $ first p
pre::Nat (Pair (Nat a))->Nat a
pre n=second.n next $ cons zero zero
--pre::(((b->c)->(c->c)->c)->(b->c)->(c->c)->c)->b->c->c
--pre = \ n f x-> n (\ g h->h (g f)) (\ u->x) (\ u->u)
--sub::Nat (Pair (Nat a))->((Nat (Pair (Nat a))->Nat a)->Nat (Pair (Nat a))->Nat a)->Nat a
--sub::Nat (Nat a)->Nat b->Nat c
sub::Nat a->Nat b->Nat a
sub a b=b pre a
mul::Nat (Nat a)->Nat a->Nat a
mul a b=a (add b) zero
four::Nat a
four=mul two two
eight::Nat a
eight=mul four two
threeTwo::Nat a
threeTwo=mul four eight
five::Nat a
five=add two three
"aaaaaaaaaaa"
2
実行可能ということは理論的な整合性があるはずなので、型クラスなどで独自に抽象化しているのかもしれません
もしこのプログラムをghcで実行できた方がいれば、実装を共有して頂けると幸いです
次回はサンプルコードを整理しつつ、具体的な解説を添えられればと思います
改めてHaskellの底力を垣間見たような気がします
ラムダ理論を学びたい方はHaskellを使いましょう