CPL

メモ。
http://www.tom.sfc.keio.ac.jp/~sakai/hiki/?CPL

論文。Categorical Programming Language
http://www.tom.sfc.keio.ac.jp/~hagino/thesis.pdf

Charity。
http://pll.cpsc.ucalgary.ca/charity1/www/home.html

論文。About Charity
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.51.2805
Charity is a categorical programming language based on distributive categories (in the sense of Schanuel and Lawvere) with strong datatypes (in the sense of Hagino)
だそうな。後はまあどうでもいい(酷

とりあえず、CPL。何を言ってるのか理解するのに30分くらいかかったけど、全部普遍性が基礎になってるらしい。

right object prod(a,b) with pair is
  pi1: prod -> a
  pi2: prod -> b
end object;

は「任意の対象xと射f:x->a,g:x->bが与えられているとき、射h:x->prod(a,b)で
pi1.h=f
pi2.h=g
を満たすものが一意的に存在し、これをpair(f,g)と書く」と読むらしい。分かりづらい。

結局、上のように書くと
pair :: (x->a) -> (x->b) -> (x -> prod a b)
prod :: a -> b -> prod a b
pi1 :: prod a b -> a
pi2 :: prod a b -> b
という4つの関数と、
pi1.(pair f g) = f
pi2.(pair f g) = g
という2つの書き換え規則が定義されると考えればいいっぽい？

right objectがあれば、left objectもあって

left object coprod(a,b) with case is
  in1: a -> coprod
  in2: b -> coprod
end object;

は「任意の対象xと射f:a->x,g:b->xが与えられているとき、射h:coprod(a,b)->xで、
h.in1=f
h.in2=g
を満たすものが一意的に存在し、これをcase(f,g)と書く」と読む。

CHARITYの方では、直積は組み込みであるらしい。直和は、

data coprod(A, B) -> X = in1: A -> X
                       | in2: B -> X.

で定義される。

Haskellだと

data Coprod a b = In1 a
                | In2 b

なので、まあ似ている。

とりあえず感想と疑問(論文をちゃんと読めば書いてあるのかもしれないけど)
・圏論の概念を用いているけども、普遍性は「存在すれば一意的」であることしか保証しないのに対して、こっちは定義できるものはなんでも存在できる世界。terminal objectは若干別腹
・Categorical Combinatory Logicのような体系だと、書き換え規則は、天下り的に与えられる(圏論にinspireされたものだけど)のに対して、こっちは書き換え規則は定義から生成されるのが大きな違いっぽい
・CPLの方が、CHARITYよりもprimitiveなとこから始めてるっぽい
・CPLとCHARITYの差は？
・CHARITYは、distributive categoryを基礎にしているらしいけど、CPLではdistributiveあることは保証されない？(そもそも、CHARITYがdistributiveである理由も分かってないけど)
・CHARITYでは、全ての計算は停止するらしいけど、CPLでは?(停止しそうな気はするけど)
・CPLやCHARITYで計算の合流性は保証されるんだろうか？