このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

［参照用 記事］

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

雑記／備忘

2013年の初頭に、デイヴィッド・スピヴァックの関手データモデル（functorial data model）について紹介しました。

あれから3年3ヶ月が経過して、今、関手データモデルや圏論データベース（categorical database）の状況はどうなっているでしょうか。

一言でいえば、

  • 派手に喧伝はされてないが、着実に発展している

となるでしょう。その進展の様子を次の3つの側面から概観してみます。

  1. ビジネス
  2. ソフトウェア
  3. 理論

内容：

  1. ビジネス： Categorical Informatics, Inc
  2. ソフトウェア： FQL IDE
  3. 理論： 等式論理と代数データベース

※ リンクと注釈がたくさんあるのは、この記事が、この話題に関する説明付きブックマークになるように、と意識したからです。

ビジネス： Categorical Informatics, Inc

関手データモデルに基づく製品やサービスを提供するIT企業としてCategorical Informatics, Inc が設立されています。

この企業が、急速な成長とイグジットを狙うスタートアップなのか、研究の合間にビジネス活動もボチボチやる程度のゆるーいチームなのか、ハッキリとは分かりません。いずれにしても、Categorical Informaticsが関手データモデル／圏論データベースのテクノロジーを扱う企業である事は間違いありません。

関手データモデルの創始者*1であるデイヴィッド・スピヴァック（David Spivak）はCategorical Informaticsのメンバーですが、彼のコミットメントの度合いはそれ程高くないように思います。スピヴァックはデータベース以外の研究もしてますし*2、学生の指導もしてます*3。ベンチャー起業家になる気はたぶんないでしょう。

Categorical Informaticsの中心人物となるのはライアン・ウィズネスキー（Ryan Wisnesky）*4です。

ウィズネスキーは、2012年頃*5からCategoricalData.netにおいてソフトウェアを開発していたようです。僕が2013年にCategoricalData.netを見た印象では、ソフトウェアも文書も断片的で何をやってるのか／やりたいのか？ 分かりませんでした。その後たまに覗いても、あまり進捗した様子もないので忘れてしまったのですが、開発はちゃんと継続されていたのですね。

CategoricalData.netで開発されていたFQL IDEは、ちゃんと動くものとなり、マニュアルもだいたい揃っています*6。これがCategorical Informaticsの主力製品（今はこれしかない）というわけです。Categorical Informaticsは、ソフトウェア以外に、企業のデータ統合（data integration）案件などに対する分析・コンサルティングもやるようです。

Categorical Informaticsのもう一人のメンバーであるジョシュア・タン（Joshua Tan）も研究者で、ウィズネスキーとスピヴァックの学生です。が、スタートアップの経験があるということで彼がビジネスサイドを担うとのこと。

スピヴァック、ウィズネスキー、タンの三人とも、とてもアカデミックな感じで、資金や人を集められるのかなー？ と余計な心配をしてしまいます。アカデミズム出身で辣腕を振るう起業家もいるので先入観はいけませんけどね。とりあえず大学（MIT）やNIST（National Institute for Standards and Technology）、NSF（National Science Foundation）からの支援はあるようです。スピヴァックのプロジェクト提案書が承認された、ってことでしょう。

ウィズネスキーはIBMと関係があり、スピヴァックはオラクルやマイクロソフトに顔を出したりしています。パワーのある企業が関手データモデルに興味を示せば劇的な展開もあるかも知れません。もっとも、そんな展開が望ましいかどうかはまた別問題ですけど。

ソフトウェア： FQL IDE

FQL IDEは、関手データモデルやオペラディクス（Operadics）理論などを実装するソフトウェアです。Javaで書かれています。名前にFQL（Functorial Query Language）が冠されていますが、実際には複数の言語（後述）を扱います。基本的にはコードエディタで、言語処理系に対するフロントエンド機能を兼ね備えたものです。

ちゃんと動きますが、プロトタイプの域を抜けてない感じで、実用に使えるソフトウェアになるにはまだ時間がかかりそうです。実用性を脇においても、個人的には不満が色々あります。が、今回は不満を言うのはヤメときます。

