読者です 読者をやめる 読者になる 読者になる

anti scroll

ブラウザと小説の新しい関係を模索する

reactive programming / getterは共変、setterは反変

プログラミング

reactive programmingについての動画(語り手がハイテンション)を見つけました。

http://channel9.msdn.com/Events/Lang-NEXT/Lang-NEXT-2014/Keynote-Duality

まだ前半しかみてないのですが、途中getterとsetterを「共変(covarience)」と「反変(contravarience)」という概念を使って説明している箇所があって、あんまりピンと来なかったので、少し落ち着いて考えてみました。

というわけで以下は備忘録です。

サブタイプ

動画の人は「コーラはソーダのサブタイプ」って説明してました。

ソーダ型はコーラ型を含むので、ソーダ型で記述できた式は、ソーダの部分をコーラに置き換えても動作するはずです。

で、こういう状況を

ソーダ型 >= コーラ型

なんて書くことにします。

共変と反変

例えば型をもとに新しい型を作る型構築ルールRがあったとします。

で、これをソーダ型に適用したR(ソーダ型)と、コーラ型に適用したR(コーラ型)が、

R(ソーダ型)>= R(コーラ型)

という風に、元の関係を維持しているとき(つまりR(ソーダ型)の部分を、R(コーラ型)で置き換えることができるような状況になっているとき)、Rを「共変」と言います。

逆にR(コーラ型)の部分が、R(ソーダ型)で置き換え可能な状況になっている場合は「反変」と言います。

で、動画(の前半)で言ってることは、元のサブタイピングの関係に対して、getterの型構築子は共変だけど、setterの型構築子は反変になるから気をつけてね、ってことだと思います。

getterは共変

例えば、NumのサブタイプをIntとします。

で、Numは他にもFloatとかもサブタイプに含むものとします。

Num >= Int
Num >= Float

続いて、getterを作る型構築ルールを次のように定義します。

getter(A) = () -> A

つまり、getter(A)は型Aから「何かしたらAが返る」という関数型を生み出すものとします。これをNum/Intに当てはめると

  • getter(Num):() -> Num
  • getter(Int): () -> Int

となります。

さて、プログラムの中に、getter(Num)が求められている処理があったとして、それをgetter(Int)に置き換えることはできるでしょうか。

これは問題ありません。

なぜならgetter(Num)を処理できる式は、getter(Num)の返り値となるNum型を処理できるのであり、そこがInt型を返すgetter(Int)に置き換わったとしても、問題なく処理できるはずだからです。

つまり getter(Num)な部分は、getter(Int)で置き換え可能なので、

getter(Num) >= getter(Int)

となります。

これは元のサブタイピングの関係(Num >= Int)と方向が一緒なので「それぞれの型を返す関数を作る」getter型構築子は共変(covarient)である、と言えます。

setterは反変

次にsetter型をつくる型構築ルールを次のように定義します。

setter(A) = A -> ()

型Aを受け取って何かをする、という型です。

つまり

  • setter(Num): Num -> ()
  • setter(Int): Int -> ()

このとき、setter(Num)が求められている箇所を、setter(Int)に置き換えることは出来るでしょうか。

これは出来ません。

なぜなら、Int型だけじゃなくFloat型も受け取るであろうsetter(Num)を前提に書かれた箇所を、Int型しか扱えないsetter(Int)で置き換えることはできないからです。

しかし、その逆はできるのです。

つまり、setter(Int)を受け取る部分を、setter(Num)に置き換えることは出来ます。

なぜなら、setter(Int)が受け取る型のすべて(といってもIntだけですが)を、setter(Num)は受理できるからです。

よって、型変換後の両者の対応関係は、

setter(Int) >= setter(Num)

となり、これは元のサブタイピングの関係性(Num >= Int)と方向が逆なので、「それぞれの型を受け取って何かする関数を作る」というsetter型構築子は反変(contravarient)である、と言えます。

(こんな感じの理解でいいのかな?)

参考:反変性と共変性(計算機科学)