haskellの教会数字の減算

Question

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

- >（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 

Answer 1

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

Answer 2

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のシノニムは私のコードではまれです。

Answer 3

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

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

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に読み込みます！

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