一個外行對依值型別的理解-文字檔

導航：首頁 > 程式語言、邏輯學> 一個外行對依值型別的理解-文字檔

可使用[Typst https://typst.app]生成。

deptype.typ

#set par(
  justify: true,
  leading: 1em,
)

#let CJKNonCJKSpacing = 0.2em

#let RegExCJK = "[\p{Han}\p{Hiragana}\p{Katakana}\p{Hangul}\p{Bopomofo}]"
#let RegExNonCJK = "[^\p{Han}\p{Hiragana}\p{Katakana}\p{Hangul}\p{Bopomofo}]"

#let RegExNonCJK = "[^\p{Han}\p{Hiragana}\p{Katakana}\p{Hangul}\p{Bopomofo}]"


#show regex(RegExCJK+RegExNonCJK) : it => {
    text[#it.text.first()#box(width: CJKNonCJKSpacing,"")#it.text.last()]
}

#show regex(RegExNonCJK+RegExCJK) : it => {
    text[#it.text.first()#box(width: CJKNonCJKSpacing,"")#it.text.last()]
}

#set page(
  numbering: "1 / 1",
)

#set text(
    size: 12pt,
    font: ("Linux Libertine", "Noto Serif CJK TC"),// "Linux Libertine Mono O"
    )

#let hd1(txt) = box[
    #set text(
    font: ("FreeSans", "Noto Sans CJK TC"),// "Linux Libertine Mono O"
    )
    = #txt ]

#let hd2(txt) = box[
    #set text(
    font: ("FreeSans", "Noto Sans CJK TC"),// "Linux Libertine Mono O"
    )
    == #txt ]
#let remark(txt, number) = box(width:100%,
fill: rgb("#EBFAEF"), [
#v(1em)
#align(center,[#txt~~#sub([[#number]])])
#v(1em)])

#hd1("一個外行對依值型別的理解")

（始撰於2023-07-14，完稿2023-07-16，使用#link("https://creativecommons.org/licenses/by-nc-sa/4.0/")[CC BY-NC-ND授權]）

依值型別 (dependent type) 是型別理論 (type theory) 的重要概念，也是FP的進階概念。因為概念很抽象，而且還要會點型別概念，方好入手。雖此係函數式程式語言的重要概念，但是許多程式人，會仰之彌高，進而生畏，降低學習意願，遑論相關係的定理證明了。

身為一個外行，之前筆者亦如是。對型別理論感到興趣之際，面對依值型別還是一頭霧水，不知何以理解。然最近稍理解些，所以做了這份筆記。

#hd2("型別是一群變數的群體，但型別自身有無群體？")

大家應該都很清楚，1, 12, 1000, -1都屬於 $"Int"$ 這個「整數型別」；3.1416、7.2、-11.22都是 $"Float"$「浮點數型別」。就連一個函數輸入 $"Int"$ 返回 $"Str"$ 字串 (string) 的函數，也可以視為「輸入 $"Int"$ 返回 $"Str"$」的函數型別，即 $"Int" arrow.r "Str"$ 型別。

型別內包許多東西（常數、變數等等），雖然型別和高中教的集合不一樣，但是也是「許多東西的合稱」。

這樣可以推論，整數、小數、浮點數等型別，甚至函數型別，非常多元。但是是否有「型別的型別」？就像一群村里組成鄉鎮一樣，一群鄉鎮是否可以組成縣一樣。

型別理論其實是有描述的，稱為 "kind"（這個詞我不知道如何用華語表示），用星號 $ast.op$ 表示。若是變數 $x$ 屬於型別 $T$ 時可以用 $x:T$ 表示，同理，型別 $T$ 屬於 kind $ast.op$ 時，可以使用 $T::ast.op$（兩個冒號$::$用來和「$"數":"型別"$」區分。另外kind的群體叫做 "sort"，但太複雜，按下不表，讀者現在只要知道「type < kind < sort」即可。

該階層概念，係依值型別概念的先備知識。另一個概念是簡單型別lambda運算的型別指派 (typing)。

#hd2("若有apple，且有pen，則……")

以下簡單介紹一下簡單型別lambda演算的概念。

假設我們有一個型別為$"Int"$的變數$x$，記為$x:"Int"$，和旁邊的上下文（context，可理解為一群程式碼的集合，記為$Gamma$）組合起來的新程式碼，即「$Gamma, x:"Int"$」之中，可推論另一數$y$屬於$"Str"$，即$y:"Str"$。那麼，下列引數 (argument) 為$x$，回傳$y$的匿名lambda函數（不會的可以看一下JavaScript或是Python對lambda的講解）的型別是什麼呢？

```
function(Int x){
    return y; // y is a "Str"
}
```

依上文以箭頭表示函數型別的方法，是$"Int" arrow.r "Str"$。

如果將整段話綜整描述的話，即：若從「上下文$Gamma$和$x:"Int"$」之組合中，可獲知$y:"Str"$，則可推論出：

#remark([從上下文$Gamma$可知，`function (Int x){return y;}`的型別是$"Int" arrow.r "Str"$。], 1)

用附帶型別的lambda運算中，可以表示為$(lambda (x : "Int") . y) : ("Int" arrow.r "Str")$，其中括號可以省略，變成：

#remark([$lambda x : "Int" . y : "Int" arrow.r "Str"$],2)

將型別以代數A, B標記，context 之間，以逗號,結合，並使用$A arrow.double.r B$（若$A$則$B$）的邏輯符號，[1]就變成：

#remark([若從 $Gamma, (x : A)$可推知$y : B arrow.double.r $從$Gamma$可推知$lambda x : "Int" . y : A arrow.r B$],3)

型別理論下「從$A$可得知$B$」以$A tack.r B$表示；「$A$可以推論出$B$」可以用$display(A / B)$表示，所以[3]寫成：

#remark([$display((Gamma, (x : A) tack.r y : B) / (Gamma tack.r lambda x : A . y : A arrow.r B))$[[使用者:Tankianting|Tankianting]]（[[使用者討論:Tankianting|討論]]） 2023年7月16日 (日) 23:28 (CST)#box[[#set text(
    size: 10pt)
    T-ABS]]], 4)

