私はforallに疎外されている

それは私の頭が残念だからなんですが。。。

今日の昼間についつたでPolymorphismの話がちろと出たので、というか私が出してたので、そこからふと次のケースら

(1) forall a.a

(2) forall a.(Num a) => a

(3) forall a.a -> a

(4) [ forall a.a ]

(5) forall a.[ a ]

5つを取りあえず考えてみた。

まず(1)から...

(1)

うーん分からないなぁみたいな。ちょっと分からないんですよ！！

取りあえずこの時の"a"って、何なんでしょう。

兎も角、結果的に ( forall a.a )というのは何かしら型に成らないといけない筈です。多分。

取りあえず考えるにも手がかりが無かったので、ここでCurry-Howard同型対応にヒントを求めるとどうかなーとか思いました。

forall a.aのaには何かしらの型が入って行くとして、C/H同型対応的には「型=命題」「定義=証明」なわけですから、forall a.aは「全ての命題が導出/証明出来る」という事なんじゃないかーと。

するとまぁ

case1 :: forall a.a
case1 = ?

となる所の?が欲しい。数理論理学をやった事がある人はピンと来る(来るかなぁ...?)気がするのですが「あるブツからなんでもかんでも証明出来る」その時の「ブツ」っていうのは矛盾(⊥)でしかるべきで、そうすると「 ? = ⊥ 」になる筈です。

で

case1 :: forall a.a
case1 = undefined

とかやってghciに喰わせてみると型チェックをパスしたので、取りあえずこういう解釈で合ってるんですかねぇ・・・。

C/H同型対応について思いを馳せない場合はどうなるかも一応考えてみました。

上にならってcase1をそのまま使うとして、例えばcase1 = {1,2,3}でforall a.aがそれに対応する型だとします。

しかしながら、このケースでは当然a = Charだのa = Stringだのは満たせませんからダメで・・・。

所でHaskellは全ての型の要素としてbottom-type(⊥)を持っているので、そうすると case1 = {⊥}とするとaにどの型が来ても「一応不味くは無い」かなぁとか思うので・・・。

一応というのは、a = Intの時当然Int型の値として⊥,1,2,3,...があって、しかしながらcase1は値としては⊥しか持たないので1,2,3,...は許容出来ないとかそういう感じです。

凄く適当に言うと、型を値の集合と見た時に、ありうる全ての型(集合としての)の積集合を取ると⊥だけになるので、とか。

OCamlだと

# let v = Obj.magic 0;;
val v : 'a = <poly>
# v;;
- : 'a = <poly>

これなんか違うんじゃないですか・・・。OCamlでやりたい時はどうするんだろう。

(2)

型が型クラスNumの文脈で制限されてる(とかの言い方で良いんだろうっけ)ものの、積集合的な考えをすると先と同じく⊥だろうと思ってまぁ。

case2 :: forall a.(Num a) => a
case2 = undefined

とは言え、折角なので文脈Numを利用出来ないかなーと思って、なんかふわふわな感じでやれば良いんだろうから

case2 :: forall a.(Num a) => a
case2 = 1

これでも型チェックは通った。
でもこれはなんで出来るんか分かりませんね。

http://www.sampou.org/haskell/report-revised-j/basic.html#numeric-literals
これかな。

(3)

これはParametric Polymorphismなので・・・というわけにもいかないんですが・・・。

(1)と(2)で行ったような解釈が出来ないもんなんでしょうか。

id1 = \(x::t1) -> x {t1 = {⊥,1,2,3}}
id2 = \(x::t2) -> x {t2 = {⊥,'a','b','c'}}
...

とやっていって、その積集合(といってもこの場合は取り方が自明じゃないと思うんですが)を見ると結局

id = \(x::Bottom) -> x {Bottom = {⊥}}

になるんじゃないかなーと。そうすると現実と矛盾するので...

(4)

要素として⊥しか持たないリスト型

(5)

(3)と同様に不明。こちらはデータ型に対する問題だと思うんですが

[ 事実としては知っています。けれども、(3)と同様にforall自体をどう解釈していけば良いんだろうなぁと ]

結局の所

これらのforallに一貫して意味を与える術が欲しいなーという所です。

Link

http://en.wikibooks.org/wiki/Haskell/The_Curry-Howard_isomorphism

The problem with ⊥ より
However, if we work with a limited subset of Haskell's type system, and in particular disallow polymorphic types,
we have a consistent logic system we can do some cool stuff in.
http://en.wikibooks.org/wiki/Haskell/The_Curry-Howard_isomorphism

この一文がどこからやって来てるんだろう・・・という。

この辺で上の文章が出てくるんだろうかなぁ。
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.17.9230
でもこれはSubtypingな時の話(HaskellだとTypeClass使う時)だろうけど、その時ってBottomは必須なんだろうか。とも。

メモ

v :: forall a.[a]
v = [1,2,3] -- type check error
-- なんかこの辺に違和感を覚える
-- これと同じ事をOCamlでやろうとするとどうなるんだろう。

f1 :: forall a.[a] -> Int
f1 (h:_) = 1
f1 _     = 0

f1 [1,2,3] -- なんでもござれ

f2 :: [forall a.a] -> Int
f2 (h:_) = 1
f2 _     = 0

f2 [undefined] -- この類いだけ

v :: forall a.[a]
v = [1,2,3]

が出来なくてなんでや！！となるのは、f1の引数の型が同じくなっているので、そこだけ切り取ると、「同じ型シグネチャが付いている部分」に同じ値が入らない！！とかで違和感を感じていたんじゃないかと気付いた。

v :: forall a.[a]
v = ?

この定数関数vの?は、型変数aにどんな型適用が起こったとしてもそれを満たさなければいけない。そういう定義でなければ成らないのに、【?=[1,2,3]】とかだとまぁStringの型適用が起こったら一発でアウトなわけで。

すると、多分vに入りうるのはundefinedが絡むなにかだけですね多分。

「定義を書く事が出来たならば」型変数を実際の型としたもの(つまりどんなインスタンス持って来ても良い)として考えても良くなるんですねハイ。

結局

f2 :: [forall a.a] -> Int
f2 (h:_) = 1
f2 _     = 0

f2 [1,2,3]

とかが出来ないのは、これは当然な話で、定義が書けたとしても[forall a.a]{forall a.aはundefinedしか無い}にforall a.(Num a) => [a]を持ってくる事は出来ませんから、これは引数に適用する段階の話でアウト。

結局

コメントあたりにあるのですが、定義した式が適切な型全てを持てなければなりません。

それに従えば

x :: forall a.a
x = 42

これでは当然あれですので

x :: forall a.a
x = undefined

にしか成れません。

コレに従って、

id :: forall a.a -> a
id x = x

これが何故適切な定義になっているかというと、引数として与えられる型を上手く使っている(といってもただそのまま返している)からです。

_head :: forall a.[ a ] -> Maybe a
_head [h : _ ] = Just h
_head _        = Nothing

これもまぁもう完全にそういう事です。

重要なのは、「自分の行った定義」が「型シグネチャを満たすか」どうかですそういうことです。

私が誤解していたのは

x :: forall a.a
x = 42

これは出来るべきで、というのも「どんな型でも大丈夫っていう型シグネチャを与えたんだから」「42」ぐらい入らないといかんだろ！！と。

全く逆で、定義が与えられて型シグネチャが付くからこそ42やらなんやらが与えられるようになるってことです。ハイ。

眠いです。