現在、FQL IDEは次の4つの言語をサポートしています。

  1. FQL（Functorial Query Language）
  2. FQL++
  3. FPQL（Functorial Programming and Query Language）
  4. OPL（Operadic Programming Language）

なんで4つも言語があるの？ たぶん、試行錯誤の結果がそのまま残ってしまった、という事情でしょう*7。構文と用途は少しずつ違う、言い換えると、4つとも似たような構文で用途も相当かぶっています。これ、あまりよろしくない状況（個人的不満じゃなくて、誰でも思うことだよね）。

いずれは単一言語に統合する予定なんでしょうが、現状では：

  1. FQL ： データベース言語としては一番分かりやすく使いやすい。
  2. FQL++ ： FQLの機能拡張・後継のはずだ（った）が、データベース言語としての使い勝手は落ちている。見捨てられたらしい。ただし、圏論の学習にはとても有用。
  3. FPQL ： FQLのプログラム機能を強化したものらしいが、マニュアルがないのでよく分からない。OPLに吸収されて開発は止まりそう。
  4. OPL ： 現状では、機能的に最上位の言語。プログラミング機能もデータベース機能も持っている。しかし、FQLに比べて記述が面倒になっているし、ビジュアライズもSQL生成機能もないので、OPLでFQLを置き換えられるとは言いがたい。

とりあえずFQLを使ってみることをおすすめします。SQLデータベースと関手データモデルに関する基本的な知識があれば使えます。スキーマ、スキーマ間の対応（マッピング）、データベースインスタンス（実際のデータのこと）、データベースインスタンス間の変換などを、比較的簡単な構文で定義できます。そして、スキーマの対応を使った問い合わせを実行できます。

要するに、データベースに関わる一通りの作業がFQLにより出来るのです。FQLコードに対応するSQLスクリプトも（可能ならば）生成してくれます。ある程度の規模の実例は、"Functorial Data Migration: From Theory to Practice"(9ページ) にレポートされています。

新しい言語OPLは、データベースに関わる概念以外に、型システムを導入し（まだ不十分）、汎用プログラミング言語との連携を意識しています。また、等式的推論機能を入れて、かすかに証明支援系の香りを醸し出しています。

型システムと等式的推論を入れた結果、CafeOBJなどのOBJファミリーやAlloyなどに近いものになっています。これは当然のことで、OBJファミリーのベースとなっているインスティチューションと、FQLのベースとなっている関手データモデルは、事実上同じものです。そのことは次の記事に書きました。

Alloyとの類似性に関して言えば、「Alloyを理屈っぽく考えてみようと思う」で次のように書いたことがあります。

関手データモデルとAlloyは、かなり親和性が高いんじゃないか、と感じるのです。
[...snip...]
また、関手データモデルを理解する道具としてAlloyが役に立つとも言えます。

これはつまり、AlloyのモデルとFQL／OPLのモデルは似てるってことです。今ではFQL／OPLが使えるので、関手データモデルにAlloyを使う理由はなくなった、とも言えますが。

形式的仕様記述言語、モデル発見器、証明支援系などを使った経験があれば、FQL／OPLはとっつきやすいと思います。また、OPLと一緒に使える汎用プログラミング言語はJavaScripなので、大変にポピュラーな言語と連携できるわけです（Java8にJavaScriptエンジンNashorn（ナスホーン）が付いているので、それを使ってJavaScriptコードを走らせています）。でも、JavaScriptとの連携方法がすげーカッコ悪い -- 将来の改善に期待。

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

理論： 等式論理と代数データベース

今の関手データモデルを初期（2010年から2012年くらい）のものと比べると、理論面でも長足の進歩を遂げています。圏論特有のアブストラクト・ナンセンスを突き詰めているようにも見えますが、ソフトウェア実装のための要求が相当な刺激・圧力になっているはずです。

当初の関手データモデルでは、テーブル（レコードの集合）とドメイン（値の集合）の区別をしていませんでした。テーブルのカラム（属性）、外部キーによる関連性、レコードの挿入・削除などは、集合圏モデルではすべて写像で表現されてしまうので、テーブルとドメインの区別は不要、あるいは暗黙に決まるという方針でした。また、データベースの制約は単純な等式（パス同値関係＝可換図式）だけしか書けない*8ので、論理式としての記述能力は貧弱でした。

