質問をすることでしか得られない、回答やアドバイスがある。

15分調べてもわからないことは、質問しよう!

新規登録して質問してみよう
ただいま回答率
85.50%
Haskell

Haskellは高い機能性をもった関数型プログラミング言語で、他の手続き型プログラミング言語では難しいとされている関数でも容易に行うことができます。強い静的型付け、遅延評価などに対応しています。

GHC

Glasgow Haskell Compiler(GHC) は Haskell コンパイラです 異なる複数のアーキテクチャのネイティブコードや、C言語へコンパイルする事ができます。

Q&A

解決済

2回答

2375閲覧

HaskellでChurch numeralの実装

selpo

総合スコア41

Haskell

Haskellは高い機能性をもった関数型プログラミング言語で、他の手続き型プログラミング言語では難しいとされている関数でも容易に行うことができます。強い静的型付け、遅延評価などに対応しています。

GHC

Glasgow Haskell Compiler(GHC) は Haskell コンパイラです 異なる複数のアーキテクチャのネイティブコードや、C言語へコンパイルする事ができます。

1グッド

2クリップ

投稿2015/03/03 11:23

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

lang

1true x y = x 2false x y = y 3_if b x y = b x y 4zero f x = x 5one f x = f x 6s n f x = f (n f x) 7isZero n = n (\x->false) true 8add m n f x = m f (n f x) 9mult m n f = m (n f) 10toInt n = n (+1) 0 11toChurch 0 = zero 12toChurch n = s (toChurch (n-1)) 13pre 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以外ならそのまま返すだけの単純な関数なのですが…。

lang

1let 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

DrqYuto👍を押しています

気になる質問をクリップする

クリップした質問は、後からいつでもMYページで確認できます。

またクリップした質問に回答があった際、通知やメールを受け取ることができます。

バッドをするには、ログインかつ

こちらの条件を満たす必要があります。

guest

回答2

0

ベストアンサー

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数を数値に変換するために用意したもので、本質的な部分ではありません。

Haskell

1data C = C { unC :: C -> C } | A C | Z 2 3(.$.) :: C -> C -> C 4(.$.) = unC 5 6toInt :: C -> Int 7toInt Z = 0 8toInt (A c) = 1 + toInt c 9toInt n = toInt $ n .$. C A .$. Z 10 11toChurch :: Int -> C 12toChurch 0 = zero 13toChurch n = s .$. toChurch (n - 1) 14 15false, true, _if :: C 16false = C (\x -> C (\y -> y)) 17true = C (\x -> C (\y -> x)) 18_if = C (\b -> C (\x -> C (\y -> b .$. x .$. y))) 19 20zero, one, s :: C 21zero = C (\f -> C (\x -> x)) 22one = C (\f -> C (\x -> f .$. x)) 23s = C (\n -> C (\f -> C (\x -> f .$. (n .$. f .$. x)))) 24 25isZero :: C 26isZero = C (\n -> n .$. (C (\x -> false)) .$. true) 27 28add, mult, pre :: C a 29add = C (\m -> C (\n -> C (\f -> C (\x -> m .$. f .$. (n .$. f .$. x))))) 30mult = C (\m -> C (\n -> C (\f -> m .$. (n .$. f)))) 31pre = C (\n -> C (\f -> C (\x -> 32 (n .$. (C (\g -> C (\h -> h .$. (g .$. f)))) .$. (C (\u -> x))) .$. (C (\u -> u))))) 33 34hoge :: C 35hoge = C (\n -> _if .$. (isZero .$. n) .$. one .$. n)

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

Haskell

1toInt $ hoge .$. zero 2toInt $ hoge .$. one 3toInt $ hoge .$. (toChurch 8)

投稿2015/08/14 18:26

編集2015/08/15 00:15
YoshikuniJujo

総合スコア33

バッドをするには、ログインかつ

こちらの条件を満たす必要があります。

0

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

lang

1type Cbool a = a -> a -> a 2type Cnum a = (a ->a) -> a -> a 3 4true :: Cbool a 5true x y = x 6 7false :: a -> a -> a 8false x y = y 9 10not :: Cbool (Cbool a) -> Cbool a 11not x = x false true 12 13zero :: Cnum a 14zero f = id 15 16one :: Cnum a 17one f = f 18 19two :: Cnum a 20two f = f . f 21 22succ :: Cnum a -> Cnum a 23succ cn f = f . cn f 24 25_if :: Cbool a-> a -> a-> a 26_if b x y = b x y 27 28isZero :: (Cnum (Cbool a1)) -> Cbool a1 29isZero n = n (\x -> false) true 30 31f a b c :: (Cnum (Cbool a)) -> a -> a -> a 32f a b c = _if (isZero a) b c 33

投稿2015/03/07 00:59

qoopty

総合スコア15

バッドをするには、ログインかつ

こちらの条件を満たす必要があります。

selpo

2015/03/07 14:29

ありがとうございます。 なんとなくわかってきました。 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とやらを使うしかないのでしょうか。
guest

あなたの回答

tips

太字

斜体

打ち消し線

見出し

引用テキストの挿入

コードの挿入

リンクの挿入

リストの挿入

番号リストの挿入

表の挿入

水平線の挿入

プレビュー

15分調べてもわからないことは
teratailで質問しよう!

ただいまの回答率
85.50%

質問をまとめることで
思考を整理して素早く解決

テンプレート機能で
簡単に質問をまとめる

質問する

関連した質問