標籤：

遞歸類型系統

你好，類型（七）：Recursive type

04-25

上文我們介紹了簡單類型化 $lambda$ 演算系統 $lambda^ o$ ，並給它擴充了單位類型，

本文繼續為它添加新的特性。

我們將提到let和letrec表達式，函數的不動點，

代數數據類型，以及遞歸類型。

最後我們發現，無類型系統實際上是具有，唯一遞歸類型的一種情形。

let綁定

當寫一個複雜表達式的時候，為了避免重複和增加可讀性，

通常我們會給某些子表達式命名，其中一個常用辦法是，使用let表達式。

為此，我們要對簡單類型化 $lambda$ 演算系統 $lambda^ o$ 進行擴展，

添加let表達式的語法項，求值規則以及類型規則。

新的語法：

$t::=...|let~x:T=t~in~t$

新的求值規則：

$let~x:T=v~in~t o [xmapsto v]t$

$frac{t_1 o t_1}{let~x:T_1=t_1~in~t_2 o let~x:T_1=t_1~in~t_2}$

新的類型規則：

$frac{Gammavdash t_1:T_1~~~~Gamma,x:T_1vdash t_2:T_2}{Gammavdash let~x:T_1=t_1~in~t_2:T_2}$

這樣我們就可以寫出let表達式了， $let~x:T_1=t_1~in~t_2$ ，

它表示，求值表達式 $t_1$ ，然後將其綁定到 $t_2$ 中自由出現的 $x$ 上面，

即在當前這種情況下（顧及let polymorphism），let可以表示為， $(lambda x:T_1.t_2)t_1$ 。

不動點

以上let表達式， $let~x:T_1=t_1~in~t_2$ ，

對 $t_1$ 求值的時候有一個限制，那就是 $t_1$ 中不能出現 $x$ ，

否則就像方程一樣， $x$ 出現在了等式的兩邊， $x=t_1(x)$ ，

此時， $t_2$ 中自由出現的 $x$ ，將是這個方程的解。

不過，通常而言， $t_1$ 中是可以出現 $x$ 的，這時候我們就需要使用letrec進行綁定了。

為了看清letrec的真面目，我們用一個求階乘的例子來說明問題，

$letrec~f:nat o nat=lambda y:nat.(if~Eq?~y~0~then~1~else~y*f(y-1))~in~f~5$

其中， $nat$ 表示整數類型。

為了求解 $f=lambda y:nat.(if~Eq?~y~0~then~1~else~y*f(y-1))$ ，

我們定義一個新函數 $F$ ，使得，

$F=lambda f:nat o nat.lambda y:nat.(if~Eq?~y~0~then~1~else~y*f(y-1))$ ，

注意到 $f=F(f)$ ，所以 $f$ 是 $F$ 的不動點。

這裡我們暫且不討論不動點的存在性和唯一性問題，

只是引入一個不動點運算元， $fix_sigma:(sigma osigma) osigma$ ，

它可以用來計算任意函數 $F:sigma osigma$ 的不動點。

為了達到這個目的， $fix_sigma$ 必須滿足以下約束條件， $fix_sigma=lambda f:sigma osigma.f(fix_sigma f)$ 。

引入了 $fix_sigma$ 之後，letrec就可以用let表示出來了，

$letrec~f:sigma=t_1~in~t_2Leftrightarrow let~f:sigma=(fix_sigmalambda f:sigma.t_1)~in~t_2$

代數數據類型

在某些編程語言中，可以自定義遞歸類型，例如在Haskell中，

data List a = Nil | Cons a (List a)lst :: List Int lst = Cons 1 $ Cons 2 $ Nil

以上定義採用了遞歸的方式，定義了一個代數數據類型List，

所謂代數數據類型，是由基本類型經過複合運算，得來的類型。

Haskell中，使用|表示和類型（sum type），

而帶參數值構造器（value constructor）Cons，

用於表示各參數（a，List a）類型的積類型（product type），

無參構造器Nil，用來表示單位乘積類型（empty product）。

（關於函數類型與指數的關係，以後有機會再介紹。）

和letrec中的場景相似的是，List也出現在了等式的兩邊，

於是，我們定義 $mu t.sigma$ ，表示滿足等式 $t=sigma$ 的最小類型，

其中， $t$ 和 $sigma$ 是類型，且 $t$ 通常會在 $sigma$ 中出現。

因此，以上遞歸定義的List類型可以表示為， $muphi.lambdaalpha.(1+alpha imes(phi~alpha))$

其中， $alpha$ 表示類型參數a，

$phi$ 是一個函數，用於表示類型構造器（data constructor）List，

$mu$ 運算元用來計算類型的不動點。

無類型λ演算

在無類型 $lambda$ 演算系統 $lambda_eta$ 中，定義遞歸類型， $mu t.t o t$ ，它滿足類型等式 $t=t o t$ 。

這樣的話，無類型 $lambda$ 演算系統 $lambda_eta$ ，就可以無縫的嵌入到一個類型化的系統中去了，

該系統只存在一個類型，即遞歸類型 $mu t.t o t$ ，

所有的項，都具有這個類型。

因此，對於支持遞歸類型的系統而言，

無類型相當於具有唯一類型（Untyped means uni-typed）。

總結

本文介紹了遞歸類型，引入了兩個運算元 $fix_sigma$ 和 $mu$ ，分別用來求解函數和類型的不動點。

但是，待求的不動點是否存在，是否唯一，我們仍不能確定。

要想證明這件事情並不簡單，需要補充很多額外的數學知識，

例如，良基歸納法和最小不動點定理，

此外，不動點的存在性，和遞歸的終止性也有關係。

好在我們所遇到的大多數場景，都是滿足這些要求的，

因為，我們總是先確信這個解是存在的，然後再去編程，例如，

fact :: Int -> Int fact 1 = 1fact n = n * fact (n - 1)

將fact寫到等式兩邊，能讓我們更方便對fact進行定義。

參考

Algebraic data type

Empty product

Foundations for programmming languages

Practical Foundations for Programming Languages

下一篇：你好，類型（八）：Subtype

推薦閱讀：

※柯里化的前生今世（十）：類型和類型系統

TAG:類型系統 | 遞歸 |