このような状況だと、通常のプログラミング言語が持つキチンとした型システムや論理式による複雑な条件記述との接点がうまく見いだせません。Categorical Informaticsチームの最近（2015年, 2016年）の目標は「データベースと汎用プログラミング言語との統合」らしく*9、型システム（type system）と等式論理（equational logic）を関手データモデルと上手に接合する、という課題を解決しつつあります。その主要な成果は次の2つの論文に述べられています。

  • Title: An Equational Formalism and Design Pattern for Functorial Data Integration (v3: 28 Apr 2016)
  • Authors: Patrick Schultz, Ryan Wisnesky
  • URL: http://arxiv.org/abs/1503.03571
  • Pages: 40 pages
  • Title: Algebraic Databases (10 Feb 2016)
  • Authors: Patrick Schultz, David I. Spivak, Christina Vasilakopoulou, Ryan Wisnesky
  • URL: http://arxiv.org/abs/1602.03501
  • Pages: 80 pages

実装と運用に近い事項がEquational Formalismに述べられていて、その背景となる一般的・抽象的な枠組みのほうはAlgebraic Databasesで展開されています。

プロ関手（profunctor）、フレーム付き双圏（framed bicategory）、二重圏（double category）、カン拡張（Kan extension）などの道具が使われているので理解するのは骨が折れます。とは言え、これらの道具はデータベースやプログラミングと関係しそうだ、と感じていたものではあります。道具を使うのにためらいは不要です。「関手データモデル入門 4：ためらってしまう心を取り除く」より：

道具を使うにあたっての制限や障害はありません。ためらう必要はない、リミッターなしフルスロットルで使ってみればいいのです。

これらの道具立てに関連する過去記事を挙げておきます：

素朴でシンプルだった当初の理論と比べるとだいぶ難しくなってしまいましたが、本質が変わったわけではありません。より精密化されて柔軟な定式化になった、ということです。

FQL／OPLも、これらの理論を背景に設計・実装が進むのでしょう。どんなソフトウェアになっていくのか楽しみです。

*1:関手データモデルのアイデアは20世紀から存在はしていました。しかし、その面目を一新したのはスピヴァックなので、モダンな関手データモデルの創始者はスピヴァックである、と言っていいと思います。

*2:数学 http://arxiv.org/find/math/1/au:+Spivak_D/0/1/0/all/0/1 計算科学 http://arxiv.org/find/cs/1/au:+Spivak_D/0/1/0/all/0/1 応用 http://math.mit.edu/~dspivak/informatics/applied/ などの一覧を眺めれば、スピヴァックの興味の範囲が随分広いことが分かるでしょう。

*3:例えば、http://arxiv.org/abs/1506.03119 はスピヴァックの学生の論文。

*4:Wisneskyの発音を http://ja.forvo.com/ で探してもありませんでした。似た綴の"Wisniewski"が「ウィズネスキー」と書かれるので、このカタカナ表記を採用します。

*5:"Functorial Data Migration" http://arxiv.org/abs/1009.1166 のログを見ると、スピヴァックの関手データモデルに関する最初の投稿は2010年の9月です。しばらく間を置いてソフトウェア開発がスタートしたようです。

*6:チュートリアルはあるのですが、網羅的なリファレンスがないのが困りますね。説明が見つからないキーワードが幾つかあります。

*7:これら複数の言語を比べると、関手データモデルの実装に対する考え方・方針がどのように変遷したかをトレースすることができます。現時点でのマニュアルは、歴史的資料として意味がありそうです。(1)FQL http://categoricaldata.net/fql/tutorial.pdf (2)FQL++ http://categoricaldata.net/fql/tutorial2.pdf (3)OPL http://categoricaldata.net/fql/oplManual.pdf

*8:単純な制約の使い方は「関手的データモデル入門 2：統一的に制約を書く方法」にあります。

*9:2010年のスライドなどを見ると、2010年の時点で既に、スピヴァックはプログラミング言語の型システムとデータベースの統合を考えていた様子が伺えます。2015, 2016年は「そろそろ本気出そうぜ」の年といえるでしょう。