カインド

Ergでは全てが型付けられている。型自体も例外ではない。「型の型」を表すのが カインド(種) である。例えば1がIntに属しているように、IntはTypeに属している。Typeは最もシンプルなカインドである 原子カインド(Atomic kind) である。型理論的の記法では、Typeは*に対応する。

カインドという概念で実用上重要なのは1項以上のカインド(多項カインド)である。1項のカインドは、例えばOptionなどがそれに属する。1項カインドはType -> Typeと表される¹。ArrayやOptionなどの コンテナ は特に型を引数に取る多項カインドのことなのである。 Type -> Typeという表記が示す通り、実はOptionはTという型を受け取ってOption Tという型を返す関数である。ただし、この関数は通常の意味での関数ではないため、1項カインド(unary kind)と普通は呼称される。

なお、無名関数演算子である->自体も型を受け取って型を返す場合カインドとみることができる。

また、原子カインドでないカインドは型ではないことに注意してほしい。-1は数値だが-は数値ではないのと同じように、Option Intは型だがOptionは型ではない。Optionなどは型構築子と呼ばれることもある。

assert not Option in Type
assert Option in Type -> Type

なので、以下のようなコードはエラーになる。 Ergではメソッドを定義できるのは原子カインドのみで、メソッドの第一引数以外の場所でselfという名前を使えない。

# Kは単項の一種です
K: Type -> Type
K T = Class ...
K.
    foo x = ... # OK、これはいわゆるスタティックメソッドのようなもの
    bar self, x = ... # TypeError: cannot define a method to a non-type object
K(T).
    baz self, x = ... # OK

2項以上のカインドの例としては{T: U}(: (Type, Type) -> Type), (T, U, V)(: (Type, Type, Type) -> Type), ...などが挙げられる。

0項のカインド() -> Typeも存在する。これは型理論的には原子カインドと同一視されることもあるが、Ergでは区別される。例としてはClassなどがある。

Nil = Class()

カインドの包含関係

多項カインド間にも部分型関係、もとい部分カインド関係があります。

K T = ...
L = Inherit K
L <: K

すなわち、任意のTに対しL T <: K TならばL <: Kであり、その逆も成り立ちます。

∀T. L T <: K T <=> L <: K

高階カインド

高階カインド(higher-order kind)というものもある。これは高階関数と同じコンセプトのカインドで、カインド自体を受け取るカインドである。(Type -> Type) -> Typeなどが高階カインドである。高階カインドに属するオブジェクトを定義してみよう。

IntContainerOf K: Type -> Type = K Int
assert IntContainerOf Option == Option Int
assert IntContainerOf Result == Result Int
assert IntContainerOf in (Type -> Type) -> Type

多項カインドの束縛変数はK, L, ...などと表されるのが通例である(KはKindのK)。

セットカインド

型理論において、レコードという概念がある。これはErgのレコードとほぼ同じものである²。

# これは`レコード`であり、型理論でいうところの`レコード`に相当するものである
{x = 1; y = 2}

レコードの値が全て型であるとき、それはレコード型といって型の一種であった。

assert {x = 1; y = 2} in {x = Int; y = Int}

レコード型はレコードを型付けする。察しの良い方は、レコード型を型付けする「レコードカインド」があるはずだと考えたかもしれない。実際に、それは存在する。

log Typeof {x = Int; y = Int} # {{x = Int; y = Int}}

{{x = Int; y = Int}}のような型がレコードカインドである。これは特別な記法ではない。単に、{x = Int; y = Int}のみを要素に持つ列挙型である。

Point = {x = Int; y = Int}
Pointy = {Point}

レコードカインドの重要な特性は、T: |T|であり、U <: Tであるとき、U: |T|であるという点にある。これは列挙型が実際には篩型の糖衣構文であることからもわかる。

# 通常のオブジェクトでは{c} == {X: T | X == c}だが、
# 型の場合等号が定義されない場合があるので|T| == {X | X <: T}となる
{Point} == {P | P <: Point}

型制約中のU <: Tは、実はU: |T|の糖衣構文である。このような型のセットであるカインドは一般にセットカインドと呼ばれる。セットカインドはIteratorパターンでも現れる。

Iterable T = Trait {
    .Iterator = {Iterator}
    .iter = (self: Self) -> Self.Iterator T
}

多項カインドの型推論

Container K: Type -> Type, T: Type = Patch K(T, T)
Container(K).
    f self = ...
Option T: Type = Patch T or NoneType
Option(T).
    f self = ...
Fn T: Type = Patch T -> T
Fn(T).
    f self = ...
Fn2 T, U: Type = Patch T -> U
Fn2(T, U).
    f self = ...

(Int -> Int).f() # どちらが選択されるだろうか?

上の例で、メソッドfはどのパッチが選ばれるのだろうか。素朴に考えてFn Tが選ばれるように思われるが、Fn2 T, Uもあり得るし、Option TはTそのままを含むので任意の型が該当し、Container K, Tも `->`(Int, Int)すなわちContainer(`->`, Int)としてInt -> Intにマッチする。なので、上の4つのパッチすべてが選択肢としてありえる。

この場合、以下の優先基準に従ってパッチが選択される。

任意のK(T)(e.g. T or NoneType)はTypeよりもType -> Typeに優先的にマッチする。
任意のK(T, U)(e.g. T -> U)はTypeよりも(Type, Type) -> Typeに優先的にマッチする。
3項以上のカインドについても同様の基準が適用される。
置換する型変数が少なく済むものが選択される。例えばInt -> IntはK(T, T)(置換する型変数: K, T)やT -> U(置換する型変数: T, U)よりもT -> T(置換する型変数: T)が優先的にマッチする。
置換数も同じ場合は選択不能としてエラー。

¹ 型理論の記法では*=>* ↩

² 可視性などの微妙な違いはある。↩

The Erg Book

カインド

カインドの包含関係

高階カインド

セットカインド

多項カインドの型推論