HaskellでChurch numeralの実装

Question

HaskellでChurch numeralを実装しようと、
以下のような関数を定義しました。

true x y = x
false x y = y
_if b x y = b x y
zero f x = x
one f x = f x
s n f x = f (n f x)
isZero n = n (\x->false) true
add m n f x = m f (n f x)
mult m n f = m (n f)
toInt n = n (+1) 0
toChurch 0 = zero
toChurch n = s (toChurch (n-1))
pre n f x = (n (\g h->h(g f)) (\u->x)) (\u->u)

toInt(add (toChurch 3) (toChurch 8))などは、きちんと11になります。preの定義はWikipediaから引っ張ってきました。

ところが、上の関数をSample.hsに書いて、ghciで読み込んだ後、次の単純な関数を定義しようとすると、エラーになります。直感的には、nが0なら1を、0以外ならそのまま返すだけの単純な関数なのですが…。

let hoge n = _if (isZero n) one n

下記のエラーが出るのですが、型がうまく取れていなさそうだということしかわかりません。どうすればよいのでしょうか。
それとも、Haskellでは型の制限でChurch numeralを実装するのは不可能でしょうか。

Occurs check: cannot construct the infinite type:
t2
~
(t1 -> t3 -> t4 -> t4)
-> (t6 -> t5 -> t6) -> ((t8 -> t7) -> t8 -> t7) -> t2 -> t
Relevant bindings include
n :: (t1 -> t3 -> t4 -> t4)
-> (t6 -> t5 -> t6) -> ((t8 -> t7) -> t8 -> t7) -> t2 -> t
(bound at <interactive>:2:10)
hoge :: ((t1 -> t3 -> t4 -> t4)
-> (t6 -> t5 -> t6) -> ((t8 -> t7) -> t8 -> t7) -> t2 -> t)
-> t
(bound at <interactive>:2:5)
In the third argument of ‘_if’, namely ‘n’
In the expression: _if (isZero n) one n

Answer 1

HaskellでChurch数を表現するには以下のようにすれば可能です。
再帰的な型を扱うためには明示的に型を作成してやる必要があります。

より単純な例でまずは説明します。
たとえばf x = x xのような場合xの型はどうなるでしょうか。
xの型がaだったとするとxは引数xを取り何かを返す関数でもあるのでxの型はa -> bとなります。
すると今度はxの型は(a -> b) -> cとなります。
さらにxの型は((a -> b) -> c) -> dとなり...のようにいつまでも型が決まりません。
このような場合、代数的データ型で明示的に再帰的な型を作ってやる必要があります。
newtype R a = R { unR :: R a -> a }のようにします。
すると、型R aは(R a -> a)を保持する再帰的な型となります。
このようにするとf x = unR x xのように表現することができます。

型Rの場合、再帰的になっているのは引数の部分('->'の左側)だけです。
Church数の場合、返り値('->'の右側)の部分も再帰的にする必要があるので、以下のような型となります。

見やすさを考えて(.$.)という演算子を定義していますが、
実際にしていることはCとunCによって関数をデータ型Cに入れたり出したりしているということになります。

静的な型付けで再帰的な型を定義するこのやりかたは僕には非常に美しいように感じます。
またA CやZはChurch数を数値に変換するために用意したもので、本質的な部分ではありません。

data C = C { unC :: C -> C } | A C | Z

(.$.) :: C -> C -> C
(.$.) = unC

toInt :: C -> Int
toInt Z = 0
toInt (A c) = 1 + toInt c
toInt n = toInt $ n .$. C A .$. Z

toChurch :: Int -> C
toChurch 0 = zero
toChurch n = s .$. toChurch (n - 1)

false, true, _if :: C
false = C (\x -> C (\y -> y))
true = C (\x -> C (\y -> x))
_if = C (\b -> C (\x -> C (\y -> b .$. x .$. y)))

zero, one, s :: C
zero = C (\f -> C (\x -> x))
one = C (\f -> C (\x -> f .$. x))
s = C (\n -> C (\f -> C (\x -> f .$. (n .$. f .$. x))))

isZero :: C
isZero = C (\n -> n .$. (C (\x -> false)) .$. true)

add, mult, pre :: C a
add = C (\m -> C (\n -> C (\f -> C (\x -> m .$. f .$. (n .$. f .$. x)))))
mult = C (\m -> C (\n -> C (\f -> m .$. (n .$. f))))
pre = C (\n -> C (\f -> C (\x ->
	(n .$. (C (\g -> C (\h -> h .$. (g .$. f)))) .$. (C (\u -> x))) .$. (C (\u -> u)))))

hoge :: C
hoge = C (\n -> _if .$. (isZero .$. n) .$. one .$. n)

これを読み込んで以下のようにすると求めていた結果が得られるはずです。

toInt $ hoge .$. zero
toInt $ hoge .$. one
toInt $ hoge .$. (toChurch 8)

Answer 2

型を明示してチャーチ数を書きました。

type Cbool a = a -> a -> a
type Cnum a = (a ->a) -> a -> a

true :: Cbool a
true x y = x

false :: a -> a -> a
false x y = y

not :: Cbool (Cbool a) -> Cbool a
not x = x false true

zero :: Cnum a
zero f = id

one :: Cnum a
one f = f

two :: Cnum a
two f = f . f

succ :: Cnum a -> Cnum a
succ cn f = f . cn f

_if :: Cbool a-> a -> a->  a
_if b x y = b x y

isZero :: (Cnum (Cbool a1)) -> Cbool a1
isZero n = n (\x -> false)  true

f a b c ::  (Cnum (Cbool a)) -> a -> a -> a
f a b c = _if (isZero a) b c

Comments

[selpo]

ありがとうございます。

なんとなくわかってきました。
Cnumの型は(a->a)->a->aですが、isZeroの引数としてはa=Cbool bでなければならない、ということですね。
本来のchurch numeralはCnum aのaは任意の型としても扱えるのに、Haskellでは制限が加わる、と。
そうすると、_if (isZero n) one nと書いてしまうと、oneとnの型が食い違ってエラーになる、と。

確かに、_if (isZero n) one nの代わりに_if (isZero n) one mと違う変数にすれば解決できますね。
しかし、そうすると期待した動作をさせることはできないのではないでしょうか…。
やはり無理そうに思えてきました…。
Unsafeとやらを使うしかないのでしょうか。