チャーチ数の加減乗除

型推論を無効にする方法を発見。

型推論をごまかす Y コンビネータ
L の定義は、本当は L x y = x (y y) です。(y y)の部分が自己言及になって、GHC ではこの部分の型をうまく処理できません。そこで、unsafeCoerce で型推論をごまかしています。

http://d.hatena.ne.jp/kazu-yamamoto/20100519/1274240859

おかげで、断念していたHaskell版のチャーチ数の引き算とYコンビネータを使った割り算(と剰余)が作れた。
これで加減乗除の基本演算がそろった。感謝。

import Unsafe.Coerce

m x = x (unsafeCoerce x)
y f = m (\x -> f (m x))

true  x y = x
false x y = y
not'  p   = p false true
and'  p q = p q false
or'   p q = p true q

cons x y f = f x y
car p = p true
cdr p = p false

inc n f x = f (n f x)
incs p = cons (cdr p) (inc (cdr p))
dec n = car (n incs (const n0))

n0 f x = x
n1 f x = f x
n2 = inc n1
n4 = n2 n2
n5 = inc n4

add m n f x = m f (n f x)
mul m n f   = m (n f)
pow m n     = unsafeCoerce n m
sub m n     = unsafeCoerce n dec m

is0  n = n (const false) true
le m n = is0 (sub m n)
ge m n = le n m
lt m n = not' (ge m n)
gt m n = lt n m

mod' f m n = (lt m n) m       (f (sub m n) n)
div' f m n = (lt m n) n0 (inc (f (sub m n) n))

num n = n (+1) 0 :: Int
main = print $ map (\f -> num $ f n5 n2) [add,mul,pow,sub,y mod',y div']

実行結果
それぞれ5+2, 5*2, 5^2, 5-2, 5%2, 5/2の計算結果になっている。

[7,10,25,3,1,2]

結局unsafeCoerceを使ったのはmコンビネータとpowとsubの3カ所。
n4 = n2 n2はそのまま通るのに、なぜpowはunsafeCoerceをつけないとエラーになるのかが謎。