<譯> 函數類型

時間 2019-11-07

標籤函數類型简体版

原文原文鏈接

-> 上一篇：《函子性》編程

譯註：因爲距離上一章翻譯的時間過久，因此有些內容可能有點不太相符。等我翻譯完下一篇，再找時間校對一下。segmentfault

到如今爲止，我已屢次語焉不詳的提到函數類型。函數類型有別於其餘類型。數據結構

以 Integer 爲例，它是整數的集合。Bool 是兩個元素構成的集合。然而一個函數類型 a -> b 的內涵要更大一些，它是從 a 到 b 的全部態射構成的集合。從一個對象到一個對象的態射所構成的集合，叫 hom-集。只有在集合的範疇中，hom-集自身也是一個對象——hom-集是一個集合。編程語言

對於其餘範疇而言，hom-集會造成一個外部範疇。於是，這樣的 hom-集被稱爲外 hom-集。函數式編程

集合的範疇的自引用屬性使得函數類型變得有些特殊。可是，至少在某些範疇中，有一種方法能夠構造 hom-集這樣的對象。這種 hom-集被稱爲內 hom-集。函數

泛構造

暫時忘掉函數類型是集合這回事，咱們先着手嘗試去構造一個函數類型，或者從廣義上說，去構造一個內 hom-集。像之前那樣，咱們能夠從集合的範疇尋找線索，只需不觸碰任何與集合有關的性質便可，這樣所獲得的結果對於其餘範疇也是適用的。工具

可將函數類型視爲一種複合類型，由於它描述的是一個參數類型（Argument Type）與結果類型（Result Type）之間的關係。以前咱們見過這種複合類型的構造——那些包含了對象之間的關係的東西。咱們用泛構造定義過積類型與餘積類型。可使用一樣的技巧來定義函數類型，前提是需給出能夠聯繫三種對象的模式。這三種對象分別是：咱們要構造的函數類型，參數類型及結果類型。spa

顯然，聯繫這三種類型的模式就是函數應用（Function Application）或求值。對於函數類型，假設存在一個候選者 z（注意，在非集合的範疇中，z 只不過是個普通的對象），設參數類型爲 a（一個對象），函數『應用』可將 z 與 a 構成的序對映射爲結果類型 b（一個對象）。如今，咱們有三個對象了，它們中有兩個是固定的（一個是參數類型，另外一個是結果類型），剩下的那個就是『應用』。scala

『應用』是一種映射，咱們該如何將它融入到咱們剛纔所創建的模式之中？若是容許查看對象的內部，那麼咱們就能夠將一個函數 f（z 的一個元素）與參數 x 封裝爲序對，而後將這個序對映射爲 f x（f 做用於 x，所得結果就是 b 的一個元素）。

在集合的範疇中，能夠從 z 這個函數集合中拮取一個函數 f，而後再從 a（類型）中拮取一個 x 做爲參數，而後就能夠獲得 b （類型）中的一個元素 f x。

只是能處理單個的序對 (f, x) 是沒有多少意思的，咱們要處理的是函數類型的候選者 z 與參數類型 a 的積，即 z × a。這個積是一個對象，能夠選擇從這個對象到 b 的一個箭頭 g 做爲態射，g 也就是『應用』。在集合的範疇中，g 就是將每一個 (f, x) 映射爲 f x 的函數。

這樣，咱們就創建起了這樣一個模式：對象 z 與對象 a 的積，經過態射 g 被關聯到另外一個對象 b。

對象與態射構成的模式，它是函數類型的泛構造的起點。

要利用泛構造技巧來清晰的刻畫函數類型，這樣的模式夠用麼？這個模式不適於全部範疇，可是對於咱們感興趣的那些範疇，它夠用了。還有一個問題：定義一個函數類型，必須事先定義積類型嗎？有些範疇是不可積的，或者並不是全部成對的對象都能構成積。這個問題的答案是不行，若是沒有積類型，就沒有函數類型。等下文在討論指數時再來談這個問題。

如今回顧一下泛構造。咱們以對象與態射構成的模式爲起點，它是一種不精確的查詢，一般會命中不少東西。特別是在集合的範疇中，幾乎每同樣東西都與其餘東西具備相關性。咱們能夠拮取任意一個對象 z，將其與 a 造成積，再找個函數將積映射爲 b（除非 b 是空集）。

