変性

badge

Ergは多相型のサブタイピングを行えるが、一部注意しなくてはならない点がある。

まずは通常の多相型の包含関係を考える。一般に、コンテナKと代入する型A, Bがあり、A < Bのとき、K A < K Bとなる。 例えば、Option Int < Option Objectとなる。よって、Option Objectで定義されているメソッドは、Option Intでも使用可能である。

典型的な多相型であるArray!(T)型について考える。 今回は要素の数を問題にしないのでArray!(T, N)ではないことに注意してほしい。 さて、Array!(T)型には.push!と.pop!というメソッドが存在し、それぞれ、要素の追加・取り出しを意味する。型はこうである。

Array.push!: Self(T).(T) => NoneType Array.pop!: Self(T).() => T

直感的に理解できることとして、

  • s: StrのときArray!(Object).push!(s)はOK(StrをObjectにアップキャストすれば良い)
  • o: ObjectのときArray!(Str).push!(o)はNG
  • Array!(Object).pop!().into(Str)はNG
  • Array!(Str).pop!().into(Object)はOK

である。これは、型システム的には

  • (Self(Object).(Object) => NoneType) < (Self(Str).(Str) => NoneType)
  • (Self(Str).() => Str) < (Self(Object).() => Object)

を意味する。

前者は奇妙に思えるかもしれない。Str < Objectなのに、それを引数に取る関数は包含関係が逆転している。 型理論では、このような関係(.push!の型関係)を反変(contravariant)といい、その逆、.pop!の型関係は共変(covariant)という。 つまり、関数型は引数の型に関して反変であり、戻り値の型に関して共変である、といえる。 複雑に聞こえるが、先程見た通り実例に当てはめて考えれば合理的なルールである。 それでもいまいちピンと来ない場合は次のように考えるとよい。

Ergの設計方針に、「入力の型は大きく、出力の型は小さく」というのがある。これはまさに関数の変性から言える。 上のルールを見れば、入力型は大きい方が全体として小さい型になる。 汎用の関数は明らかに専用の関数より希少だからである。 そして出力型は小さい方が全体として小さくなる。

結果として上の方針は「関数の型を最小化せよ」と言っているのに等しい。

非変性

Ergにはもう一つ変性がある。それは非変性(non-variance)である。 これは組み込み型ではSharedCell! T!などが持っている変性である。これは、T! != U!なる2つの型T!, U!に関して、例え包含関係があったとしてもSharedCell! T!とSharedCell! U!間でキャストができないことを意味する。 これは、SharedCell! T!が共有参照であることに由来する。詳しくは共有参照を参照。

変性指定された全称型

全称型の型変数は、その上限・下限を指定できます。

|A <: T| K(A)
|B :> T| K(B)

型変数リスト内では型変数の 変性指定 を行っています。上の変性指定において、型変数Aは型Tに対する任意のサブクラスであり、型変数Bは型Tに対する任意のスーパークラスであると宣言されています。 このとき、TをAに対する上限型、Bに対する下限型ともいいます。

変性指定は重ねがけすることもできます。

# U<A<T
|A<: T, A :> U| ...

以下に変性指定を使ったコードの例を示します。

show|S <: Show| s: S = log s

Nil T = Class(Impl=Phantom T)
Cons T = Class(Nil T or List T)
List T = Class {head = T; rest = Cons T}
List(T).
    push|U <: T|(self, x: U): List T = Self.new {head = x; rest = self}
    upcast(self, U :> T): List U = self

変性指定

List Tの例については注意が必要なので、もう少し詳しく説明します。 上のコードを理解するためには多相型の変性について知っておく必要があります。変性についてはこの項で詳しく解説していますが、さしあたって必要となる事実は以下の3つです:

  • 通常の多相型、List TなどはTに対して共変(U > TのときList U > List T)
  • 関数T -> Uは引数型Tに対して反変(S > Tのとき(S -> U) < (T -> U))
  • 関数T -> Uは戻り値型Uに対して共変(U > Sのとき(T -> U) > (T -> S))

例えば、List IntはList Objectにアップキャスト可能、Obj -> ObjはInt -> Objにアップキャスト可能であるということです。

ここで、メソッドの変性指定を省略した場合どうなるか考えます。

...
List T = Class {head = T; rest = Cons T}
List(T).
    # List T can be pushed U if T > U
    push|U|(self, x: U): List T = Self.new {head = x; rest = self}
    # List T can be List U if T < U
    upcast(self, U): List U = self

この場合でも、ErgコンパイラはUの上限・下限型をよしなに推論してくれます。 ただし、Ergコンパイラはメソッドの意味を理解しないことに注意してください。コンパイラはただ変数・型変数の使われ方に従って機械的に型関係を推論・導出します。

コメントに書いてある通り、List Tのheadに入れられる型UはTのサブクラス(T: IntならばNatなど)です。すなわち、U <: Tと推論されます。この制約は.push{U}の引数型を変更するアップキャスト(List(T), U) -> List(T) to (List(T), T) -> List(T)(e.g. List(Int).push{Object})を禁止します。ただし、U <: Tという制約は関数の型の包含関係を改変しているわけではないことに注意してください。(List(Int), Object) -> List(Int) to (List(Int), Int) -> List(Int)である事実は変わらず、ただ.pushメソッドにおいてはそのようなアップキャストを実行できないという意味になります。 同様に、List TからList UへのキャストはU :> Tという制約のもとで可能なので、そのように変性指定が推論されます。この制約は、.upcast(U)の戻り値型を変更するアップキャストList(T) -> List(T) to List(T) -> List(T)(e.g. List(Object).upcast(Int))を禁止します。

では、このアップキャストを許可するようにした場合はどうなるか考えます。 変性指定を反転させてみましょう。

...
List T = Class {head = T; rest = Cons T}
List(T).
    push|U :> T|(self, x: U): List T = Self.new {head = x; rest = self}
    upcast(self, U :> T): List U = self
# TypeWarning: `U` in the `.push` cannot take anything other than `U == T`. Replace `U` with `T`. Or you may have the wrong variance specification.
# TypeWarning: `U` in the `.upcast` cannot take anything other than `U == T`. Replace `U` with `T`. Or you may have the wrong variance specification.

U <: Tという制約とU :> Tという変性指定の両方を充足するのはU == Tのときだけです。なので、この指定にはほとんど意味がありません。 実際は「U == Tであるようなアップキャスト」=「Uの箇所については変えないアップキャスト」のみが許可されています。

付録: ユーザー定義型の変性

ユーザー定義型の変性は、デフォルトでは非変である。しかし、Inputs/Outputsというマーカートレイトで変性を指定することもできる。 Inputs(T)と指定すると、その型はTに関して反変となる。 Outputs(T)と指定すると、その型はTに関して共変となる。

K T = Class(...)
assert not K(Str) <= K(Object)
assert not K(Str) >= K(Object)

InputStream T = Class ..., Impl := Inputs(T)
# Objectを受け入れるストリームは、Strを受け入れるともみなせる
assert InputStream(Str) > InputStream(Object)

OutputStream T = Class ..., Impl := Outputs(T)
# Strを出力するストリームは、Objectを出力するともみなせる
assert OutputStream(Str) < OutputStream(Object)