Tan Kian-ting的維基

「一個外行對依值型別的理解-文字檔」修訂間的差異

一個外行對依值型別的理解-文字檔 (檢視原始碼)

於 2024年7月17日 (三) 23:50 的修訂

移除 1,020 位元組 、 2024年7月17日 (星期三)
無編輯摘要
 
行 55： 行 55：
#hd1("一個外行對依值型別的理解")
#hd1("一個外行對依值型別的理解")


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


依值型別 (dependent type) 是型別理論 (type theory) 的重要概念，也是FP的進階概念。因為概念很抽象，而且還要會點型別概念，方好入手。雖此係函數式程式語言的重要概念，但是許多程式人，會仰之彌高，進而生畏，降低學習意願，遑論相關係的定理證明了。
依值型別 (dependent type) 是型別理論 (type theory) 的重要概念，也是FP的進階概念。因為概念很抽象，而且還要會點型別概念，方好入手。雖此係函數式程式語言的重要概念，但是許多程式人，會仰之彌高，進而生畏，降低學習意願，遑論相關係的定理證明了。
行 101： 行 101：
型別理論下「從$A$可得知$B$」以$A tack.r B$表示；「$A$可以推論出$B$」可以用$display(A / 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(
#remark([$display((Gamma, (x : A) tack.r y : B) / (Gamma tack.r lambda x : A . y : A arrow.r B))$~~~~#box[[#set text(
     size: 10pt)
     size: 10pt)
     T-ABS]]], 4)
     T-ABS]]], 4)
行 119： 行 119：
用型別理論的語言表示為：
用型別理論的語言表示為：


#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(
#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))$~~~~#box[[#set text(
     size: 10pt)
     size: 10pt)
     T-APP]]], 6)
     T-APP]]], 6)
行 129： 行 129：
1. 若在上下文$Gamma$中，包含變數$x$，其型別為$A$，則從$Gamma$可得知$x : A$。亦即：
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(
#remark([$display((x : A in Gamma) / (Gamma tack.r x : A))$~~~~#box[[#set text(
     size: 10pt)
     size: 10pt)
     T-VAR]]], 7)
     T-VAR]]], 7)
行 137： 行 137：
#remark([$display((#box[
#remark([$display((#box[
     #set text(font : ("Linux Libertine", "Noto Serif CJK TC"))
     #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(
     c是型別為A的常數]) / (Gamma tack.r c : A))$~~~~#box[[#set text(
     size: 10pt)
     size: 10pt)
     T-CONST]]], 8)
     T-CONST]]], 8)
行 151： 行 151：
[6]T-APP若一樣移除變數，可得到：
[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(
#remark([$display((Gamma tack.r A arrow.r B #h(2em) Gamma tack.r A) / (Gamma tack.r B))$~~~~#box[[#set text(
     size: 10pt)
     size: 10pt)
     T-APP]]], 10)
     T-APP]]], 10)
行 173： 行 173：
我們從[7]開始：
我們從[7]開始：


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


這是型別的推論法，但是我們引入「型別需要屬於kind」的概念，所以前提需要加一條：「自上下文$Gamma$，可得知型別$A$屬於kind $ast.op$，即$A :: ast.op$」，因此補充如下：
這是型別的推論法，但是我們引入「型別需要屬於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)
#remark([$display((x : A in Gamma #h(2em) Gamma tack.r A::ast.op) / (Gamma tack.r x : A))$~~~~[T-VAR]], 12)


然後為了建構依值型別，我們需要引入Pi型別($Pi$-type)的概念。
然後為了建構依值型別，我們需要引入Pi型別($Pi$-type)的概念。
行 201： 行 201：
1. $display(limits(Pi)_(x : "Int") "Str" )$
1. $display(limits(Pi)_(x : "Int") "Str" )$
2. $display(limits(Pi)_(x : "Int") ("Foo" x) )$
2. $display(limits(Pi)_(x : "Int") ("Foo" x) )$
3. $display(limits(Pi)_(x : "Int") (limits(Pi)_(x : "Str") ("Foo" x #h(0.5em) y) ))$
3. $display(limits(Pi)_(y : "Int") (limits(Pi)_(x : "Str") ("Foo" x #h(0.5em) y) ))$


為了建構一個Pi型別，需要擴充[4]：
為了建構一個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)
#remark([$display((Gamma, (x : A) tack.r y : B) / (Gamma tack.r lambda x : A . y : A arrow.r B))$~~~~], 14)


因為引入型別屬於kind的概念，所以前提仍加$A::ast.op$，但是建構出的函數可不只是$Gamma tack.r lambda x : A . y : A arrow.r B$如此簡單了，要考慮$B$是$Pi$型別的情況，所以需要將$Pi$型別的規定，套用到產出函數的型別，修改如下：
因為引入型別屬於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)
#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))$~~~~[T-ABS]], 15)


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




#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)
#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|討論]]）[T-APP]], 17)




取自「https://kianting.info/wiki/w/特殊:手機版差異/2762」