日々の流転

λ. サブタイプと代入

http://www15.ocn.ne.jp/~rodinia/Blog/MyJournal22.html#categorymisc5

私はOCamlの型システムについては全然知らないので勘違いしているかも知れませんが、この問題は単にその型システムが安全でないというだけのように思えます。

安全な型システムであれば、型Aが型Bのサブタイプであることの必要条件として、少なくとも、Bのインターフェース中の正(負)の位置に現れる全ての型について、Aでの対応する型がそのサブタイプ(スーパータイプ)になっていることを要求するはずです。

この例では、型 <n : <y : b>; m : a> のフィールドnが代入可能ということは、この型が setN: <y : b> -> () というメソッドを持っているのと同じとみなせるので、型 <y : b> は負の位置にも現れていると考えるべきでしょう。したがって、<n : <x : a, y : b>; m : a> が <n : <y : b>; m : a> のサブタイプであるためには、<x : a, y : b> が <y : b> のスーパータイプである必要があります。しかし、これはいくらなんでも成り立ってませんよね?　それにも関わらず <n : <x : a, y : b>; m : a> を <n : <y : b>; m : a> のサブタイプと認めてしまうような型システムであれば、実行時にエラーが起こって当然だと思います。

ちなみに、サブタイピングをサポートする関数型言語の他の例としてO'Haskellがありますが、このようなコードはちゃんと型エラーになります。(以下に出てくるCmdはIOモナドみたいなものです)

-- type constructor (kind * -> *) (variance +)
struct Y y =
   getY :: Cmd y
 
-- type constructor (kind * -> * -> *) (variance + +)
struct XY x y < Y y =
   getX :: Cmd x
 
-- type constructor (kind * -> * -> *) (variance 0 +)
struct S n m =
   getN :: Cmd n
   setN :: n -> Cmd ()
   getM :: Cmd m
 
-- OK
cast1 :: S a (XY a b) -> S a (Y b)
cast1 x = x
 
-- NG
cast2 :: S (XY a b) a -> S (Y b) a
cast2 x = x
{-
ERROR "Test.hs" (line 21): Type error in variable
*** term                : x
*** type                : S (XY a b) a
*** does not match      : S (Y b) a
-}
 
-- NG
test :: S (XY a b) a -> Y b -> Cmd ()
test x y = x.setN y
{-
ERROR "Test.hs" (line 31): Type error in function application
*** term                : (.setN)
*** type                : S a b -> a -> Cmd ()
*** constraints         : Y c < a, a = XY b c
*** because             : variable has conflicting bounds
-}

λ. オブジェクトはレコード型か？

生存記録(2005-02-12) では「レコード型との違いは、自己参照できる点だと思う」と書かれているけど、任意のレコード型Aの上に不動点結合子fix_A:(A->A)->Aが定義されている世界ならば、自己参照してるレコードなんていくらでも定義できるし、あまり本質的な違いではないような気がする。

……考えていて、ふと、オブジェクトがレコード型と同一視されるのは、メッセージが(引数の違いを無視すれば)高々有限個しか存在しないからではないかと思った。高々有限個しかないから、関数をフィールドとするレコードで表現できてしまう。では、もしメッセージが有限個ではなく、しかも何らかの代数構造(プロセス代数的な何か?)を持っていたとしたらどうだろうか?

λ. OOの型理論の本

http://www15.ocn.ne.jp/~rodinia/Blog/MyJournal22.html#categorymisc7

読んだことはないですが、最も参照されているのは "A Theory of Objects", Martin Abadi and Luca Cardelli だと思います。