2011-07-06 15 views
16

私はハスケルに教会の数字を実装しようとしていますが、私は軽度の問題にぶつかりました。私が試してみて、減算を行うとき> T2haskellの教会数字の減算

- >(T1 - - > T2)T =( - > T1 T):無限の種類を構築することができません:Haskellはチェックを発生

で無限の種類を訴えます。私のラムダ計算が有効であると私は99%肯定的です(そうでなければ教えてください)。私が知りたいのは、自分の仕事でハスケルを働かせるためにできることがあるかどうかです。

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 
+0

型宣言「型教会a =(a-> a) - > a-」を作成する必要があります。そのクリーナー、違いはありません。 – alternative

+0

また、タイプシグネチャを書き出すのに役立ちます。それは問題がどこにあるのかを正確に教えてくれるでしょう... – alternative

+0

ghciが適切に推論できるかどうかを調べるためにタイプシグネチャを削除してしまい、うまくいけばエラーを取り除きます(エラーは変更されていません)...また、私型の周りのかっこを好むそれはそれが私にとってもっと目立つようにします – Probie

答えて

5

のみ型指定されていないバージョンでpredChurchdoesn't work in simply typed lambda calculus、この定義。 Haskell hereで動作するpredChurchのバージョンを見つけることができます。

+0

ありがとう、それは私が探していた答えでした。私は、タイプを気にしないようにするために、私がすることができる何らかの魔法があるかどうか疑問に思っていました。私はすでにhaskellで動作する定義を持っています、私はhaskellで動作する型のないバージョンを得ることができるかどうかを知りたがっています。再度、感謝します。 – Probie

+1

@Probie:最初のビットは単純型のλ計算のみを指しています。多形型、型クラス、 'data'と' newtype'、および再帰的束縛のいずれもせずにハスケルに似ています。 –

25

predChurchであり、多形性がHindley-Milnerタイプ推論によって正しく推定されるという問題があります。たとえば、次のように書いています。

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

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

問題は、Church aが教会の数字を正しく特定できないということです。教会の数字は単純に数字を表しています - その型パラメータはどういう意味ですか?例:

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

このタイプチェックはありますが、fooは確かに教会の数字ではありません。タイプを制限する必要があります。教会の数字は、特定のaだけでなく、のいずれかがaである必要があります。正しい定義は次のとおりです。

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

あなたはこのようなタイプを有効にするには、ファイルの先頭に{-# LANGUAGE RankNTypes #-}を持っている必要があります。上位タイプはヒンドリー - ミルナーによってinferrableされていないため、

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

あなたここに型シグネチャを与える必要があります。

は、今、私たちは私たちが期待する型シグネチャを与えることができます。

我々はsubChurchを実装するために行くときしかし、別の問題が発生する:

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

私はこれがなぜ起こるか、私はforallがあまりにも自由型チェッカーによって展開されていると思うが100%を確認していません。私を驚かせることはありません。上位ランクの型は、コンパイラに与える困難のために少し脆くなることがあります。さらに、抽象度がの場合はtypeを使用しないでください。newtypeを使用する必要があります(定義の柔軟性が向上し、型チェックによるコンパイラの助けとなり、抽象化の実装を使用する場所がマークされます) :

subChurch

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

同じ:

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

そして、我々はロールし、必要に応じて展開するようpredChurchを変更する必要があり

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

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

新しい抽象化を作成する場合は、常にnewtypeをお勧めします。通常のtypeのシノニムは私のコードではまれです。

+2

よく説明! – augustss

+6

'type'エラーについては、Haskellで多型は単相型引数でのみインスタンス化されなければならないので起こります:' type Church = forall a。 (a - > a) - >(a - > a) '型変数' a'は単相性でなければならないが、 'subChurch'定義ではそうではない('(n predChurch) '型変数' a'多型である 'Church'に設定されています)。ここに詳細な説明があります:http://okmij.org/ftp/Haskell/types.html#some-impredicativity –

-1

同じ問題が発生しました。そして私はタイプシグネチャを追加することなくそれを解決しました。

解決策は、conscarSICPからコピーされました。

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 

フルソースhereを見つけることができます。

私は実際にsub m n = n pred mを書いた後に驚き、タイプエラーなしでghciに読み込みます!

ハスケルコードは簡潔です! :-)

+2

これは実際には機能しません。あなたがGHCiで推論された型を見ると、それらはあまりにも特殊です。 'showChurch $ sub(プラス3つの2つ)'は型エラーを出します。 – hammar

+0

@hammar Oooops、あなたは正しいです。私は 'sub two one 'だけをテストしました。 'sub three two'は型エラーを出します。 – wenlong