<譯> 類型與函數

原文見 http://bartoszmilewski.com/20...

上一篇 -> 複合：範疇的本質

類型與函數構成的範疇在編程中擔任着重要的角色。咱們討論一下類型是什麼，爲何須要它。

誰須要類型？

關於靜態 vs 動態，強類型 vs 弱類型，彷佛存在着一些爭論。下面我用一個思想實驗讓這些選擇變得更直觀一些。想象一下，無數只猴子在快樂的隨機敲打着鍵盤，產生程序，編譯，而後運行。

對於機器語言而言，猴子們產生的任何字節的組合都會被計算機接受並運行。咱們應該慶幸，高級的語言，由於有負責檢查詞法與語法錯誤的編譯器的存在，致使大部分猴子由於努力敲打鍵盤卻未獲得香蕉而拂手而去，而剩下的那些猴子胡亂敲打所生成的程序若是能經過編譯，它們更有可能變成有用的程序。類型檢查也提供了一個門檻，能夠攔截無心義的程序。此外，在強類型的靜態語言中，能夠在編譯期間發現類型錯誤，從而在大部分不正確的程序運行以前就幹掉了它們，而動態類型語言只能在運行時進行類型檢查……

那麼，問題就來了，咱們想讓猴子們高興麼，或者咱們想產生正確的程序麼？

這個關於猴子的思想實驗，一般的目標是讓打字的猴子們創做一部莎士比亞全集的。在這個過程當中，若是有拼寫檢查與語法檢查，就能夠提升成功的可能性。類型檢查的比喻具備更重要的意義，由於它能夠肯定，一旦羅密歐被識別爲人類，那麼他就沒法生根發芽長出樹葉或者在他強大的重力場中捕獲光子。

類型關乎複合

範疇論與箭頭的複合有關。可是並不是任意兩個箭頭均可以複合。一個箭頭的目標對象必須與下一個箭頭的源對象相同，這樣的兩個箭頭方能複合。在編程中，咱們將一個函數的返回結果傳遞給另外一個函數。若是目標函數不能正確的解析源函數傳遞來的數據，程序就不會工做。首尾必須相連，方能實現複合。編程語言的類型系統越強，箭頭的配合就越容易描述與檢驗。

我見過惟一的一場反對強類型檢查的嚴肅爭論，認爲它可能會扼殺一些程序，而這些程序在語義上倒是正確的。現實中，這種狀況出現的概率很是之小，而且每一種語言都提供了某種後門，可讓代碼在真正須要的時候經過類型檢查。即便是 Haskell 這樣的語言，也有這種後門。可是這種設施應該謹慎使用。卡夫卡的小說《變形記》中的葛裏高爾，當他變異爲巨大的甲蟲時，打破了類型系統，其結局你們也都看到了。

我見過的另外一場爭論，是認爲類型的處理給程序員帶來巨大的負擔。在不得不爲 C++ 的迭代器寫一些類型聲明的時候，我深有同感。可是有一種技術叫類型推導，它可讓編譯器在須要的時候可以根據上下文推導出大部分類型。在 C++ 中，如今能夠用 auto 變量，其類型具體是什麼就交付給編譯器來肯定。

在 Haskell 中，大部分場合，類型聲明並不是必須。不過 Haskell 程序猿仍是趨向於使用類型聲明，由於他們可讓代碼具備語義，也能使得編譯錯誤更容易理解。Haskell 的實際編程中，每每是在項目的一開始就進行類型設計，而後用類型的聲明驅動程序的實現，最終類型聲明會變成代碼註釋，可是這種註釋對於編譯器是有意義的。

強靜態類型一般用於代替代碼測試。你可能有時聽到 Haskell 程序猿說，『能經過編譯，它就是正確的』。固然，沒人能擔保類型是正確的程序就可以產生正確的輸出。這種騎士般的態度所引起的結果就是，有些人研究發現強類型的 Haskell 在代碼質量方面的進展並無像你們預期的那樣好。不過，在商業軟件開發中，彷佛修復 bug 的壓力只停留在一個特定的質量級別，這個級別介乎軟件開發成本與用戶的容忍限度之間，它與編程語言或編程範式的關係不太大。更好的評價指標應該是檢查有多少項目延期交付了，或者有多少項目在大幅消減了函數式編程範式以後它及時交付了。