以上是如何建構lambda函數型別的方法，但是我們假設有一個函數$f : A arrow.r B$，輸入一個變數$a : A$，那$f(a)$的型別是什麼呢？

回到現實的程式碼。假設 `f = function (A x){return y;} // y 型別是 B`，那`f(a)`直觀來看，回傳`y`，型別就是`B`。

因此，用型別理論的角度，我們可以這樣說：

#remark([在上下文（一串程式碼）$Gamma$中，若可知$f : A arrow.r B $，

且據$Gamma$亦可知$a : A$，

則自$Gamma$可知$f(a): B$], 5)

用型別理論的語言表示為：

#remark([$display((Gamma tack.r f : A arrow.r B #h(2em) Gamma tack.r a : A) / (Gamma tack.r f#h(0.5em)a : B))$[[使用者:Tankianting|Tankianting]]（[[使用者討論:Tankianting|討論]]） 2023年7月16日 (日) 23:28 (CST)#box[[#set text(
    size: 10pt)
    T-APP]]], 6)

其中 $display((A and B …) / C)$的$and$不標，以空格區分；$f(a)$寫成$f#h(0.5em)a$。

除了[4] T-ABS和[6] T-APP兩個rule外，簡單型別lambda運算還有其他的rule：

1. 若在上下文$Gamma$中，包含變數$x$，其型別為$A$，則從$Gamma$可得知$x : A$。亦即：

#remark([$display((x : A in Gamma) / (Gamma tack.r x : A))$[[使用者:Tankianting|Tankianting]]（[[使用者討論:Tankianting|討論]]） 2023年7月16日 (日) 23:28 (CST)#box[[#set text(
    size: 10pt)
    T-VAR]]], 7)

2. 若$c$是型別為$A$的常數，則在上下文$Gamma$中，可得知$c : A$。亦即：

#remark([$display((#box[
    #set text(font : ("Linux Libertine", "Noto Serif CJK TC"))
    c是型別為A的常數]) / (Gamma tack.r c : A))$[[使用者:Tankianting|Tankianting]]（[[使用者討論:Tankianting|討論]]） 2023年7月16日 (日) 23:28 (CST)#box[[#set text(
    size: 10pt)
    T-CONST]]], 8)

=== 和邏輯學的關係

把[4]移除程式變（函）數的話，會得到：

#remark([$display((Gamma, A tack.r  B) / (Gamma tack.r A arrow.r B))$], 9)

若是會命題邏輯(sentence logic)的話，可發現這個表達式和「若有串邏輯表達語句（邏輯論述）$Gamma$和命題$A$，可得知命題B的話，則可推論該論述可知若$A$則$B$」的表達方式一樣。

