復合型

元組類型

(), (X,), (X, Y), (X, Y, Z), ...

元組具有長度和內部類型的子類型化規則 對于任何元組T，U，以下成立

* T <: () (單位規則)
* forall N in 0..<Len(T) (Len(T) <= Len(U)), U.N == T.N => U <: T (遺忘規則)

例如，(Int, Str, Bool) <: (Int, Str) 但是，這些規則不適用于函數類型的（可見）元組部分。這是因為這部分實際上不是元組

(Int, Int) -> Int !<: (Int,) -> Int

還有單位類型的返回值可以忽略，但是其他tuple類型的返回值不能忽略

配列型

[], [X; 0], [X; 1], [X; 2], ..., [X; _] == [X]

數組和元組存在類似的子類型化規則

* T <: [] (單位規則)
* forall N in 0..<Len(T) (Len(T) <= Len(U)), U[N] == T[N] => U <: T (遺忘規則)

像下面這樣的數組不是有效類型。 這是一個刻意的設計，強調陣列元素是同質化的

[Int, Str]

因此，每個元素的詳細信息都會丟失。 使用篩模來保存它

a = [1, "a"]: {A: [Int or Str; 2] | A[0] == Int}
a[0]: Int

設置類型

{}, {X}, ...

集合類型本身不攜帶長度信息。這是因為元素的重復項在集合中被消除，但重復項通常無法在編譯時確定。首先，長度信息在集合中沒有多大意義

{}是一個空集合，是擁有類型的子類型

詞典類型

{:}, {X: Y}, {X: Y, Z: W}, ...

記錄類型

{=}, {i = Int}, {i = Int; j = Int}, {.i = Int; .j = Int}, ...

具有私有屬性的類型和具有公共屬性的類型之間沒有子類型關系，但它們可以通過.Into相互轉換

r = {i = 1}.Into {.i = Int}
assert r.i == 1

函數類型

() -> ()
Int -> Int
(Int, Str) -> Bool
(x: Int, y: Int) -> Int
(x := Int, y := Int) -> Int
(...objs: Obj) -> Str
(Int, Ref Str!) -> Int
|T: Type|(x: T) -> T
|T: Type|(x: T := NoneType) -> T # |T: Type|(x: T := X, y: T := Y) -> T (X != Y) is invalid