至於單元測試可以替代強類型檢查方面也有一些爭論，考慮一下強類型語言中的常見的重構行爲：改變一個函數的參數類型。在強類型語言中，修改函數的聲明就能夠修復全部的構建錯誤。在弱類型語言中，函數的變化卻沒法傳播到它被調用的地方。單元測試雖然可以捕捉到一些錯誤，可是測試老是機率意義上的，而不是一個肯定的過程。測試是一種貧弱的證實。

類型是什麼

對於類型，最簡單的直覺就是它是值的集合。Bool 類型（記住，Haskell 中具體類型是大寫字母開頭）是一個含有 2 個元素 True 與 False 的集合。Char 類型是全部 Unicode 字符的集合。

集合多是有限或無限的。String 類型，它與 Char 列表同義，它就是個無限集的例子。

當咱們將 x 聲明爲 Integer 時：

x :: Integer

咱們想說的是，x 是一個整型數集中的一個元素。在Haskell 中，Integer 是無限集，它可以用於任意精度的算術。還有個有限集，叫 Int，它與機器類型有關，就像 C++ 的 int。

有一些微妙的東西，可使得類型與集合的定義更爲精巧。好比多態函數存在一些問題，由於事實上你不可能擁有一個全部集合的集合。可是我承諾過，我不會過於數學化。集合的範疇是個偉大的概念，它的名字就叫作 Set，咱們之後只在它上面工做。在 Set 中，對象是集合，態射（箭頭）是函數。

Set 是個很是特殊的範疇，由於咱們實際上只能從它的內部拮取一些對象，並經過操做這些對象來認識它。例如，咱們知道空集不包含任何元素。咱們知道存在只含有一個元素的集合。咱們知道函數能夠將一個集合中的元素映射到另外一個集合。它們也能將兩個元素映射爲一個，可是卻不能將一個元素映射爲 2 個。咱們還知道恆等函數能夠將一個元素映射爲自己，等等。如今咱們不妨將逐步忘記這一切，去使用純粹的範疇論語言——對象與箭頭——去表達這些概念。

在理想世界中，咱們能夠說 Haskell 的數據類型是集合，Haskell 的函數是集合之間的數學函數。只不過有個小問題：數學函數不可被執行——它只知道答案。Haskell 函數必需要計算出答案。若是答案能夠在有限步驟中被計算出來，這不是什麼問題，然而步驟的數量可能會很大。有些計算是遞歸的，它可能永遠不會終止。在 Haskell 中咱們不能阻止停不下來的函數，由於這就是著名的停機問題。這就是爲何計算機科學家搞出來一個聰明的點子，也能夠說是一個巨大的 hack，這取決於你的視角；他們爲每一種類型增長了一個特殊值，叫作底（Bottom），用符號表示爲 _|_，也能夠用 Unicode 字符 ⊥。這個『值』與無休止計算有關。所以，若一個函數聲明爲：

f :: Bool -> Bool

它能夠返回 True，False 或 _|_；後者表示它不會終止。

有趣的是，一旦你接受了將底做爲類型系統的一部分，就能夠將每一種運行時錯誤做爲底來對待，甚至能夠允許函數顯式地返回底——一般用於未定義的表達式，例如：

f :: Bool -> Bool
f x = undefined

這種類型的定義之因此能經過類型檢查，是由於 undefined 的求值結果是底，而底能夠是任何類型的值，因此它也是 Bool 類型的值。甚至，你能夠這樣不要那個 x，即：

f :: Bool -> Bool
f = undefined

由於底也是類型 Bool->Bool 這種類型的值。

能夠返回底的函數被稱爲偏函數，與全函數相對，後者老是對於每種可能的參數值返回有效的結果。

因爲底的存在，你將會看到 Haskell 類型與函數的範疇會被稱爲 Hask，而不是 Set。從理論上來看，這是致使出現無休止的複雜性的源頭，所以在這一點我要動用個人庖丁之刀將複雜砍掉。從實用的角度來看，不理睬無休止的函數與底是沒有問題的，將 Hask 視爲一個友善的 Set 便可（詳見本文末尾的參考文獻）。

