圏論学習ソフト FQL++ 入門

「関手データモデル／圏論データベース： その後の発展と現状 (2016)」 にて：

FQL IDEがサポートする4つの言語のなかで、位置付けがハッキリしないカワイソウなFQL++ですが、「圏論の学習にはとても有用」という特徴があります。これだけを切り出して圏論学習ツールにして欲しいくらいです。FQL++に関しては、いずれ別な記事で語りたいと思っています。

FQL++について語ります。2013年の記事「圏と関手をできるだけ簡単に書き下す方法」の内容を、FQL++で書いてみます。

内容：

1. FQL IDEのインストールと実行
2. 圏を記述してみる
3. FQL++の構文
4. 無限圏の扱い
5. 関手の記述
6. FQL++と圏論

FQL IDEのインストールと実行

FQL IDEは、http://categoricaldata.net/fql.html からダウンロードできます。Javaのjarファイルfql.jarと、各プラットフォームごとのインストーラー（fql.dmg, fql.exe, fql.rpm, fql.deb）が用意されています。インストーラーにはJava8のランタイムが同梱されているので、事前にJava8をインストールする必要はありません。

Java8の実行環境が既にあるのなら、jarファイルだけでいいでしょう。そうでないならインストーラーをダウンロードして実行するのがお手軽です*1。

jarファイルやインストーラーのファイル名にバージョンは埋め込まれていません。インストールしたソフトウェアを起動して[About]ダイアログを開いてもバージョン情報が出ないようです。インストールされたディレクトリのapp/CatDataIDE.cfgにバージョン情報が書いてありました、1.0です。

app.name=CatDataIDE
app.mainjar=fql.jar
app.version=1.0

Webページの説明では"FQL IDE"という呼称が使われていますが、ソフトウェア自体は"CatDataIDE"という名前のようです。

FQL IDEの起動方法は、プラットフォームやインストール方法により違いますが、起動してしまえば、プラットフォームに依存しないGUI操作となります。洗練されたGUIとは言いがたいですが、シンプルかつオーソドックスなので難しいことはないでしょう。

メニューのLoad Example:から、色々なサンプルを眺めると、FQL IDEがサポートする言語の雰囲気が分かるでしょう。各言語のマニュアルは次にあります。

• FQL http://categoricaldata.net/fql/tutorial.pdf
• FQL++ http://categoricaldata.net/fql/tutorial2.pdf
• OPL http://categoricaldata.net/fql/oplManual.pdf

圏を記述してみる

「圏と関手をできるだけ簡単に書き下す方法」において、次のようなグラフで表される圏を、

次のような構文で記述することを提案しました。

category Foo {

 f: A -> B,

 g: B -> C,

 h: A -> C

}

この例を、FQL++で記述してみます。FQL IDEを起動して、[File]-[New FQL++]で新しいタブを作って、そこに次のように書きます。（デフォルトのタブはFQL構文なのでダメです。）

category Foo = {

 objects A, B, C;

 arrows

  f: A -> B,

  g: B -> C,

  h: A -> C;

 equations;

}

[Run]ボタンを押すと、FQL IDE内部に圏が生成されて、4種の形式: Schema, Graph, Table, Text で閲覧できるようになります。このなかでSchema形式は、圏の宣言（上記のソースコード）を可視化したグラフで、次のようになります。冒頭に挙げたGraphVizのグラフと、内容的には同じものです。

FQL++の構文

前節の例から分かるように、FQL++の構文は、「圏と関手をできるだけ簡単に書き下す方法」で僕が使っていた擬似構文と酷似しています。違いは、僕がキータイプ数を節約して出来るだけ短く書けることに拘ったのに対して、FQL++は冗長さを気にしてない点でしょうか。

FQL++の圏の定義には、objects, arrows, equations の3つのパートがあり、それぞれキーワードで始まりセミコロンで終わります。中身が空であってもパートを省略することはできません。したがって、一番短い圏の記述は次のようになります。

category EmptyCat = {

 objects;

 arrows;

 equations;

}

equationsの部分には、パス同値関係（path equivalence relations）を書きます。パス同値関係については、「圏と関手をできるだけ簡単に書き下す方法」や「衝撃的なデータベース理論・関手的データモデル 入門」で説明しています。また、パス同値関係を記述するためのパス記法に関しては「関手データモデル入門 3：とても便利なスピヴァック流パス記法」で述べています。

「圏と関手をできるだけ簡単に書き下す方法」に出した、パス同値関係を含む例：

category Foo {

 f: A -> B,

 g: B -> C,

 h: A -> C
 where f;g = h

}

これをFQL++で書くと次のようです。

category Foo = {

 objects A, B, C;

 arrows

  f: A -> B,

  g: B -> C,

  h: A -> C;

 equations A.f.g = A.h;

}

もうひとつの例：

category Iso {

 f: A -> B,

 g: B -> A
 where

  f;g = A,

  g;f = B

}

