20

Haskell で教会の数字を実装しようとしていますが、ちょっとした問題が発生しました。Haskell は無限型について不平を言っています

チェックが発生します: 無限型を構築できません: t = (t -> t1) -> (t1 -> t2) -> t2

引き算をしようとすると。私は自分のラムダ計算が有効であることを 99% 確信しています (そうでない場合は教えてください)。私が知りたいのは、関数で haskell を機能させるためにできることがあるかどうかです。

module Church where

type (Church a) = ((a -> a) -> (a -> a))

makeChurch :: Int -> (Church a)
makeChurch 0 = \f -> \x -> x
makeChurch n = \f -> \x -> f (makeChurch (n-1) f x)

numChurch x = (x succ) 0

showChurch x = show $ numChurch x

succChurch = \n -> \f -> \x -> f (n f x)

multChurch = \f2 -> \x2 -> \f1 -> \x1 -> f2 (x2 f1) x1

powerChurch = \exp -> \n -> exp (multChurch n) (makeChurch 1)

predChurch = \n -> \f -> \x -> n (\g -> \h -> h (g f)) (\u -> x) (\u -> u)

subChurch = \m -> \n -> (n predChurch) m
4

3 に答える 3

30

問題は、ヒンドリー・ミルナー型推論によって正しく推論するには多形性predChurchが高すぎることです。たとえば、次のように書きたくなります。

predChurch :: Church a -> Church a
predChurch = \n -> \f -> \x -> n (\g -> \h -> h (g f)) (\u -> x) (\u -> u)

しかし、このタイプは正しくありません。AChurch aは最初の引数として an を取りますが、2 つの引数関数a -> aを渡しnています。明らかに型エラーです。

問題はChurch a、教会の数字を正しく特徴付けていないことです。教会の数字は単純に数字を表します -- その型パラメータは一体何を意味するのでしょうか? 例えば：

foo :: Church Int
foo f x = f x `mod` 42

それはタイプチェックされますが、foo間違いなく教会の数字ではありません。タイプを制限する必要があります。教会の数字は、特定の だけでなく、どのよう な場合にも機能する必要があります。正しい定義は次のとおりです。aa

type Church = forall a. (a -> a) -> (a -> a)

{-# LANGUAGE RankNTypes #-}このようなタイプを有効にするには、ファイルの先頭にある必要があります。

これで、期待する型シグネチャを与えることができます。

predChurch :: Church -> Church
-- same as before

上位の型は Hindley-Milner によって推論できないため、ここで型シグネチャを指定する必要があります。

しかし、実装しようとするとsubChurch別の問題が発生します。

Couldn't match expected type `Church'
       against inferred type `(a -> a) -> a -> a'

なぜこれが起こるのか、私には 100% 確信が持てませんforall。しかし、それは私を驚かせません。より高いランクの型は、コンパイラに提示する困難のために、少し脆弱になる可能性があります。さらに、抽象化typeに aを使用するべきではなく、 aを使用する必要があります(これにより、定義の柔軟性が高まり、コンパイラの型チェックが容易になり、抽象化の実装を使用する場所がマークされます)。newtype

newtype Church = Church { unChurch :: forall a. (a -> a) -> (a -> a) }

predChurchまた、必要に応じてロールとアンロールを変更する必要があります。

predChurch = \n -> Church $ 
    \f -> \x -> unChurch n (\g -> \h -> h (g f)) (\u -> x) (\u -> u)

と同じsubChurch：

subChurch = \m -> \n -> unChurch n predChurch m

しかし、型シグネチャはもう必要ありません。ロール/アンロールには、型を再度推測するのに十分な情報があります。

newtype新しい抽象化を作成するときは、常に s をお勧めします。私のコードでは、通常typeのシノニムはほとんどありません。

于 2011-07-06T12:55:02.640 に答える
7

この の定義はpredChurch 、単純に型付けされたラムダ計算では機能せず、型付けされていないバージョンでのみ機能します。predChurchHaskell で動作する のバージョンは、こちらにあります。

于 2011-07-06T12:38:00.517 に答える
-1

私は同じ問題に遭遇しました。そして、型シグネチャを追加せずに解決しました。

SICPcons carからコピーしたソリューションを次に示します。

cons x y = \m -> m x y
car z = z (\p q -> p)
cdr z = z (\p q -> q)

next z = cons (cdr z) (succ (cdr z))
pred n = car $ n next (cons undefined zero)

sub m n = n pred m

ここで完全なソースを見つけることができます。

を書いて本当にsub m n = n pred mビックリ、ghciで型エラーなく読み込める！

Haskell コードはとても簡潔です。:-)

于 2012-04-20T15:05:22.253 に答える