爲什麼咱們須要一個數學模型？

身爲程序猿，你所熟悉的是編程語言的語法。編程語言的各個方面在這門語言誕生之初是經過形式化標記描述的。可是語言的語義卻很難描述，有時用一本挺厚的書來描述，可能也沒法完整的說清楚。所以，語言專家們之間的討論永無休止，那些講解語言的工業化標準的書籍已經汗牛充棟了。

有些形式化工具可描述語義，可是因爲它們太複雜了，以致於只是在一些簡化的學院級語言中使用了它們。此類工具中，有一個工具叫作操做語義（operational semantic），它描述的是程序的執行機制。它定義了形式化理想化的解釋器。工業級語言的語義，相似 C++，用的是非正式的操做語義，稱之爲『抽象機器』。

使用操做語義存在的問題是要難以證實程序的正確性。要展示一個程序的性質，你只能在一個理想化的解釋器中去『運行』它。

不要緊，反正程序猿不須要去形式化的證實程序的正確性。咱們老是『思考』咱們在寫正確的程序。沒有人在鍵盤前說，『呃，我隨手寫幾行代碼，看看會發生什麼』。咱們思考的是，咱們所寫的代碼會擁有正確的行爲，產生咱們想要的結果。一旦程序作不到這些，咱們一般會至關驚訝。這意味着，咱們在寫代碼的時候沒有對程序進行推導，只是在寫完後纔在本身的大腦中的解釋器中運行它的時候才進行正確性推導。這樣作的問題是很難跟蹤全部的變量。計算機善於運行程序，人類卻不能！若是咱們能，就不必發明計算機了。

可是，還有一種選擇，它叫指稱語義（Denotational semantic），是基於數學的。在指稱語義中，每一個編程結構都會被給出數學解釋。使用它，若是你想證實程序的正確性，只須要證實一個數學定理。你可能以爲數學定理的證實是很難的，可是咱們人類創建數學方法已經上千年了，所以有大量的知識資源能夠利用。還有，與數學家所證實的那些定理相比，咱們在編程中遇到的問題一般是至關簡單的，生僻的問題不多。

Haskell 是符合指稱語義的語言，考慮用 Haskell 定義一個階乘函數：

fact n = product [1..n]

表達式 [1..n] 是一個從 1 到 n 的整型數列表。product 函數能夠將列表中的全部元素相乘。這跟數學課本里的階乘幾乎別無二致。與 C 代碼相比較：

int fact(int n) {
    int i;
    int result = 1;
    for (i = 2; i <= n; ++i)
        result *= i;
    return result;
}

還要我多說什麼？

好吧，我首先得認可我有點惡意中傷！階乘函數自己就有着明確的數學定義。敏銳的讀者可能會問：從鍵盤讀取字符或者經過網絡發送數據包，它們有數學模型麼？在很是漫長的時間裏，此類問題一直都是很尷尬的問題，答案只能是彎彎繞的那種。彷佛指稱語義不能極好的應用於一些重要的任務，而編程原本就是圍繞這些任務而生。操做語義很容易勝任這些任務。直到範疇論的出現才找到擺脫這種尷尬境地的突破口。Eugenio Moggi 發現可經過單子完成此類任務，這一發現不只扭轉了乾坤，使得指稱語義大放異彩，並使得純函數式程序變得更爲有用，也使得傳統的編程範式綻開出新的光芒。單子，咱們之後在發展更多的範疇論工具時再予以探討。

對於編程而言，擁有一個數學模型的重要的優勢就是可以對軟件的正確性給予形式化證實。這對於寫消費級軟件來講可能不是過重要，可是有些領域，失敗的代價至關高，甚至會出人命。不過，事實上當你爲健康系統寫網絡應用程序時，你可能會欣賞具備正確性證實的 Haskell 標準庫中的函數與算法。

純函數與髒函數

在 C++ 或其餘命令式語言中，咱們稱之爲函數的東西，與數學上被稱爲函數的東西是不一樣的。數學上的函數是值到值的映射。