[6]T-APP若一樣移除變數，可得到：

#remark([$display((Gamma tack.r A arrow.r B #h(2em) Gamma tack.r A) / (Gamma tack.r B))$[[使用者:Tankianting|Tankianting]]（[[使用者討論:Tankianting|討論]]） 2023年7月16日 (日) 23:28 (CST)#box[[#set text(
    size: 10pt)
    T-APP]]], 10)

和命題邏輯的「若一串邏輯表達語句$Gamma$可知若$A$則$B$，且亦可知$A$，則$Gamma$亦可知$B$」一樣。

這種型別推論和邏輯推論如出一轍的情況，叫做Curry-Howard同構 (Curry-Howard Correspondence)。而簡單型別lambda運算的推論方法，對應到命題邏輯。

== 擴充到依值型別

現在我們可以推衍到簡單的依值型別形式$lambda$LF。

但什麼叫「依值型別」？可以想成「型別裡面內嵌著數」，若一個屬於某型別$S$的數$x$被包在型別$T$裡面裝變數的「容器」，則T這個型別，實際鑲嵌$x$，不論其型別$S$是浮點數、整數、或是樹狀結構、函數，只要是有type的都行。

為了方便理解，打比方：

我們假設有個型別，屬於kind $ast.op$，叫做$"DepType"(x)$，且有一個函數$f(x)$，輸入一個$"Int"$，輸出的型別是$"DepType"(x)$。則$f(x)$的型別不是固定的一個詞句，更非一成不變，而是取決於$x$的「表達式」，隨$x$改變。比如$f(42)$，型別就叫做$"DepType"(42)$；$f(101)$，型別就叫做$"DepType"(101)$。

但要如何在程式中，生出（建構出）依值型別的函（變）數？推論過程比較複雜些。

我們從[7]開始：

#remark([$display((x : A in Gamma) / (Gamma tack.r x : A))$[[使用者:Tankianting|Tankianting]]（[[使用者討論:Tankianting|討論]]） 2023年7月16日 (日) 23:28 (CST)], 11)

這是型別的推論法，但是我們引入「型別需要屬於kind」的概念，所以前提需要加一條：「自上下文$Gamma$，可得知型別$A$屬於kind $ast.op$，即$A :: ast.op$」，因此補充如下：


#remark([$display((x : A in Gamma #h(2em) Gamma tack.r A::ast.op) / (Gamma tack.r x : A))$[[使用者:Tankianting|Tankianting]]（[[使用者討論:Tankianting|討論]]） 2023年7月16日 (日) 23:28 (CST)[T-VAR]], 12)

然後為了建構依值型別，我們需要引入Pi型別($Pi$-type)的概念。

其為函數型別，輸入$x : S$，輸出值型別為$T$——但$T$除了是常型別如：$"Str", "Int"…$，或型別變數$A, B, C,…$外，也可以是包含可以被值套用(applicable)的依值型別，如$P(x), Q(x)$（型別內的括號()書寫時可忽略），甚至是另一個Pi型別。這種狀況可以用下列程式碼的函數類比：

```
// S是Type
Type PiType1(S x){
    return T; /* T是 Type，可以是P(x)、Q(x)、Array(x)
    PiType2(A y){...}等*/
}

```

Pi型別表達如下：

#remark([$display(limits(Pi)_(x : S) T )$], 13)

下列是合規的Pi型別：

