最近OCamlという言語でプログラミングの勉強をしている。↓の素晴らしい本を読んでいる。
*1日本はOCamlほかML系言語の研究者がけっこういて、本やネット上の解説が充実している。助かる。MLというのはMeta Languageの略で、大計算機科学者のロビン・ミルナーの研究に端を発する言語である。OCamlもこの流れに位置する。
MLは多相型システムというのを持っている。これはジラール先生が開発したシステムFという論理体系とカリー=ハワード的な対応を持っている、とごく大雑把には言える。なのでジラール主義者たるわたし的には興味深い。
OCamlはフランスの研究所発祥なのでジラール主義者の私にはさらに興味深い。OCamlはObjective Camlの略で、Camlという言語にオブジェクト指向を搭載したものという意味を持つ。Camlの部分はCategorical Abstract Machine Languageに由来するとか（なのでCamlの"ml"の部分はMeta Languageではないらしい）。Categorical Abstract Machineはフランスの論理学者・計算機科学者たちが提唱した圏論を使った計算モデルである。
これを言語として実装したのがCamlらしい。↓の本やWikipedia情報。
Categorical Abstract Machineにはラフォンという人が開発した線形バージョンもある。ラフォン先生はジラール先生の高弟である。このLinear Abstract Machineについては↓の本に解説がある（まだちゃんと読んでない）。
こうしたフランスの研究の流れのなかでCoqも生まれている。Coqの処理系はOCamlで書かれていてOCamlと関係が深いらしい。
フランスの論理学・計算機科学現代史はなかなかおもしろく、もっとちゃんと調べたいところ。フランス語の勉強も頑張ります。