在編程語言中，咱們可以實現數學上的函數：一個函數，給它一個輸入值，它就計算出一個輸出的值。一個平方函數就是輸入值自身的乘積。每次被調用時，對於相同的輸入，它老是能保證產生一樣的輸出。一個數的平方不會隨着月相的變化而變化。

再者，計算一個數的平方也不會對你的狗糧配方有反作用。若是有一個『函數』就是對你的狗糧配方有反作用，那麼它的模型就與數學裏的函數存在很大差別。

在命令式語言中，給予相同輸入老是能獲得相同輸出的函數，被稱爲純函數。在一種純函數式語言中，例如 Haskell，全部的函數都是純的。正是由於這一點，Haskell 更易於賦予語言以指稱語義，並使用範疇論進行建模。對於其餘語言，也能夠構造出一個純的子集，或者對反作用謹慎對待。之後咱們將會看到單子是如何只藉助純函數來對各類反作用進行建模的。總之，咱們用數學函數來約束本身，可是卻沒有任何損失。

類型的示例

一旦意識到類型是集合，你就能夠思考一些至關生僻的類型。例如，空集這種類型是什麼？在 Haskell 中，空集是 Void，雖然 C++ 中也有個 void，但它倆不是一回事。Haskell 中的 Void 是一個不存儲任何值的類型。你能夠定義一個接受 Void 的函數，可是你永遠沒法調用它。由於，要調用這個函數，必須向它提供一個 Void 類型的值，但這種類型的值並不存在。至於這個函數的返回值，不須要做任何限制。它能夠返回任何類型，反正它根本沒有機會運行。換句話說，它是一個具備多態返回類型的函數。Haskell 程序員將其命名爲：

absurd :: Void -> a

記住，a 是一個類型變量，它可接受任何類型。函數的名字不太相符。這種類型與函數，在邏輯學上有更深刻的解釋，它們被稱爲 Curry-Howard 自同態。Void 類型表示謊話，absurd 函數的類型至關於『由謊話能夠推出任何結論』，也就是邏輯學中所謂的『爆炸原理』。

下一個類型至關於單例集合。它是隻有一個值的類型。你可能意識不到，它實際上就是 C++ 中的 void。考慮那些輸入是 void 以及返回是 void 的函數。一個輸入是 void 的函數老是可以被調用。若是它是純函數，它就老是能返回相同的結果。例如：

int f44() { return 44; }

你可能認爲這種函數沒有輸入。可是剛纔咱們已經見識了，一個函數若是不接受任何值，它永遠也沒法被調用。那麼，這個 f44 接受了什麼？從概念上說，它接受了一個空值，並且不會再有第 2 個空值，所以咱們就不必再顯式的說起它。然而 haskell 爲空值提供了一個符號，即空的序對 ()。所以就有了搞笑的巧合（真的是巧合嗎？），輸入爲 void 的函數，C++ 與 Haskell 的版本看上去是相同的。不過，在 Haskell 中，() 也能夠用在類型、構造子上。f44 的 Haskell 版本以下;

f44 :: () -> Integer
f44 () = 44

第一行代碼描述了 f44 接受 () 類型（這個類型讀做『unit』），將其映射爲 Integer 類型。第二行代碼是經過 unit 的構造子 () 的模式匹配來定義 f44。只要你提供 unit 的值 () 就能夠調用這個函數：

f44 ()

注意，每一個 unit 函數都等同於從目標類型中選取一個值的函數（在此，就是選擇 Integer 類型的值 44）。實際上，你能夠將 f44 做爲數字 44 的另外一種表示方法，所以這也是如何經過與函數（箭頭）的交互來代替集合中一個顯式的元素的示例，也就是說數據與計算過程的本質上是沒有區別的。從 unit 到類型 A 的函數至關於集合 A 中的元素。

讓函數返回 void 類型會怎樣，或者說，在 Haskell 中，讓函數返回 unit 會怎樣？在 C++ 中，這樣的函數一般擔當具備反作用的函數，可是咱們知道這種函數並不是數學意義上的函數。一個返回 unit 的純函數，它什麼也不作，或者說，它惟一作的就是丟棄它所接受的輸入。

