存在型のどのへんが存在量化なのか

特にHaskellの存在型について

わかりにくい点

存在量化の話をしているはずなのにforallというキーワードを使っている

基本的にはこれに尽きるmrsekut.icon

でもまあ実際、forallを導入するだけで存在型を作れちゃうわけだから仕方がない

仮にexistsを導入したところで使用するタイミングがない

普通の関数での全称量化

Haskellにおける普通の型引数は暗黙的に全称量化されているようなもの

code:hs

id :: a -> a -- 普通の書き方

id :: forall a. a -> a -- ExistentialQuantificationを使った

ExistentialQuantificationを使うことでforallが使えるようになる

意味としては何も変わっていない

PureScriptでは常にこれを明示する必要がある

ただし、関数定義時のみの話mrsekut.icon

全称量化された型

普通の型定義を考える

code:hs

data Hoge a = HogeC { runHoge :: a }

わかりやすさのため、型コンストラクタと値コンストラクタを別の名前にしているmrsekut.icon

このような定義すると、同時に以下のような関数を定義したことになる

code:hs

HogeC :: 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である

存在量化された型

存在型を定義したとき

code:hs

data Foo = forall a. FooC { runFoo :: a }

わかりやすさのため、型コンストラクタと値コンストラクタを別の名前にしているmrsekut.icon

このような定義すると、存在量化された型と同様に考えれば、同時に以下のような関数を定義したことになる

code:hs

FooC :: forall a. a -> Foo

runFoo :: exists a. Foo -> a

existsというキーワードはHaskellにはないmrsekut.icon

型関数FooCは、

任意の型aをとって、Foo型を作る

Foo型の値を作るための値constructorである

関数runFooは、

Fooから、aを取り出す

Foo型のdeconstructorである

この定義は、「Fooから取り出せる何らかのa型が存在する」というように読める

実際、このrunFooは手動で定義するものではなく、data Foo ..を定義すれば自動で手に入る関数なので、existsを自分で使用する機会がないmrsekut.icon

よってexistsというキーワードは処理系に導入する必要がない

runFooの定義はなんでforallじゃないのか

code:hs

runFoo' :: 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は以下のように書くのと何が違うのか？

code:hs

runHoge' :: exists a. Hoge a -> a

これは「「Hoge aからa取り出せる」ような何らかの型aが少なくとも1つは存在する」と読める

∃x. Pxは、∀x. Pxを含意するので、主張として弱くなる

存在型とか関係なく、通常の論理式の話

つまり、「どのへんが存在量化なのか」と問われると、

deconstructorが存在量化になっている、と回答することになる

だから、data Foo = forall a. FooC aのような型が存在型でっせ、と見せられても瞬時にはどのへんが存在量化なのか分かりづらい

#??

命名が厳しくない？という可能性はある

しらんけどmrsekut.icon

これに対して「存在型」と命名したことによる認識の難しさみたいなものはありうる

ただ、読んでないけどTaplの「存在型」の1つ前の章が全称型なので、その対比を見ればピッタリの命名だったりするのかもしれん