圏論プログラミング言語 CPL

プログラミング

Hagino’s Categorical Programming Language について紹介します。

wikipedia:CPL (圏論プログラミング言語)によれば、

CPL (正式名称：Categorical Programming Language) は圏論に基づいたデータ型の定義と計算モデルを持つ関数型プログラミング言語であり、1987年、萩野達也によって発案された。圏論の計算機科学に対する応用の黎明期に生まれた言語である。

CPL (圏論プログラミング言語)

ということです。1987年なので、まあ昔に作られた言語です。JavaやRubyよりも前。

CPLのデータ型

CPLでは、様々なデータ型を、CPLのプログラム中で定義できます。直積も、直和も、自然数も、そして関数も定義可能です。

ユニット型（終対象）1はこう定義されます:

right object 1 with ! is
end object


直積prodの定義はこんな感じ:

right object prod(A,B) with pair is
  pi1: prod -> A
  pi2: prod -> B
end object

直和（余積）coprodはこう:

left object coprod(A,B) with case is
  in1: A -> coprod
  in2: B -> coprod
end object

自然数の定義:

left object nat with pr is
  0: 1 -> nat
  s: nat -> nat
end object

リストの定義:

left object list(A) with prl is
  nil: 1 -> list
  cons: prod(A, list) -> list
end object

そして関数（冪対象）の定義:

right object exp(A,B) with curry is
  ev: prod(exp, A) -> B
end object

定義の構文はこんな感じです。

{left|right} object 関手(型変数1, ..., 型変数n) with 仲介射 is
  自然変換1: 型式1 -> 型式1'
  ...
  自然変換m: 型式m -> 型式m'
end object

自然変換の型式に、定義中の関手が現れる場合は、型変数を省略し、関手だけを書きます。

CPLのプログラム

CPLのプログラムは自然変換として、A型のデータはユニット型（終対象）から対象Aへの射として表現されます。ただし、データは次のように、left objectの自然変換{\alpha_L}かright objectの仲介射{\psi_R}(e_1, \cdots, e_n)を合成したものと定義されています。

{ \displaystyle c ::= I \mid \alpha_L \circ c \mid \psi_R (e_1, \cdots, e_n) \circ c }

例えば、次のようなものがデータです。

I
!.I
0.I
s.0.I
s.s.0.I
pair(s.0, s.s.0).I
curry(pi2).I

Iは恒等射を表します。通例、恒等射は省略されます。

次のプログラムは自然数の足し算を行います。

ev.pair(pr(curry(pi2), curry(s.ev)).pi1, pi2)

CPLのデータ型の正体

データ型の定義に、rightとかleftとか付いていますよね？ CPLのデータ型には、右随伴関手として定義されるものと左随伴関手として定義されるものの2種類があります。論文にはこう書いてあります。

従来の言語では, 右随伴関手は言語本来に与えられており, プログラマーは左随伴関手を使って自分のデータ型を定義していた.

カテゴリー理論的関数型プログラミング言語

left objectの自然変換 = 代数データ型のコンストラクター

自然数の定義を見ると、普通の代数データ型の定義と同じように見えますよね。例えば、Haskellでも次のように定義できるわけです。（GADTの記法を使っていますけど）

data Nat where
    Zero :: Nat
    Succ :: Nat -> Nat

left objectの自然変換は、代数データ型のコンストラクターに対応しているようです。

left objectの仲介射 = パターンマッチによる分岐

それでは、仲介射は何に対応するのか。HaskellのEither型には、either :: (a -> c) -> (b -> c) -> Either a b -> cという関数が定義されていますけど、これがCPLのcoprodのcaseに相当します。f : A -> C, g : B -> Cのとき、case(f,g) : coprod(A,B) -> Cです。

つまり、おおざっぱに言えば、CPLのleft objectの仲介射は、パターンマッチによる分岐に相当します。ほんとうは、natやlistのような再帰的データ型では、foldに対応します。（catamorphismだそうです。）

right objectの自然変換 = オブジェクトのメソッド

論文には「右随伴関手は言語本来に与えられており」と書かれているわけですけど、これは関数型プログラミング言語を見た場合、タプルとか関数とかはプリミティブだってことです。まあレコード型とかは自分で定義できますけどね。

でも本当は、他の言語にもright object相当の物があります。CPLにおけるright objectはオブジェクト指向プログラミングのオブジェクトの定義と一緒です。

代数と余代数、クラスと余クラス - 檜山正幸のキマイラ飼育記

Javaで関数オブジェクトのインターフェースを定義できますよね。

interface Function<A,B> {
    public B call(A a);
}

CPLでの関数の定義をもう一度載せます。

right object exp(A,B) with curry is
  ev: prod(exp, A) -> B
end object

自然変換evが、callメソッドに対応していることが分かります。

right objectの仲介射 = オブジェクトのインスタンス

right objectの仲介射は、インスタンスです。例えば、curryを使って関数オブジェクトのインスタンスが作れます。

curry(s.pi2)

メソッドの引数との直積にして、ev“メソッド”を合成することで、“メソッド呼出し”ができます。

ev.pair(curry(s.pi2), 0)

JavaScriptで書けば、こういうことですね。

var obj = {ev: function(x) {return x + 1;}};
obj.ev(0);

（これはanamorphismですかね。）

まとめ

まとめると、CPLのleft objectは他の言語でenumだとかvariantだとかADTだとか呼ばれるようなもの、CPLのright objectは他の言語でrecordだとかstructだとかclassだとかinterfaceだとか呼ばれるようなものだと言えます。これでCPLのプログラムが読めますね!

オダンゴ図によるプログラムの表現

こんな感じでプログラムを絵にかいて見てみることもできます。カリー化の表記などは、檜山さんの記事を大いに参考にしています。モノイド閉圏、オダンゴ、留め金、池袋 - 檜山正幸のキマイラ飼育記

参考文献

こちらは酒井政裕さんによるイントロダクション。