/LugendrePublic/存在量化(和訳)

generated at 2/17/2025, 9:51:01 PM
存在量化(和訳)
原文

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

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

 EQ1.hsdata Foo = forall a. MkFoo a (a -> Bool)
        | Nil


データ型 Foo には，次の型を持つ2つの型コンストラクタがある．

 EQ2.hsMkFoo :: forall a. a -> (a -> Bool) -> Foo
Nil   :: Foo


 MkFoo 型の型変数 a はデータ型 Foo には現れない．例えば，次の式は問題ない．

 EQ3.hs[MkFoo 3 even, MkFoo 'c' isUpper] :: [Foo]


ここで， (MkFoo 3 even) は整数を Bool にマップする関数 even と整数をパッケージングする．加えて， (MkFoo 'c' isUpper) は，文字とそれを使う関数をパッケージングしている(訳注：ここでのパッケージングとは関数と整数の情報をまとめているということ)．これら2つはそれぞれ Foo 型であり，単一のリストに入れることができる．

我々は Foo 型の値で何ができるだろうか？特に， MkFoo でパターンマッチングをするとどうなるだろうか？

 EQ4.hsf (MkFoo val fn) = ???

我々が val と fn について知ってることはその2つの間に互換性があるということだけなので，我々ができそうな唯一の意味のあることは fn を val に適用して， Bool 値を得ることだけである．例えばこんな感じ：

 EQ5.hsf :: Foo -> Bool
f (MkFoo val fn) = fn val

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


なぜ存在か？

これは存在量化とどこが関係しているだろうか？単に， MkFoo が以下とほぼ同型の型を持っているからである．

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

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

存在と型クラス

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

 EQ7.hsdata Baz = forall a. Eq a => Baz1 a a
        | forall b. Show b => Baz2 b (b -> b)

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

 EQ8.hsBaz1 :: forall a. Eq a => Baz1 a a -> Baz
Baz2 :: forall b. Show b => Baz2 b (b -> b) -> Baz

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

 EQ9.hsf :: Baz -> String
f (Baz1 p q) | p == q    = "Yes"
            | otherwise = "No"
f (Baz2 v fn)            = show (fn v)

操作的には，辞書渡しによる型クラスの実装では，コンストラクタ Baz1 と Baz2 はそれぞれ Eq と Show の辞書を格納し，パターンマッチングでそれらを取り出す必要がある．


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

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

 EQ10.hsdata Counter a = forall self. NewCounter
   { _this     :: self
   , _inc      :: self -> self
   , _display  :: self -> IO()
   , tag       :: a
   }

ここで， tag はパブリックフィールドであり，型付セレクタ関数 tag :: Counter a -> a をもつ． self 型は外から隠されており， _this ,  _inc ,  _display を関数として適用しようとするとコンパイル時エラーが発生する．言い換えれば，存在量化された型変数を使わないような型を持つフィールドのみレコードセレクタ関数を生成する．(この例では，レコードセレクタが定義されていないフィールドの名前はアンダースコアから始めているが，これはただのプログラミングスタイルであり，GHCはこれを無視する．)

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

 EQ11.hsinc ::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

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

 EQ12.hscounterA :: 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)に対するレコードの更新構文はサポートされている．

 EQ13.hsseTag :: Counter a -> a -> Counter a
seTag obj t = obj{ tag= t}


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

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

例としては，
 EQ14.hsdata 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は存在量化された型変数であるため)

data G a b where { G1 { g1::a, g2::c } :: G a [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の結果の型の単純な型変数引数ではない)


制限事項

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

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

ここでは， MkFoo によって束縛された型は「逃げて」しまう．なぜなら， a は f1 の結果だからである．なぜこれが間違ってるかを理解する一つの方法は， f1 がどんな型を持っているかを調べることである．
 EQ16.hsf1 :: Foo -> a      -- 奇妙な型

結果の型でこの a とはなんだろうか？ 明らかに以下を表すものではないだろう．
 EQ17.hsf1 :: forall a. Foo -> a    -- 間違っている

これはただ，元のプログラムが明白に間違っているだけである．他のエラーとして次のコードが有る．
 EQ18.hsf2 (Baz1 a b) (Baz1 p q) = a == q

 a == b や p == q は可能だが， a == q は Baz1 コンストラクタから作られる2つの異なる型を等号で結んでいるので間違っている．

 let または where の束縛の中の存在量化されたコンストラクタに対してパターンマッチングを行うことはできない．よって次は違法である．
 EQ19.hsf3 x = a == b where { Baz1 a b = x }

代わりに case 式を使えば良い．
 EQ20.hsf3 x = case x of Baz1 a b -> a == b

一般に， case 式か，関数定義パターンでのみ，存在量化されたコンストラクタによるパターンマッチングが可能になる．この制限の理由は，実際は実装のせいである．束縛群の型検査 は，事態を複雑にしている存在量化が無い場合であっても既に悪夢である．さらに，モジュールのトップレベルでの存在型のパターン束縛は意味がない．なぜなら，存在量化された型が「逃げてしまう」のを妨ぐ明確な方法がないからである．だから今のところ，言葉で簡単に表現できる制約がある．それがいかに腹立たしいかすぐ理解できるだろう．

 newtype 宣言には存在量化は使用できない．よって次のコードは違法である．
 EQ21.hsnewtype T = forall a. Ord a => MkT a

理由：型 T の値は Ord t の辞書と型 t の値のペアとして表す必要がある．これは， newtype には具体的な表現がないという考えと矛盾する． newtype の代わりに data を使うことで，同じ効率と効果を得ることができる．オーバーロードが含まれていない場合， data は実装コストを持つため，存在量化された newtype を許可する言い分もあるわけだが，そもそも単一フィールドの存在量化されたコンストラクタはそれほど役に立たない．故に，それを変更する説得力のある理由がない限り，この単純な制限は有効である．

存在量化されたデータコンストラクタのデータ型のインスタンスを deriving で導出することはできない．殆どの場合，それは意味を成さないからである．例えば次のコードを考えよう．
 EQ22.hsdata T = forall a. MkT [a] deriving ( Eq )

通常の方法で Eq を導出するには，2つの MkT コンストラクタの単一のコンポーネントが等しい必要がある．
 EQ22.hsinstance Eq T where
   (MkT a) == (MkT b) = ???

しかしながら， a と b は明確に違う型で，故に比較できない．導出したインスタンスが意味を成す例を想像することは可能だが，単純にそのような宣言を禁止する方が簡単である．自分自身で独自のインスタンスを定義しましょう．