複合型

タプル型

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

上のタプル型は構文糖であり、(X, Y) == Tuple [X, Y]である。

タプルには、中の型だけでなく長さについての部分型規則が存在する。任意のタプル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

また、ユニット型の戻り値は無視できるが、その他のタプル型の戻り値は無視できない。

配列型

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

上の配列型は構文糖であり、[X; N] == Array X, Nである。

配列に関してもタプルと同様の部分型規則が存在する。

* 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

セット型

{}, {T; _}, ...

上のセット型は構文糖であり、{T; N} == Set T, Nである。

セット型は長さの情報を持つが、あまり使われない。セットでは要素の重複は排除されるが、重複の判定は一般にコンパイル時には出来ないためである(そのため、長さは確定できず、多くの場合でパラメータは消去される)。そもそもセットにおいて長さの情報はあまり意味をなさない。

{}は空集合であり、すべての型のサブタイプである。{T}とすると定数Tのみを含む型となるので注意。

辞書型

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

上の形の辞書型はすべてDict K, Vのサブタイプである。Dict K, Vは均質化された辞書型を意味する。 {K: V} <: Dict K, Vであり、{X: Y, Z: W} <: Dict X or Z, Y or Wである。

レコード型

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

上の形のレコード型はすべてRecordのサブタイプである。属性が非公開のレコード型は公開のレコード型のスーパータイプである。属性は非公開化できるが、逆はできないということである。

{.i = Int} <: {i = Int}

関数型

() -> ()
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

バインドされたメソッド型

Int.() -> Int
Int.(other: Int) -> Int
# e.g. 1.__add__: Int.(Int) -> Int

C.(T) -> Uの型はT -> Uのサブタイプである。実際両者はほとんど変わらないが、C.(T) -> UはCをレシーバ型とするメソッドの型であり、__self__という属性からレシーバにアクセスできる。

The Erg Book