瞭解函數式編程中的遞歸代數類型

嘿，我很難理解遞歸代數類型如何工作以及如何正確使用它們。例如，採取下面的RAT定義自然數：瞭解函數式編程中的遞歸代數類型

data Nat = Zero | Succ Nat

我們在這裏使用的RAT，因爲設定值的需求是無限的，我知道這個原理是在表達方面的每一個新的價值前一個，但我不明白這是如何形成自然數的。有人會介意清理嗎？由於

來源

2012-03-31 user1058210

用'1 +'翻譯'Succ'。對於適當的操作次數，每個自然數爲1 +（1 +（...（1 + 0）...））。 – 2012-03-31 13:21:26

這說明：

Nat是一種類型。
Zero有類型Nat。這代表自然數0
如果n有類型Nat，然後Succ n已鍵入Nat。這代表自然數n +1。

因此，舉例來說，Succ (Succ Zero)表示2時，Succ (Succ (Succ Zero))表示3，Succ (Succ (Succ (Succ Zero)))表示4，等等。（從0和接班人定義自然數的這一系統被稱爲Peano axioms。）

事實上，Zero和Succ只是特殊類型的函數（構造函數）被宣佈創建Nat值：

Zero :: Nat 
Succ :: Nat -> Nat

從普通功能不同的是，你可以把他們分開與模式匹配：

predecessor :: Nat -> Nat 
predecessor Zero = Zero 
predecessor (Succ n) = n

這對於遞歸代數數據類型來說並不特別，當然，這只是代數數據類型;但代數數據類型可以具有與其中一個字段相同類型的值的簡單事實是在此創建遞歸的原因。

來源

2012-03-31 13:21:09 ehird

謝謝你這個明確答案ehird！那麼Succ構造函數是一個代表n + 1的內置函數嗎？我很困惑，因爲我認爲這只是以正常的方式宣佈另一個可能的價值。如果我們有一個數n，爲什麼我們要表示值n + 1，即自然數序列中的下一個值？我們不關心我們如何表達價值n嗎？感謝最後的模式匹配位 - 這非常有用！ – user1058210 2012-03-31 13:43:25

不，它不是內置的;你可以將它重命名爲「Fnarf」，它會完全一樣。我們的想法是，我們定義這個類型，並將它的每個值賦給一個*意義*作爲自然數：我們*表示*類型的數據。 'Succ n'代表* n * + 1，因爲* n *必須用* another *'Nat'表示。如果你有'零'（0），並且你想要1，你必須使用'Succ Zero'來表示0 + 1 = 1.如果你有'Succ Zero'（1），並且你想要2，使用Succ（Succ Zero）來表示1 + 1 = 2 ...等等。 – ehird 2012-03-31 13:50:46

@ user1058210不，Succ不是內置的。這只是你給構造函數的名字。你需要一種從'n'到'n + 1'的方式，所以你可以表示任何數字。如果定義只是「數據Nat =零」，則只能表示零。當然，你可以將它擴展到更多的數字，如'數據Nat = Zero | One |兩個'，但這種方法只給你一個有限數量的數字。使用Succ，您可以將'Succ'應用到'Zero'' n'次來表示數字'n'。 – sepp2k 2012-03-31 13:51:14

瞭解函數式編程中的遞歸代數類型

回答

相關問題