Erg 的類型系統

下面簡單介紹一下 Erg 的類型系統。詳細信息在其他部分進行說明

如何定義

Erg 的獨特功能之一是(普通)變量、函數(子例程)和類型(Kind)定義之間的語法沒有太大區別。所有都是根據普通變量和函數定義的語法定義的

f i: Int = i + 1
f # <函數 f>
f(1) # 2
f.method self = ... # 語法錯誤: 無法為子例程定義方法

T I: Int = {...}
T # <kind 'T'>
T(1) # 類型 T(1)
T.method self = ...
D = Class {private = Int; .public = Int}
D # <類 'D'>
o1 = {private = 1; .public = 2} # o1 是一個不屬于任何類的對象
o2 = D.new {private = 1; .public = 2} # o2 是 D 的一個實例
o2 = D.new {.public = 2} # 初始化錯誤: 類 'D' 需要屬性 'private'(: Int) 但未定義

Classification

Erg 中的所有對象都是強類型的頂層類型是{=}，實現了__repr__、__hash__、clone等(不是必須的方法，這些屬性不能被覆蓋) Erg 的類型系統包含結構子類型 (SST)。該系統類型化的類型稱為結構類型結構類型主要分為三種: Attributive(屬性類型)、Refinement(細化類型)和Algebraic(代數類型)

	Record	Enum	Interval	Union	Intersection	Diff
kind	Attributive	Refinement	Refinement	Algebraic	Algebraic	Algebraic
generator	record	set	range operator	or operator	and operator	not operator

也可以使用名義子類型(NST)，將 SST 類型轉換為 NST 類型稱為類型的名義化。結果類型稱為名義類型在 Erg 中，名義類型是類和Trait。當我們簡單地說類/Trait時，我們通常指的是記錄類/Trait

	Type	Abstraction	Subtyping procedure
NST	NominalType	Trait	Inheritance
SST	StructuralType	Structural Trait	(Implicit)

整個名義類型的類型(NominalType)和整個結構類型的類型(StructuralType)是整個類型(Type)的類型的子類型

Erg 可以將參數(類型參數)傳遞給類型定義。帶有類型參數的 Option、Array 等稱為多項式類型。這些本身不是類型，但它們通過應用參數成為類型。諸如 Int、Str 等沒有參數的類型稱為簡單類型(標量類型)

一個類型可以看成一個集合，并且存在包含關系。例如，"Num"包含"Add"、"Sub"等，"Int"包含"Nat" 所有類的上類是Object == Class {:}，所有類型的下類是Never == Class {}。這在下面描述

類型

像 Array T 這樣的類型可以看作是 Type -> Type 類型的函數，它以 T 類型為參數并返回 Array T 類型(在類型論中也稱為 Kind)。像 Array T 這樣的類型專門稱為多態類型，而 Array 本身稱為一元 Kind

已知參數和返回類型的函數的類型表示為(T, U) -> V。如果要指定同一類型的整個雙參數函數，可以使用 |T| (T, T) -> T，如果要指定整個 N 參數函數，可以使用 Func N。但是，Func N 類型沒有關于參數數量或其類型的信息，因此所有返回值在調用時都是Obj 類型

Proc 類型表示為 () => Int 等等。此外，Proc 類型實例的名稱必須以 ! 結尾

Method 類型是一個函數/過程，其第一個參數是它所屬的對象 self(通過引用)。對于依賴類型，也可以在應用方法后指定自己的類型。這是 T!(!N) 類型和 T!(N ~> N-1)。() => Int 等等

Erg 的數組(Array)就是 Python 所說的列表。[詮釋; 3]是一個數組類，包含三個Int類型的對象

Note: (Type; N) 既是類型又是值，所以可以這樣使用
Types = (Int, Str, Bool)

for! Types, T =>
    print! T
# Int Str Bool
a: Types = (1, "aaa", True)

pop|T, N|(l: [T; N]): ([T; N-1], T) =
    [*l, last] = l
    (l, last)

lpop|T, N|(l: [T; N]): (T, [T; N-1]) =
    [first, *l] = l
    (first, l)

以 ! 結尾的類型可以重寫內部結構。例如，[T; !N] 類是一個動態數組要從"T"類型的對象創建"T!"類型的對象，請使用一元運算符"!"

i: Int! = !1
i.update! i -> i + 1
assert i == 2
arr = [1, 2, 3]
arr.push! 4 # 導入錯誤
mut_arr = [1, 2, 3].into [Int; !3]
mut_arr.push4
assert mut_arr == [1, 2, 3, 4].

類型定義

類型定義如下

Point2D = {.x = Int; .y = Int}