這樣，咱們的祕密武器——排名（Ranking）就派上了用場，就是檢查一下是否是在函數類型的候選者之間存在惟一的映射——能夠因式化泛構造的映射。當且僅當存在一個惟一的從 z' 到 z 的映射，使得 g' 可由 g 的因式來構造，便可斷定伴隨態射 g（從 z×a 到 b）的 z 比伴隨 g' 的候選者 z' 更好。（提示：請結合下圖來閱讀這段文字。）

在函數類型的候選者中創建排名機制

如今到了須要技巧的部分了，這也是我一直故意拖延着不談這種特殊的泛構造的緣由。假設存在態射 h:: z' -> z，咱們想得到從 z'×a 到 z×a 的態射。因爲積類型是具備函子性的，所以就知道該怎麼作了。因爲積類型自己是一個函子（更確切的說，是二元自函子），所以能夠提高一對態射。也就是說，咱們不只能定義對象的積，也能定義態射的積。

因爲不須要改變 z'×a 這個積的第二個成員 a，所以咱們要提高的態射序對是 (h, id)，其中 id 是做用於 a 的恆等態射。

如今咱們能夠創建『應用』的因式了，將 g' 表示爲 g 的因式：

g' = g ∘ (h × id)

這裏，關鍵之處在於態射積的做用（譯註：它扮演了一個係數的角色）。

泛構造的第三個步就是選出最好的那個候選者——咱們稱之爲 a⇒b（在這裏，將它視爲一個對象的名字便可，不要與 Haskell 類型類的約束符號混淆，下文會給出其餘命名方式）。這個對象伴隨的『應用』——從 (a⇒b)×a 到 b 的態射——咱們稱之爲 eval。若是其餘候選者所對應的『應用』g 都能由 eval 的『因式』被惟一的構造出來，那麼 a⇒b 就是最好的那個候選者。

泛函數對象的定義。此圖與上面那副圖相同，可是如今 a⇒b 是『泛』的。

形式定義以下：

一個從 a 到 b 的函數對象是伴隨着態射

