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