請注意，如果從變量中省略 .，它將成為類型中使用的私有變量。但是，這也是必需的屬性由于類型也是對象，因此類型本身也有屬性。這樣的屬性稱為類型屬性。在類的情況下，它們也稱為類屬性

下面是 Add 類型的定義，需要 +(中間運算符)。R, O 是所謂的類型參數，可以是真正的類型(類)，例如 Int 或 Str。在其他語言中，類型參數被賦予特殊的符號(泛型、模板等)，但在 Erg 中，它們可以像普通參數一樣定義類型參數也可以用于類型對象以外的類型。例如數組類型[Int; 3] 是 Array Int, 3 的語法糖。如果類型實現重疊，用戶必須明確選擇一個

Add R = Trait {
    .AddO = Type
    . `_+_` = Self.(R) -> Self.AddO
}

._+_是Add._+_的縮寫。前綴運算符 .+_ 是 Num 類型的方法

Num = Add and Sub and Mul and Eq
NumImpl = Patch Num
NumImpl.
    `+_`(self): Self = self
    ...

多態類型可以像函數一樣對待。通過將它們指定為 Mul Int、Str 等，它們可以是單態的(在許多情況下，它們是用實際參數推斷出來的，而沒有指定它們)

1 + 1
`_+_` 1, 1
Nat.`_+_` 1, 1
Int.`_+_` 1, 1

前四行返回相同的結果(準確地說，底部的返回 Int)，但通常使用頂部的 Ratio.+(1, 1) 將返回 2.0 而不會出錯這是因為 Int <: Ratio，所以 1 向下轉換為 Ratio 但這不是演員

i = 1
if i: # 類型錯誤: i: Int 不能轉換為 Bool，請改用 Int.is_zero()
    log "a"
    log "b"

這是因為 Bool <: Int (True == 1, False == 0)。轉換為子類型通常需要驗證

類型推理系統

Erg 使用靜態鴨子類型，因此幾乎不需要顯式指定類型

f x, y = x + y

在上面的代碼中，帶有 + 的類型，即 Add 是自動推斷的； Erg 首先推斷出最小的類型。如果f 0, 1，它將推斷f x: {0}，y: {1}，如果n: Nat; f n, 1，它會推斷f x: Nat, y: {1}。最小化之后，增加類型直到找到實現。在 {0}, {1} 的情況下，Nat 與 Nat 是單態的，因為 Nat 是具有 + 實現的最小類型如果是 {0}, {-1}，它與 Int 是單態的，因為它不匹配 Nat。如果子類型和父類型之間沒有關系，則首先嘗試具有最低濃度(實例數)(或者在多態類型的情況下參數更少)的那個 {0} 和 {1} 是枚舉類型，它們是部分類型，例如 Int 和 Nat 例如，可以為枚舉類型指定名稱和請求/實現方法。在有權訪問該類型的命名空間中，滿足請求的對象可以使用實現方法

Binary = Patch {0, 1}
Binary.
    # self 包含一個實例。在此示例中，為 0 或 1
    # 如果你想重寫self，你必須追加！ 必須添加到類型名稱和方法名稱
    is_zero(self) = match self:
        0 -> True
        1 -> False # 你也可以使用 _ -> False
    is_one(self) = not self.is_zero()
    to_bool(self) = match self:
        0 -> False
        1 -> True

此后，代碼"0.to_bool()"是可能的(盡管"0 as Bool == False"是內置定義的) 這是一個實際上可以重寫 self 的類型的示例，如代碼所示

Binary! = Patch {0, 1}!
Binary!
    switch! ref! self = match! self:
        0 => self = 1
        1 => self = 0

b = !1
b.switch!()
print! b # => 0

結構類型(匿名類型)

Binary = {0, 1}

上面代碼中的 Binary 是一個類型，其元素是 0 和 1。它也是 Int 類型的子類型，它同時具有 0 和 1 像 {} 這樣的對象本身就是一種類型，可以在分配或不分配給上述變量的情況下使用這樣的類型稱為結構類型。當我們想強調它作為后者而不是類(命名類型)的用途時，它也被稱為未命名類型。{0, 1}這樣的結構類型稱為枚舉類型，還有區間類型、記錄類型等

類型標識

無法指定以下內容。例如，您不能指定 Int 和 Int 和 Int 和 Int 和 Int 和 Int 例如，Int和Str都是Add，但是Int和Str不能相加

add l: Add, r: Add =
    l + r # 類型錯誤: `_+_` 沒有實現: |T, U <: Add| (T, U) -> <失敗>

此外，下面的類型 A 和 B 不被認為是同一類型。但是，類型"O"被認為是匹配的

... |R1, R2, O, A <: Add(R1, O); B <: Add(R2, O)|

The Erg Book