eval :: ((a⇒b) × a) -> b`

的 a⇒b，它對於伴隨着態射

g :: z × a -> b

的任意其餘對象 z 而言，存在惟一的態射

h :: z -> (a⇒b)

g 可表示爲 h 與 eval 所構成的因式：

g = eval ∘ (h × id)

雖然不能擔保對於某個範疇中的任意的對象 a 與 b 都存在着 a⇒b，可是對於集合的範疇卻老是存在着這樣的 a⇒b，而且在集合的範疇中，a⇒b 與 Hom-集 Set(a,b) 同構。這也是爲什麼在 Haskell 中咱們將函數類型 a -> b 解釋爲範疇意義上的函數對象 a⇒b 的緣由。

柯里化

如今再次觀察函數類型的全部候選者。不過，此次咱們將態射 g 視爲兩個變量 z 與 a 的函數：

g :: z × a -> b

一個接受積類型的態射與一個接受兩個變量的函數很類似。特別是在集合的範疇中，g 是接受值的序對的函數，其中一個值來自集合 z，另外一個來自集合 a。

另外一方面，泛性質告訴咱們，對於每一個這樣的 g，都存在惟一的態射 h——將 z 映射爲一個函數類型 a⇒b：

h :: z -> (a⇒b)

在集合的範疇中，這偏偏意味着 h 是一個接受 z 類型並返回一個從 a 到 b 的函數的函數。也就是說，h 是一個高階函數。所以這種泛構造在「接受兩個變量的函數」與「接受一個變量並返回函數的函數」之間創建了壹壹對應的關係。這種對應關係叫作柯里化，而且 h 叫作 g 的柯里化版本。

這種對應關係一對一的，由於對於任意 g 都存在惟一的 h，而對於任意的 h，老是能重建一個接受 2 個參數的函數 g，即：

g = eval ∘ (h × id)

可將函數 g 稱爲 h 的反柯里化版本。

柯里化是 Haskell 內建的語法。返回一個函數的函數：

a -> (b -> c)

常常被視爲一個接受兩個參數的函數，也就是將上述的函數簽名中的括號去掉，即：

a -> b -> c

接受多個參數的函數，這種解釋比較符合咱們的直覺。例如：

catstr :: String -> String -> String
catstr s s’ = s ++ s’

這個函數也能夠表示爲下面的形式——接受一個參數而後返回一個函數（匿名函數）的函數：

catstr’ s = \s’ -> s ++ s’

這兩種定義是等價的，而且兩者均可以部分應用於 1 個參數，結果產生一個單參數的函數，例如：

greet :: String -> String
greet = catstr 「Hello 「

嚴格的說，接受 2 個參數的函數，它本質上接受的是一個序對（積類型）：

(a, b) -> c

這兩種形式的相互轉換有點微不足道，有兩個函數能夠實現它們的相互轉換。沒什麼可奇怪的，這兩個函數分別叫 curry 與 uncurry：

curry :: ((a, b)->c) -> (a->b->c)
curry f a b = f (a, b)

uncurry :: (a->b->c) -> ((a, b)->c)
uncurry f (a, b) = f a b

注意，curry 是函數類型泛構造的因子生成器，將其寫爲下面的形式會更清晰一些（譯註：我卻愈來愈以爲混亂了！）：

factorizer :: ((a, b)->c) -> (a->(b->c))
factorizer g = \a -> (\b -> g (a, b))

因式生成器基於候選者生成因子 eval。

在非函數式語言中，例如 C++，能夠實現柯里化，但不是那麼簡單。可將 C++ 中的多參數函數視爲接受元組（Tuple）的 Haskell 函數（儘管有些東西至關混亂，在 C++ 中能夠定義顯式接受 std::tuple 的函數，也能夠定義變參函數，還能夠定義接受已初始化的列表的函數）。

藉助模板 std::bind，可實現 C++ 函數的部分應用。例以下面接受兩個字符串的函數：

std::string catstr(std::string s1, std::string s2) {
        return s1 + s2;
}

可基於這個函數定義接受一個字符串的函數：

using namespace std::placeholders;

auto greet = std::bind(catstr, "Hello ", _1);
std::cout << greet("Haskell Curry");

雖然 Scala 要比 C++ 或 Java 更加的函數化，可是它卻作不到函數的部分應用。若是你預期本身所定義的函數將會被部分應用，不得不借助多參數列表：

def catstr(s1: String)(s2: String) = s1 + s2

庫的做者對於這部分函數的定義須要具備前瞻性。

指數

在數學領域，從對象 a 到對象 b 的函數或內 hom-對象（hom-集合中的對象）一般稱爲指數，表示爲 $b^a$。注意，函數參數類型位於指數的位置。這種形式看上去會很奇怪，可是當你瞭解了函數與積的關係時，就能領會這種形式的美妙之處。咱們已經見識了必須藉助積來實現內 hom-對象的泛構造，然而函數與積還有更深的聯繫。

考慮一下那些創建在有限類型——值的數量爲有限的類型，例如 Bool, Char, 甚至 Int 或 Double 之上的函數。至少在理論上，這些函數可被記憶化，亦便可將這些函數轉化爲表，而後經過查表的方式得到函數返回值。這是函數（態射）與函數類型（對象）之間等價的本質。

例如，一個接受 Bool 的（純）函數能夠被特化爲一對值：一個對應於 False，另外一個對應於 True 。比方說，全部從 Bool 到 Int 的函數等價於全部 Int 序對所構成的集合，用積來表示就是 Int × Int，或者再有點創造性，可將其表示爲 $Int^2$。

再看一個例子，C++ 的 char 類型，它包含 256 個值。在 C++ 標準庫中常常會使用數據查詢的方式來定義一些函數。例如 isupper 或 isspace 都是用表來實現的，它等價於 256 個布爾值構成的元組。元組是積類型，所以咱們要處理的是 256 個 Bool 值的積：bool × bool × bool × ... × bool。在算術中，重複的積就是冪。若是你將 bool 乘以它自身 256（或 char）次，那麼你獲得的就是 $bool^{char}$。

bool 的 256-元組一共有多少個？答案是 $2^256$ 個。這也就是從 char 到 bool 的不一樣函數的總數，每一個函數對應惟一的 256-元組。同理，從 bool 到 char 的函數數量是 $256^2$。在這些例子中，函數類型的指數表示至關美妙。

咱們可能並不想將一個接受 int 或 double 的函數徹底的記憶化，由於這樣不切實際，可是函數與數據類型之間的等價性老是客觀存在的。還有一些有限類型，例如列表、字符串或樹，若是將接受這些類型的函數進行記憶化，須要無限的存儲空間。然而 Haskell 是一種惰性語言，所以在惰性求值的（無限的）數據結構與函數之間的界限並不那麼明顯。這種函數與數據之間的對偶性揭示了 Haskell 的函數類型與範疇化的指數對象之間的等價性——咱們又朝向數據邁進了一步。

笛卡爾閉範疇

儘管我會繼續使用集合範疇做爲類型與函數的模型，可是要注意很大一部分範疇也可以勝任這項任務。這些範疇被稱爲笛卡爾閉的，集合範疇就屬於此類範疇。

一個笛卡爾閉範疇必須包含：

終端對象
任意對象序對的積
任意對象序對的指數

若是你能將指數想象爲重複的積（多是無限次），那麼你就能夠將笛卡爾閉範疇想象爲支持任意數量的積運算的範疇。特別是，可將終端對象想象爲 0 個對象的積，或者一個對象的 0 次冪。

從計算機科學的角度來看，笛卡爾閉範疇的有趣之處在於它爲簡單的類型 Lambda 演算——全部類型化的編程語言的基礎—提供了模型。

終端對象與積也分別具備對偶物：初始對象與餘積。笛卡爾閉範疇也支持後者，積經過分配率可轉化爲餘積：

a × (b + c) = a × b + a × c
(b + c) × a = b × a + c × a

這樣的範疇被稱爲雙向笛卡爾閉範疇。在下一節中就會看到集合範疇是這種範疇的基本範例以及這種範疇一些有趣的性質。

指數與代數數據類型

從指數的角度來闡釋函數類型，這種方式也能很好的適用於代數數據類型。事實上，中學代數中所涉及的 0，1，加法，乘法以及指數等結構，在任何雙向笛卡爾閉範疇中一樣存在，它們分別對應於初始對象，終端對象，餘積，積以及指數等。咱們如今尚未足夠的工具（諸如伴隨（Adjunction）或 Yoneda 定理）來證實這一點，不過在此我能夠將此直觀的呈現出來。

0 次冪

$$a^0 = 1$$

在範疇論中，0 即初始對象，1 即終端對象，『相等』即恆等態射。指數即內 hom-對象。上面這個特殊的指數表示的是從初始對象到任意對象 $a$ 的態射集合。基於初始對象的定義，這樣的態射只有一個，所以 hom-集 $C(0, a)$ 是一個單例集合。一個單例集合在集合範疇中是終端對象，所以上面這個等式在集合範疇中是成立的，這也意味着它在任何雙向笛卡爾閉範疇中都成立。

在 Haskell 中，咱們用 Void 表示 0，用 unit 類型 () 表示 1，用函數類型表示指數。全部從 Void 到任意類型 a 的函數集合等價於 unit 類型——單例集合。換句話說，有且僅有一個函數 Void -> a，這個函數以前咱們已經見識了，它叫 absurd。不過，這多少有點投機倒把，緣由有二。第一，在 Haskell 不存在沒有值的類型——每種類型都包含着『永不休止的運算』，即底。第二，absurd 的全部實現都是等價的，由於不管用那種方式實現它們，也沒人可以執行它們——沒有值能夠傳遞給 absurd。（若是你傳遞給它一個永不休止的運算，它什麼也不會返回！）

1 的冪

$$1^a = 1$$

在集合範疇中，這個等式重申了終端對象的定義：從任意對象到終端對象存在惟一的態射。從 a 到終端對象的內 home-對象一般與終端對象自己是同構的。

在 Haskell 中，只有一個函數是從任意類型 a 到 unit 類型的，以前見過這個函數—— unit。你能夠認爲它是 const 函數對 () 的偏應用。

1 次冪

$$a^1 = a$$

這個等式重申了從終端對象出發的態射可用於從對象 a 中拮取元素。這種態射的集合與對象 a 自己是同構的。在集合範疇與 Haskell 中，集合 a 與從 a 中拮取元素的函數 () -> a 是同構的。

指數的和

$$a^{b+c} = a^b \times a^c$$

從範疇論的角度來看，這個等式描述的冪爲兩個對象的餘積的指數與兩個指數的積同構。在 Haskell 中，這種代數等式有着很是特別的解釋，它告訴了咱們，兩個類型的和的函數與兩個參數類型爲單一類型的函數的積同構。這偏偏就是咱們在定義做用於和類型的函數時所用到的分支分析，也就是說，函數定義中的 case 語句能夠用兩個或多個處理特定類型的函數來替代。例如，下面這個從和類型 (Eigher Int Double) 出發的函數 f：

f :: Either Int Double -> String

能夠定義爲一個函數對：

f (Left n)  = if n < 0 then "Negative int" else "Positive int"
f (Right x) = if x < 0.0 then "Negative double" else "Positive double"

在此，n 是 Int，而 x 是 Double。

指數的指數

$$(a^b)^c = a^{(b\times c)}$$

這個等式表達的是指數對象形式的柯里化——返回一個函數的函數等價與積類型的函數（帶兩個參數的函數）。

積的指數

$$(a\times b)^c = a^c\times b^c$$

在 Haskell 中，返回一個序對的函數與一對函數等價，後者的每一個函數都返回序對的一個元素。

這些中學數學裏的等式能夠提高至範疇論中而且在函數式編程中得到應用，這一切很是難以想象。

柯里-霍華德同構

我曾提到過邏輯學與代數數據類型之間的一些對應。Void 類型與 unit 類型 () 分別對應於錯誤與正確。積類型與和類型分別對應於邏輯與運算 $\wedge$ 與邏輯或運算 $\vee$。遵循這一模式，咱們所定義的函數類型對應於邏輯推理 $\Rightarrow$，換句話說，類型 a -> b 能夠讀爲『若是 a 那麼 b』。

根據柯里-霍華德同構理論，每種類型可視爲一個命題——爲真或爲假的陳述語句。若是類型是有值的，那麼它就是真命題，不然就是僞命題。在實踐中，若是一個函數類型有值，亦即存在這樣的函數，那麼與它對應的邏輯推理就爲真。去實現一個函數，就是在證實一個定理。寫程序，就等價於證實許多定理。下面看幾個例子。

以函數類型定義中所用的 eval 函數爲例，它的簽名是：

eval :: ((a -> b), a) -> b

它接受一個由函數與其參數構成的序對，產生相應的類型。這個函數是一個態射的 Haskell 實現，該態射爲：

eval :: (a⇒b) × a -> b

這個態射定義了函數類型 a⇒b（或指數類型 $b^a$）。運用柯里-霍華德同構理論，可將這個簽名轉化爲邏輯命題：

$$((a\Rightarrow b)\wedge a) \Rightarrow b$$

可將上面這條陳述讀爲：若是 b 由 a 推出爲真，而且 a 爲真，那麼 b 確定爲真。這就是所謂的確定前件式。要證實這個定理，只須要實現一個函數，即：

eval :: ((a -> b), a) -> b
eval (f, x) = f x

若是你給我一個從 a 到 b 的函數 f 以及 a 類型的一個值 x 所構成的序對，我就能夠將 f 做用於 x，從而產生 b 類型的一個值。經過實現這個函數，我能夠證實 ((a -> b), a) -> b 是有值的。所以，在咱們的邏輯中，這一確定前件式爲真。

結果爲假的邏輯命題是怎樣的？看這個例子，若是 a 或 b 爲真，那麼 a 確定爲真：

$$a \vee b \Rightarrow a$$

這個命題確定是錯的，由於當 a 爲假而 b 爲真時，就能夠構成一個反例。運用柯里-霍華德同構理論，可將這個命題映射爲函數簽名：

Either a b -> a

你能夠試試看，根本沒法實現這樣的函數，由於對於 Right 構造的值而言，沒法產生類型爲 a 的值。（注意，我說的是純函數）。

最後，來理解一下 absurd 函數：

absurd :: Void -> a

將 Void 視爲假，可得：

$$false \Rightarrow a$$

這意味着由謊話可推理出一切（爆炸原理）。對於這個命題（函數），下面用 Haskell 給出的一個證據（實現）：

absurd (Void a) = absurd a

其中 Void 的定義以下：

newtype Void = Void Void

這是咱們慣用的花招，這個定義使得 Void 不可能用於構造一個值，由於你要用它構造一個值，前提是必須先提供這個類型的一個值。這樣就可使得 absurd 永遠沒法被調用。

這些例子頗有趣，可是在現實中可以用柯里-霍華德同構嗎？平時可能用不到，可是像 Agda 或 Coq 這樣的編程語言，它們能夠利用柯里-霍華德同構來證實定理。

計算機不只僅是數學家的輔助工具，它正在掀起基礎數學的一場革命。在這個領域，最新的研究熱點是同倫類型論（Homotopy type theory），它是類型理論的龐枝，也涉及布爾類型、整型、積、餘積以及函數類型等結構，而且彷佛是要驅散人們對它是否有用的質疑，Coq 與 Agda 將這一理論進行了形式化構建。計算機對這個世界的革命途徑不止一種。