Existential Types
Existential typeとは、(1)のようにforallがデータコンストラクタの前について定義されるデータ型のことをいう*1。(2)とは違って、forallで修飾された型変数ができあがった型のパラメータになっていないことに注意して欲しい。
(1)
data Proc i o = forall b c. Proc (i -> b) (b -> c) (c -> o) data Obj = forall a. Show a => Obj a
(2)
data ProcX i b c o = ProcX (i -> b) (b -> c) (c -> o) data Show a => ObjX a = ObjX a
Existential typeの定義は、Objを例に取ると、このように読める。
「任意の(forall)Showクラスに属す型aに対し、変数xの型がaであれば、Obj xはObjという型になる」
また、逆にコンストラクタを外すことを考えると、
「yの型がObjであれば、Showクラスに属する型aが何かあって(exists)、y@(Obj x)のxの型はaである」
ということがわかる。前者はデータコンストラクタを中心においた理解で、後者はできあがった型とはどういうものかという理解だといえるだろう。後者の考え方*2がexistential typeという名前の由来である。
データコンストラクタの型
Proc :: forall i o b c. (i -> b) (b -> c) (c -> o) Obj :: forall a. Show a => a -> Obj a
例
Procは複数の手続きを一体にまとめて外に途中の型を漏らさないという例である。
runProc :: i -> o runProc (Proc f g h) = h . g . f testProc1 :: Proc Int Int testProc1 = Proc (* 10) show length testProc2 :: Proc Int Int testProc2 = Proc (+ 1) (* 2) (`div` 8)
Objのようにtype classと併用することも多い。同じクラスに属するオブジェクトの型を区別しないで扱うことができる。以下はheterogeneous*3なリストを作れるという例である。x :: Objからx@(Obj y)の中身yについてわかることは、型がShowクラスに属するということだけである。したがってyに対してできることは「Showクラスに属する型の変数になら必ずできること」に制限されている。
objs = [Obj 1, Obj "str", Obj True] testObj = map f objs where f (Obj y) = show y
Type classを用いず、直接「メソッド」を持たせて「オブジェクト」を作ることもできる。
data Obj = forall a. Obj a (a -> Bool) bools = [f x | (Obj x f) <- [Obj 3 even, Obj 'c' isUpper]]
応用(Dependent types)
以下のように、実行時に値から型を作ることもできる。これは静的チェック時には型情報が外にもれないことを利用している。
type Vector1 = Double type Vector2 = (Double, Double) data AVec = forall v. Vec v => AVec v -- Value to Types tovec :: [Double] -> AVec tovec [x] = AVec x tovec [x,y] = AVec (x, y) -- Types to Values apply :: (forall v. Vec v => v -> r) -> AVec -> r apply f (AVec v) = f v -- Main program prog :: Vec v => v -> String prog = show class Show v => Vec v where instance Vec Double where instance Vec (Double,Double) where
*Dependent> apply prog $ tovec [1,2] "(1.0,2.0)" *Dependent> apply prog $ tovec [1] "1.0"
