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)である、と言えます。
(こんな感じの理解でいいのかな?)