存在型のどのへんが存在量化なのか
特にHaskellの存在型について
わかりにくい点
存在量化の話をしているはずなのに
forall というキーワードを使っている基本的にはこれに尽きる
でもまあ実際、
forall を導入するだけで存在型を作れちゃうわけだから仕方がない仮に
exists を導入したところで使用するタイミングがない普通の関数での全称量化
Haskellにおける普通の型引数は暗黙的に全称量化されているようなもの
hsid :: a -> a -- 普通の書き方
id :: forall a. a -> a -- ExistentialQuantificationを使ったExistentialQuantificationを使うことで
forall が使えるようになる意味としては何も変わっていない
PureScriptでは常にこれを明示する必要がある
ただし、関数定義時のみの話
全称量化された型
普通の型定義を考える
hsdata Hoge a = HogeC { runHoge :: a }わかりやすさのため、型コンストラクタと値コンストラクタを別の名前にしている
このような定義すると、同時に以下のような関数を定義したことになる
hsHogeC :: forall a. a -> Hoge a
runHoge :: forall a. Hoge a -> a型関数
HogeC は、任意の型
a を取って、 Hoge a 型を作る Hoge a 型の値を作るための値constructorである関数
runHoge は、任意の型
a に対して、 Hoge a から、 a を取り出す Hoge a 型のdeconstructorである存在量化された型
存在型を定義したとき
hsdata Foo = forall a. FooC { runFoo :: a }わかりやすさのため、型コンストラクタと値コンストラクタを別の名前にしている
このような定義すると、存在量化された型と同様に考えれば、同時に以下のような関数を定義したことになる
hsFooC :: forall a. a -> Foo
runFoo :: exists a. Foo -> a exists というキーワードはHaskellにはない型関数
FooC は、任意の型
a をとって、 Foo 型を作る Foo 型の値を作るための値constructorである関数
runFoo は、 Foo から、 a を取り出す Foo 型のdeconstructorであるこの定義は、「
Foo から取り出せる何らかの a 型が存在する」というように読める実際、この
runFoo は手動で定義するものではなく、 data Foo .. を定義すれば自動で手に入る関数なので、 exists を自分で使用する機会がないよって
exists というキーワードは処理系に導入する必要がない runFoo の定義はなんでforallじゃないのかhsrunFoo' :: forall a. Foo -> a この場合、「
runFoo' は、 Foo から、任意の a を取り出す」と読めるしかし、実際の
runFoo は「任意の a を取り出せる」わけではない runFoo はdeconstructorなので、もともと Foo 型の値がどこかにある前提で、それに対して使うのだから、そのどこかの
Foo の中身が、 Int と String しかないような状況も普通にありうるわけで、その状況下で「任意の
a を取り出せる」わけはなく、「
Int か String 」しか取り出せないそれを論理式風に書くなら、「
Foo から取り出せる何かしらの型 a が存在する」となるではなぜ、
runHoge :: forall a. Hoge a -> a は、 exists じゃないのかここで、全称量化の方の話に戻った時に、
runHoge は以下のように書くのと何が違うのか？hsrunHoge' :: exists a. Hoge a -> aこれは「「
Hoge a から a 取り出せる」ような何らかの型 a が少なくとも1つは存在する」と読める∃x. Pxは、∀x. Pxを含意するので、主張として弱くなる
存在型とか関係なく、通常の論理式の話
つまり、「どのへんが存在量化なのか」と問われると、
deconstructorが存在量化になっている、と回答することになる
だから、
data Foo = forall a. FooC a のような型が存在型でっせ、と見せられても瞬時にはどのへんが存在量化なのか分かりづらい命名が厳しくない？という可能性はある
しらんけど
これに対して「存在型」と命名したことによる認識の難しさみたいなものはありうる