存在量化(和訳)

型の中で存在量化された型変数を許す．

データ型宣言での存在量化子の利用のアイデアはPerryによって提案され，Hopeらによって実装された．その後，LauferとOderskyによって形式化された．Lennart AugustssonのhbcというHaskellコンパイラで数年使われ，非常に有用と判明した．ここにそのアイデアを書く．次の宣言を考えてみよう．

code: EQ1.hs

data Foo = forall a. MkFoo a (a -> Bool)

| Nil

code: EQ2.hs

MkFoo :: forall a. a -> (a -> Bool) -> Foo

Nil :: Foo

code: EQ3.hs

code: EQ4.hs

f (MkFoo val fn) = ???

code: EQ5.hs

f :: Foo -> Bool

f (MkFoo val fn) = fn val

これにより，異種の値をそれらを操作する一連の関数とともにパッケージングし，そのパッケージの集まりを同じ方法で取り扱うことができる．存在型でこのようにOOPのようなプログラミング(ダック・タイピング)をかなり表現することができる．

なぜ存在か？

code: EQ6.hs

MkFoo :: (exists a. (a, a -> Bool)) -> Foo -- 擬似コード

しかし，Haskellプログラマは前述したように，普通の全称量化された型を安全に考えることができ，それによって新しい存在量化された構造を追加することを避けることができる．

存在と型クラス

簡単な拡張はコンストラクタの前に任意のコンテキストを許すことだ．例えば次のようになる．

code: EQ7.hs

data Baz = forall a. Eq a => Baz1 a a

| forall b. Show b => Baz2 b (b -> b)

2つのコンストラクタは期待通り次のような型を持つ．

code: EQ8.hs

Baz1 :: forall a. Eq a => Baz1 a a -> Baz

Baz2 :: forall b. Show b => Baz2 b (b -> b) -> Baz

しかし，Baz1でパターンマッチングをすると，マッチした値を同値比較でき，Baz2でパターンマッチングすると最初にマッチした値を文字列に(関数を適用できるのはもちろん)変換することができる．故に次のプログラムは合法である．

code: EQ9.hs

f :: Baz -> String

f (Baz1 p q) | p == q = "Yes"

| otherwise = "No"

f (Baz2 v fn) = show (fn v)

レコードのコンストラクタ

GHCはレコード構文とともに存在型を使用することも許す．例えば，以下のようなコードが書ける．

code: EQ10.hs

data Counter a = forall self. NewCounter

{ _this :: self

, _inc :: self -> self

, _display :: self -> IO()

, tag :: a

}

これらの隠しフィールドを利用するには，いくつかのヘルパー関数を作成する必要がある．

code: EQ11.hs

inc ::Counter a -> Counter a

inc (NewCounter x i d t) = NewCounter

{ _this = i x, _inc = i, _display = d, tag t }

display :: Counter a -> IO ()

display NewCounter{ _this = x, _display = d } = d x

これにより，様々な内部的に異なる実装をもつカウンタを定義できる．

code: EQ12.hs

counterA :: Counter String

counterA = NewCounter

{ _this = 0, _inc = (1+), _display = print, tag = "A" }

counterB :: Counter String

counterB = NewCounter

{ _this = "", _inc = ('#':), _display = putStrLn, tag = "B" }

main = do

display (inc counterA) -- print "1"

display (inc (inc counterB)) -- print "##"

存在型(とGADT)に対するレコードの更新構文はサポートされている．

code: EQ13.hs

seTag :: Counter a -> a -> Counter a

seTag obj t = obj{ tag= t}

レコード更新の規則は以下の通りである．

更新されたフィールドの型はデータコンストラクタの全称量化された型変数のみを記述できる．GADTsの場合，フィールドには，コンストラクタの結果の型に単純な型変数引数として表示される型だけが記述される．

例としては，

code: EQ14.hs

data T a b where { T1 { f1 :: a, f2 :: b, f3 :: (b, c) } :: T a b } -- cは存在量化された型変数

upd1 t x = t { f1 = x } -- OK: upd1 :: T a b -> a' -> T a' b

upd2 t x = t { f3 = x } -- BAD (f3の型にはcが記述されており，cは存在量化された型変数であるため)

upd3 g x = g { g1 = x } -- OK: upd3 :: G a b -> a' -> G a' b

upd4 g x = g { g2 = x } -- BAD (g2の型にはcが記述されおり，これはG1の結果の型の単純な型変数引数ではない)

制限事項

存在量化されたコンストラクタを使用する上ではいくつかの制限がある

パターンマッチングする時，各パターンマッチでは，存在量化された型変数ごとに異なる新しい型が導入される．これらの型は他の型と統一することも，パターンマッチのスコープから逃げることもできない．例えば次のコードは正しくない．

code: EQ15.hs

f1 (MkFoo a f) = a

code: EQ16.hs

f1 :: Foo -> a -- 奇妙な型

code: EQ17.hs

f1 :: forall a. Foo -> a -- 間違っている

これはただ，元のプログラムが明白に間違っているだけである．他のエラーとして次のコードが有る．

code: EQ18.hs

f2 (Baz1 a b) (Baz1 p q) = a == q

code: EQ19.hs

f3 x = a == b where { Baz1 a b = x }

code: EQ20.hs

f3 x = case x of Baz1 a b -> a == b

code: EQ21.hs

newtype T = forall a. Ord a => MkT a

code: EQ22.hs

code: EQ22.hs

instance Eq T where

(MkT a) == (MkT b) = ???