哈斯克爾教會數字減法

我正試圖在哈斯克爾實現教會數字，但我遇到了一個小問題。 Haskell的抱怨無限型與哈斯克爾教會數字減法

的發生檢查：無法構造無限類型：T =（T - > T1） - 當我嘗試做減法> T2

- >（T1 - > T2）。我99％肯定我的lambda微積分是有效的（儘管如果不是，請告訴我）。我想知道的是，是否有任何事情可以讓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

來源

2011-07-06 Probie

你應該做的類型聲明'型教會=（A - > A） - > A - >了'。它更乾淨，沒有不同。 – alternative

另請注意，它有助於寫出類型簽名。它會告訴你究竟問題出在哪裏...... – alternative

我最終刪除了類型簽名，看看ghci是否可以正確推斷它們，並希望擺脫錯誤（錯誤沒有改變）...另外，我更喜歡這個類型的括號。這使得它更加脫穎而出 – Probie

這個定義的predChurchdoesn't work in simply typed lambda calculus，只有在非類型化版本。你可以找到一個在Haskell here工作的predChurch版本。

來源

2011-07-06 12:38:00

謝謝，那是我正在尋找的答案。我只是想知道是否有某種魔法可以讓haskell不關心這種類型。我已經有了一個可以在haskell中工作的定義，我只是想知道我是否可以讓這個untyped版本在haskell中工作。再次感謝。 – Probie

@Probie：請記住，第一位僅是指簡單類型的λ演算，這是類似於哈斯克爾沒有任何的：多態類型，類型類，'data'和'newtype'和遞歸綁定。 –

問題是predChurch是太多態性由Hindley-Milner類型推斷正確推斷。例如，人們很容易寫：

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

但這種類型是不正確的。 A Church a將第一個參數設爲a -> a，但您傳遞的是n兩個參數函數，顯然是一個類型錯誤。

問題是，Church a沒有正確描述教會的數字。教會的數字只是一個數字 - 這個類型參數究竟意味着什麼？例如：

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

這typechecks，但foo肯定不是一個教會的數字。我們需要限制類型。教會數字需要爲任何a工作，而不僅僅是一個特定的a。正確的定義是：

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

你需要有{-# LANGUAGE RankNTypes #-}在文件的頂部，使種這樣。

現在我們可以給類型簽名我們預計：

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

您必須這裏舉一個類型簽名，因爲較高等級的類型不被辛德米爾納inferrable。

然而，當我們去實現subChurch產生了另一個問題：

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

我不是100％肯定，爲什麼出現這種情況，我認爲forall正在被typechecker過於隨意展開。儘管如此，我並不感到意外;由於它們向編譯器呈現的困難，更高等級的類型可能有點脆弱。此外，我們不應該使用type作爲抽象，我們應該使用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

但我們並不需要類型簽名了 - 沒有在卷/ UNROLL再次推斷類型的足夠信息。

我總是建議newtype S創建一個新的抽象時。定期type同義詞在我的代碼中很少見。

來源

2011-07-06 12:55:02 luqui

很好解釋！ – augustss

至於'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

我遇到了同樣的問題。我解決了它，但沒有添加類型簽名。

以下是解決方案，其中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中載入它沒有類型的錯誤！

Haskell代碼是如此簡潔！ :-)

來源

2012-04-20 15:05:22 wenlong

這不是真的有效。如果您查看GHCi中的推斷類型，它們就太專業化了，例如， 'showChurch $ sub（加上三個兩個）兩個'給出類型錯誤。 – hammar

@hammar Oooops，你是對的。我只測試了「sub two one」。 '三三二'給出類型錯誤。 – wenlong

哈斯克爾教會數字減法

回答

相關問題