1. $display(limits(Pi)_(x : "Int") "Str" )$
2. $display(limits(Pi)_(x : "Int") ("Foo" x) )$
3. $display(limits(Pi)_(x : "Int") (limits(Pi)_(x : "Str") ("Foo" x #h(0.5em) y) ))$

為了建構一個Pi型別，需要擴充[4]：

#remark([$display((Gamma, (x : A) tack.r y : B) / (Gamma tack.r lambda x : A . y : A arrow.r B))$[[使用者:Tankianting|Tankianting]]（[[使用者討論:Tankianting|討論]]） 2023年7月16日 (日) 23:28 (CST)], 14)

因為引入型別屬於kind的概念，所以前提仍加$A::ast.op$，但是建構出的函數可不只是$Gamma tack.r lambda x : A . y : A arrow.r B$如此簡單了，要考慮$B$是$Pi$型別的情況，所以需要將$Pi$型別的規定，套用到產出函數的型別，修改如下：

#remark([$display((Gamma, (x : A) tack.r y : B  #h(2em)  Gamma tack.r A::ast.op) / (Gamma tack.r lambda x : A . y : limits(Pi)_(x:A)B))$[[使用者:Tankianting|Tankianting]]（[[使用者討論:Tankianting|討論]]） 2023年7月16日 (日) 23:28 (CST)[T-ABS]], 15)

要推論函數$f$套用一個變數$a$的返回值$f#h(0.5em)a$，型別是什麼？需要擴充[6]：

#remark([$display((Gamma tack.r f : A arrow.r B #h(2em) Gamma tack.r a : A) / (Gamma tack.r f#h(0.5em)a : B))$], 16)

先把函數$f$的型別改成Pi型別：

#remark([$display((Gamma tack.r f : Pi_(x:A)B #h(2em) Gamma tack.r a : A) / (Gamma tack.r f#h(0.5em)a : B))$], 17)

因為$f(x)$這種Pi型別函數，回傳值的型別受到$x$的值改變，也就是套用變數$a$之後，$B$的型別裡面所有的$x$改成$a$（沒有的話不管它），才能得到正確的輸出型別。我們把「$B$裡面的$x$取代成$a$」寫成$[a arrow.bar.r x]B$，因此推論的rule最後寫如下：



#remark([$display((Gamma tack.r f : Pi_(x:A)B #h(2em) Gamma tack.r a : A) / (Gamma tack.r f#h(0.5em)a: [a arrow.bar.r x]B))$[[使用者:Tankianting|Tankianting]]（[[使用者討論:Tankianting|討論]]）[T-APP]], 17)


因此，若$f$型別是$Pi_(x :"Int")"Str"$時，套用10這個整數後，$f(10)$的型別是$[10 arrow.bar.r x]"Str"$，還是$"Str"$。這點和簡單型別lambda運算不變。但若是f的型別是$Pi_(x : "Int")"foo" x$時，則$f(42)$型別是$[42 arrow.bar.r x]"foo" x$，即$"foo" 42$，至$f(8)$的型別是$"foo" 8$。

=== 和邏輯的關係？

如之前說的Curry-Howard同構，依值型別的typing可類比謂詞邏輯(predicate logic)推論原則。說明如下：

假設$P$代表人(Person)這個類別，且我們從一串邏輯論述（上下文）$Gamma$中可以得知「$P$屬於類別的類別」，且$Gamma$和$P$組合在一起，可以得知$C#h(0.5em)x$，括號略，$C$指Creature（生物）。可以推演出「在該論述下，對於所有$x$屬於人的時候，$x$是生物」。這句話用形式邏輯寫如下：

#remark([$display((Gamma, P tack.r C#h(0.5em)x  #h(2em)  Gamma tack.r P::ast.op) / (Gamma tack.r forall x in P.C x))$], 18)

和[15]移除變數並改寫型別符號的長相很像：

#remark([$display((Gamma, P tack.r  C#h(0.5em)x  #h(2em)  Gamma tack.r P::ast.op) / (Gamma tack.r  limits(Pi)_(x:P) C#h(0.5em)x))$], 19)

而1.「自邏輯論述$Gamma$可知，$forall x in P. C#h(0.5em)x$」且2.「自$Gamma$可知$m in P$」，則3.「自$Gamma$可知$C#h(0.5em)m$」這種三段論邏輯，可表達如下：

#remark([$display((Gamma, tack.r  forall x in P. C#h(0.5em)x  #h(2em)  Gamma tack.r m in P) / (Gamma tack.r C#h(0.5em)m))$], 20)

[20]和[17]更改型別名稱，移除一些項目的形式很像：

#remark([$display((Gamma tack.r Pi_(x:A) C#h(0.5em)x #h(2em) Gamma tack.r m : A) / (Gamma tack.r [m arrow.bar.r x]C#h(0.5em)x))$], 21)

其中$[m arrow.bar.r x]C#h(0.5em)x = C#h(0.5em)m$~~。

所以有說依值型別對應謂詞邏輯，Pi型別對應全稱量詞$forall$。

== 接下來可以學什麼呢？

依值型別還有其他的變體，且上面僅介紹Pi型別，沒介紹Sigma型別（$Sigma$-type，對應存在量詞$exists$）。另依值型別和電腦輔助數學（邏輯）證明息息相關，若是想要踏入這些大坑，還有其他書籍可以參考
。使用依值型別的程式語言，包含Agda、Coq、Lean等，想瞭解的話可以另外學習。

但我還沒入坑，所以就留給各位看官探究了。