■

何となく自分で何がしたかったのか思い出したのと、色々混乱してたのと。

例えば、私としては、HaskellやCleanのような言語でtupleが圏論的な意味での積になってることを示したい。tupleが圏論的な意味で積になってるというのは、任意の型a,b,cと関数f:c->a,g:c->bがあったら、型c->(a,b)を持つ関数で、fst.=f,snd.=gを満たすものが(observationally equivalentなものを除いて)一意的に存在するということ。は勿論、=(\x -> (f x,g x))で簡単に作れて、逆にそういう関数hが存在すると、==(\x -> (fst (h x) , snd (h x))なので、(fst w,snd w)=wが言えれば、一意性もすぐに従う。これって当たり前に見えるけど、どうなんだろう。Sparkleで証明しようとしたけど、無理っぽい気が。(fst w,snd w)=wは、むしろ公理として採用すべき?System Fだとparametricityを仮定するとかしないと言えない(System Fでは、tupleの定義は、forall x.(a->b->x)->x)。だから、System Fばりにtupleの定義として、forall x.(a->b->x)->xを使っても、parametricityのような原理はSparkleでは使えないので、証明はできない。

あと、Haskell(というか、GHC拡張使わないとダメだけど)だと、

{-# OPTIONS -fglasgow-exts #-}
pair :: (a,b) -> (forall x.(a->b->x)->x) 
pair (x,y) = (\f -> (f x y))

fst' :: (forall x.(a->b->x)->x)->a
fst' f = f (\x y -> x)
snd' :: (forall x.(a->b->x)->x)->b
snd' f = f (\x y -> y)

pair' :: (forall x.(a->b->x)->x) -> (a,b)
pair' f = (fst' f , snd' f)

というのが書けて、pair' (pair (x,y)) = (x,y)はすぐ言えるけど、pair (pair' f) = fは言えない気がするので言えるといいなとか、型forall x.(x->x)->x->xを持つclosed termは同値な表現を除けば、Church数しか存在しないとか、始代数と終余代数が一致するとか、勿論融合変換とか。でまあ、結局Sparkleは多相ラムダ計算を十分に扱えないかな〜と思った。もっとも、

こんなこと証明できても何の役にも立たないけどね

#Haskellでは、seqがあるために、型forall x.(x->x)->x->xを持つclosed termはChurch数でないものも存在するけど。seqはshortcut fusionも成立しなくなるので、なくなるべき

Prelude> :set -fglasgow-exts
Prelude> let c1 (f::t->t) =(\x -> f x)
Prelude> let c1' (f::t->t) =(\x-> f $! x)
Prelude> c1 (\_->3) undefined
3
Prelude> c1' (\_->3) undefined
*** Exception: Prelude.undefined
Prelude> :t c1
c1 :: forall t. (t -> t) -> t -> t
Prelude> :t c1'
c1' :: forall a. (a -> a) -> a -> a

というわけでSparkleの話はおわり。さよならClean。で、どうすればいいのかということについてはよく分からない

A Logic for Parametric Polymorphismは面白いけど、どうなんだろうなぁ