これは、

category Iso = {

 objects A, B;

 arrows

  f: A -> B,

  g: B -> A;

 equations

  A.f.g = A,

  B.g.f = B;

}

この圏IsoをFQL IDEでGraph表示すると次のようになります。

無限圏の扱い

「圏と関手をできるだけ簡単に書き下す方法」の2番目の例は次です。

category Bar {

 u: A -> X,

 v: X -> B,

 g: B -> B,
 C,

 Y

}

これをFQL++に翻訳すると：

category Bar = {

 objects A, B, C, X, Y;

 arrows

  u: A -> X,

  v: X -> B,

  g: B -> B;

 equations;

}

[Run]するとエラーになってしまいます。

Error in category Bar: Category is infinite (contains self-loop and no equations)

圏を生成するグラフに自己ループ辺があるので、g, g;g, g;g;g, ... などの無限個の射が生じます。自己ループ辺に限らずサイクルを持つグラフからは無限圏が生成されます。FQL++では、無限個の射を持つ圏が扱えません。パス同値関係を入れて“有限化”します。例えば、g;g = g という関係を入れると有限化されます。

category Bar = {

 objects A, B, C, X, Y;

 arrows

  u: A -> X,

  v: X -> B,

  g: B -> B;

 equations

  B.g.g = B.g;

}

有限個の射の全体は、Table表示やText表示で確認できます。次はText表示による射の列挙です。

arrows (11):
        A.u : A -> X
        A.u.v : A -> B
        A : A -> A
        B : B -> B
        C : C -> C
        B.g : B -> B
        X : X -> X
        Y : Y -> Y
        A.u.v.g : A -> B
        X.v : X -> B
        X.v.g : X -> B

関手の記述

次に関手を記述してみましょう。「圏と関手をできるだけ簡単に書き下す方法」の例は次のものでした。

category Foo {

 f: A -> B,

 g: B -> C,

 h: A -> C
 where f;g = h

}
category Bar {

 u: A -> X,

 v: X -> B,

 g: B -> B,
 C,

 Y

}
functor F: Foo -> Bar {

 C > B,

 f > u;v

}

この関手は、次の図で表すことができます。

僕が使っていた擬似構文における関手の記述ルールは：

1. 同じ名前の対象は、デフォルトで対応付ける。明示的に対応を記述すればオーバーライドされる。
2. 同じ名前の射は、デフォルトで対応付ける。明示的に対応を記述すればオーバーライドされる。
3. パス同値関係の保存から必然的に導かれる（推論できる）対応は書かなくてもよい。

FQL++では、記述の省略はしない方針なので、すべて明示的に書き下します。上記の例は、次のように翻訳できます。ただし、圏Barを有限化するために、B.g.g = B.g を加えています。

category Foo = {

 objects A, B, C;

 arrows

  f: A -> B,

  g: B -> C,

  h: A -> C;

 equations

  A.f.g = A.h;

}
category Bar = {

 objects A, B, C, X, Y;

 arrows

  u: A -> X,

  v: X -> B,

  g: B -> B;

 equations

  B.g.g = B.g;

}
functor F = {

 objects

  A -> A,

  B -> B,

  C -> B;

 arrows

  f -> A.u.v,

  g -> B.g,

  h -> A.u.v.g;

} : Foo -> Bar

この関手 F:Foo→Bar は次のようにFQL IDEで図示されます。

圏Barの対象C, Yがやたらに離れちゃってるなー。射の対応関係も図ではよく分からない。Text表示の列挙を見たほうがいいでしょう。

On objects:
        A -> A
        B -> B
        C -> B

On arrows:
        B.g -> B.g
        A -> A
        B -> B
        C -> B
        A.f -> A.u.v
        A.h -> A.u.v.g

FQL++と圏論

FQL++はFQLの後継言語でした。FQLがSQLデータベースとの親和性を考慮した言語仕様だったのに対して、FQL++は、純粋に圏論的な概念、すなわち圏、関手、自然変換を記述することを目的とした言語です。データベースに特化した機能がなくても、圏論的な記述能力があれば大丈夫だろう、という目論見だったのでしょう。

しかし、圏、関手、自然変換だけで全てを記述することは、現実的には無理があったようです。現時点では、FQL IDEの主力言語はOPLに移っています。それでも、圏論的な概念の記述を目的とした言語FQL++は、圏論の学習には好都合で、教育的意義は大いにあります。

今回は基本的な圏と関手の記述だけを紹介しましたが、FQL++は、圏的コンビネータによるプログラミングやモナドとクライスリ圏（双対的にコモナドと余クライスリ圏）などもサポートしています。関手データモデル／圏論データベースの分野に限らず、一般的な圏論のトピックも扱えるソフトウェアだと思いますよ。

*1:最新版はjarでしか提供されないようです。一方、インストーラーがあるバージョンは安定版と考えられるので、通常の利用ではインストーラーからのインストールでいいと思います。