是否可以使用迭代增量在鍵入的教會數字上實現加法？

我找不到一種方法來將增加定義爲重複增量，儘管這可能是一種無類型的語言。這裏是我的代碼：是否可以使用迭代增量在鍵入的教會數字上實現加法？

{-# LANGUAGE RankNTypes #-} 
type Church = forall a . (a -> a) -> (a -> a) 

zero :: Church 
zero = \f -> id 

inc :: Church -> Church 
inc n = \f -> f . n f 

-- This version of addition works 
add1 :: Church -> Church -> Church 
add1 n m = \f -> n f . m f 

-- This version gives me a compilation error 
add2 :: Church -> Church -> Church 
add2 n m = n inc m

編譯錯誤我得到add2是

Couldn't match type `forall a1. (a1 -> a1) -> a1 -> a1' 
        with `(a -> a) -> a -> a' 
    Expected type: ((a -> a) -> a -> a) -> (a -> a) -> a -> a 
     Actual type: Church -> (a -> a) -> a -> a 
    In the first argument of `n', namely `inc' 
    In the expression: n inc m 
    In an equation for `add2': add2 n m = n inc m

爲什麼這是一個錯誤？ Church是不是((a->a) -> a -> a)的同義詞？

來源

2014-05-16 hugomg

您可能還喜歡[this recent question]（http://stackoverflow.com/q/23532659/791604）。 –

對於實際使用，我推薦'newtype'而不是類型同義詞。 – PyRulez

我無法讓您的代碼輸入，無論我添加了多少額外的類型註釋，儘管可能我不夠聰明。（我也嘗試添加ImpredicativeTypes）我覺得這裏的問題是，在定義

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

a只能與秩0類型實例化（即無內foralls），本身是沒有哪個Church 。所以你不能將這樣定義的教會數字應用於你的inc。

但是，有一個相對簡單的解決方法，它稍微冗長，但會使所有事情都很好地工作：使Church成爲新類型而不是類型，因此可以將其視爲單體。以下全部作品：

{-# LANGUAGE RankNTypes #-} 
newtype Church = Church { runChurch :: forall a . (a -> a) -> (a -> a) } 

zero :: Church 
zero = Church (\f -> id) 

inc :: Church -> Church 
inc n = Church (\f -> f . runChurch n f) 

add2 :: Church -> Church -> Church 
add2 n = runChurch n inc

來源

2014-05-17 03:30:43

我認爲單形不是正確的單詞; 'a'只能用_rank-0_類型實例化。 – leftaroundabout

@leftaroundabout我明白了。我一直認爲這些術語幾乎是同義詞，但我想如果它仍然包含一個類型變量，它並不是真正的單形態。 –

是否可以使用迭代增量在鍵入的教會數字上實現加法？

回答

相關問題