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

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

ただいまの
回答率

91.00%

  • Haskell

    48questions

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

  • GHC

    4questions

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

HaskellでChurch numeralの実装

受付中

回答 2

投稿

  • 評価
  • クリップ 1
  • VIEW 1,062

selpo

score 29

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
  • 気になる質問をクリップする

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

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

    クリップを取り消します

  • 良い質問の評価を上げる

    以下のような質問は評価を上げましょう

    • 質問内容が明確
    • 自分も答えを知りたい
    • 質問者以外のユーザにも役立つ

    評価が高い質問は、TOPページの「注目」タブのフィードに表示されやすくなります。

    質問の評価を上げたことを取り消します

  • 評価を下げられる数の上限に達しました

    評価を下げることができません

    • 1日5回まで評価を下げられます
    • 1日に1ユーザに対して2回まで評価を下げられます

    質問の評価を下げる

    teratailでは下記のような質問を「具体的に困っていることがない質問」、「サイトポリシーに違反する質問」と定義し、推奨していません。

    • プログラミングに関係のない質問
    • やってほしいことだけを記載した丸投げの質問
    • 問題・課題が含まれていない質問
    • 意図的に内容が抹消された質問
    • 広告と受け取られるような投稿

    評価が下がると、TOPページの「アクティブ」「注目」タブのフィードに表示されにくくなります。

    質問の評価を下げたことを取り消します

    この機能は開放されていません

    評価を下げる条件を満たしてません

    評価を下げる理由を選択してください

    詳細な説明はこちら

    上記に当てはまらず、質問内容が明確になっていない質問には「情報の追加・修正依頼」機能からコメントをしてください。

    質問の評価を下げる機能の利用条件

    この機能を利用するためには、以下の事項を行う必要があります。

回答 2

0

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

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

投稿

  • 回答の評価を上げる

    以下のような回答は評価を上げましょう

    • 正しい回答
    • わかりやすい回答
    • ためになる回答

    評価が高い回答ほどページの上位に表示されます。

  • 回答の評価を下げる

    下記のような回答は推奨されていません。

    • 間違っている回答
    • 質問の回答になっていない投稿
    • スパムや攻撃的な表現を用いた投稿

    評価を下げる際はその理由を明確に伝え、適切な回答に修正してもらいましょう。

  • 2015/03/07 23: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とやらを使うしかないのでしょうか。

    キャンセル

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

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)

投稿

編集

  • 回答の評価を上げる

    以下のような回答は評価を上げましょう

    • 正しい回答
    • わかりやすい回答
    • ためになる回答

    評価が高い回答ほどページの上位に表示されます。

  • 回答の評価を下げる

    下記のような回答は推奨されていません。

    • 間違っている回答
    • 質問の回答になっていない投稿
    • スパムや攻撃的な表現を用いた投稿

    評価を下げる際はその理由を明確に伝え、適切な回答に修正してもらいましょう。

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

  • ただいまの回答率 91.00%
  • 質問をまとめることで、思考を整理して素早く解決
  • テンプレート機能で、簡単に質問をまとめられる

関連した質問

同じタグがついた質問を見る

  • Haskell

    48questions

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

  • GHC

    4questions

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