在數學上，一個從集合 A 到單例集合的函數會將 A 中的每一個元素映射爲單例集合中的元素。對於每一個 A 都存在這樣的函數。例如對於 Integer，有：

fInt :: Integer -> ()
fInt x = ()

你向這個函數提供任何整數，它都會給你返回一個 unit。本着簡明扼要的精神，Haskell 容許你使用通配符模式，能夠用下劃線來替代要忽略的輸入。這樣你就不須要再爲它從新弄個名字。上述函數可改寫爲：

fInt :: Integer -> ()
fInt _ = ()

注意，這個函數的實現不只不依賴傳給它的參數，它也不依賴參數的類型。

對於任意類型都具備相同形式的函數，稱爲參數型多態。用類型變量來代替一個具體的類型，就能夠實現一個函數族。咱們要怎麼稱呼一個從任意類型到 unit 的函數？固然，要稱它爲 unit：

unit :: a -> ()
unit _ = ()

在 C++ 中，你能夠這樣來寫：

template<class T>
void unit(T) {}

咱們的類型學裏的下一個類型是二元集合。在 C++ 中，這個集合被稱爲 bool，在 Haskell 中則稱爲 Bool。兩者的區別是，C++ 的 bool 是內建類型，而 Haskell 的則能夠自行定義：

data Bool = True | False

這個定義得這麼讀：Bool 要麼是 True，要麼是 False。理論上，C++ 也能夠用枚舉來定義一個 Bool 類型：

enum bool {
    true,
    false
};

可是 C++ 的 enum 的類型本質上是整型。C++ 11 的 enum class 卻是自成一類了，不過你確定不想這樣來用布爾值：bool::true 與 bool::false，並且還要在代碼中包含定義了這一類型的頭文件。

輸出 Bool 的函數被稱爲謂詞。例如，Haskell 庫 Data.Char 充滿了相似 isAlpha 或 isDigit 這樣的謂詞。在 C++ 中，也有各種似的庫，它也定義了 isalpha 與 isdigit 以及其餘類似的方法，不過它們的返回值是 int 類型，而不是布爾類型；真正的謂詞被定義爲 ctype::is(alpha, c)，ctype::is(digit, c) 之類。

挑戰

1. 用你最喜歡的語言，定義一個高階函數（或函數對象）memoize。這個函數接受一個純函數 f，返回一個行爲與 f 近乎相同的函數 g，可是 g 只是第一次被調用時與 f 的功能相同，而後它在內部將結果存儲了起來，後續再用一樣的參數調用它，它只返回本身存儲的那個結果。你能夠經過觀察 f 與 g 的運行效率來區分它們。例如，讓 f 是一個須要耗費挺長時間才能完成計算的函數，這樣，當第一次調用 g 的時候，它會運行的很慢，可是用一樣的參數對 g 再次調用，則能夠當即獲得結果。

2. 標準庫中用於生成隨機數的函數，可以被 memoize 麼？

3. 大多數隨機數生成器都可以用一個種子進行初始化。請實現一個可以接受種子的函數，這個函數可將種子轉交給隨機數生成器，而後返回所得結果。這個函數能被 memoize 麼？

4. 下面的 C++ 函數，哪個是純的？試着去 memoize 它們，而後屢次調用後看看會發生什麼：能被 memoize 仍是不能。

(1) 文中的階乘函數。

(2) std::getchar()

(3) bool f() {
        std::cout << "Hello!" << std::endl;
        return true;
    }
    
(4) int f(int x)
    {
        static int y = 0;
    y += x;
    return y;
    }

5. 從 Bool 到 Bool 的函數有多少中？你能夠將它們都實現出來麼？

6. 將 Void，()（unit）以及 Bool 做爲對象，將與這些類型相關的全部函數做爲箭頭，你能畫出一個範疇麼？用函數名來標註箭頭。

參考文獻

1. Nils Anders Danielsson, John Hughes, Patrik Jansson, Jeremy Gibbons, Fast and Loose Reasoning is Morally Correct. This paper provides justification for ignoring bottoms in most contexts.

-> 下一篇：『範疇，可大可小』