存在型
Existential type
こういうことをできる型
hs data Hoge = forall x. Hoge x左辺の引数に取らない型を、右辺で使用する
普通はこういうふうに少し制限を入れて使うはず
hsdata Hoge = forall s. Show s => Hoge s使う
Haskell
PureScript
pursって元から
forall キーワードあるけど、型定義に対しては使えないんだなだから、
data Foo = ∀ a. Foo a とかはparse errorになるユースケース
参考
一番わかりやすかった
>#WIP
理論
TaPLの24章に書いている
これが初出かどうかはわからんが、
とりあえず最初の提案者はNigel Perryらしい ref
data Foo = forall x . Foo x みたいに、型クラス制約なしで、存在型を使って嬉しいパターンってあるの？あまり実用的でない気がするけど
もしないのであれば、
Show a => のような制約を付けることとセットで覚えたほうが良い？Proxyとの関係
Pursではどうするのか
少し制限を設ける
hsdata ShowYou = forall s . Show s => ShowYou sshow型クラスに属する型のみを突っ込める型
ShowYou これで包むと、IntやBoolといった具体的な型の特徴は薄れ、
「Show型クラスに属するもの」という一段抽象度の上がったものとして捉えることができる(?)
開かれた型を定義することができる ref
具体的な型を拡張するためには、本来はその定義の部分(
data Hoge =.. )を修正しないといけなかったが、存在型を用いることで、型クラスのときのように、一つインスタンスを加えれば、その型を別の場所から拡張することができる
hsdata ShowBox = forall s. Show s => SB s
heteroList :: [ShowBox]
heteroList = [SB (), SB 5, SB True]recordに対しても使える
EQ10.hsdata Counter a = forall self. NewCounter
{ _this :: self
, _inc :: self -> self
, _display :: self -> IO()
, tag :: a
}forallが積集合で、existが和集合という説明、よくわらない #??
「存在 という言葉の説明」の節が何を言っているのかわからん
論理式とのアナロジーがほしい
この説明に依ると、
[forall a. a] は、全ての型を持つ要素のリストなので、即ち「\bot」のリストとなる全ての型の共通部分となる値はHaskellの⊥型のみ
これがまだピンと来てないが
これ合ってるの？なんで「共通部分の型のリスト」になるんだ
ボトム云々以前の話
forall a. [a] は、任意の一つの a 型に対する、 [a] 型なんでも良いが、一種類の型
a のリストe.g.
[String] , [Int] これはまあわかる
[exists a. a] が、「任意の a 型」のリスト型なんでもよく、複数種類も許容する
e.g.
[String, Int, Bool] また、以下の2つは同じ意味
data T = forall a. MkT a data T = MkT (exists a. a) これこそが存在型
hsでは
exists というキーワードはないので前者で表示されるいや、やっぱわからん
上2つの段落を並べて見れば、
data T = forall a. MkT a は、「任意の」「一種類の」型 a に対しての MkT a 上の
forall a. [a] と同様。 data T = MkT (exists a. a) は、「任意の」「複数種類も許容する」型 a に対しての MkT a こっちはわかる
って感じに解釈されない？
この説明の理解、後回しにしたほうが良さそうだな