中原市民館に来ております。データベースは圏なんだそうです。SGL読書会の姉妹イベントです。
Databases are categories by Spivakさん / @bonotakeさん
Spivakさんのスライドの解説です。
- 情報の世界の coherence の欠如を解決するためにフレームワークが必要
- 圏はデータベースのスキーマ。モデルは関手。
- 圏と計算機科学は近いもの
- 圏とは Ob、Arr、s(ource)、t(arget)、p(rimary = identity)
- 圏の例: Set、Hask、A monoid
- 関手の例: 恒等関手、潰す関手、Hask → Set、単純な例、Set→Cat
- M-Set : M → Set という関手。m : S → S をactionと呼ぶ
- 有限状態オートマトンはM-Set
- M→Arr(M) Yoneda embedding になっている
- 関手を圏にする : Grothendieck construction
- DBとは・・・テーブルと関連の集まり
- 行はレコード、タプル、インスタンス
- 列は属性。列は、純粋な値またはキー
- 主キー、外部キーがあり、外部キーは別のテーブルの主キーとなる
- 他にも、「労働者とマネージャは同じ部署」「その部署の秘書は同じ部署」のような制約が考えられる
- データ型(char(4)など)は1カラム(主キー)のみのテーブルと見なす
- データベースは、テーブルが対象で、カラムが射の圏C
- C→Sets という関手が、データ
- G:D→C スキーマのモーフィズム。G* : Sets^C → Sets^D という逆向きのpull back関手
- DとCの間でデータをうまく交換できる
- RDFって？ → メタデータ。セマンティックウェブ。ブログとかで使ってた。学術データでも？
- A monoidの圏もDBスキーマになってる！ → 実際のデータの例
- DBと圏は一緒 → 全然違うモノを結びつけられる → win-win
- 異なるDBを扱う数学的基盤が弱い → 圏論を使える
- Haskも圏なのでDB。DBはユーザ定義型の圏なので、Hask内で表現できる
- データベースとプログラムは統合できる
質疑応答
- プログラムとDBは一緒だって話だけど、どう使えるの？
- LINQ的なもの？
- 関数型データベースモデル。Mutableな値の集まりとしてDBを考える。
- カラムを関数として見なすと、列を自然に合成できるという視野が生まれる
- DBは関数を外延的に表すもの、Haskellはλ式で表す。同じなのは自然に思える
- 型は値が静的に決まる。テーブルは値が動的に変わる。違う。
- この例ではInstしか考えてないが、DBを表すのであればこの関手はどんどん変わるはず
- リアクティブプログラミング。スキーマを定義しておけば、データが変わっても勝手に辻褄をあわせてくれるというパラダイム
- DDLには副作用もあるのではないか
- 副作用はあってもいいのでは。時間的に変わるものなので
- 記述する時に手続き的ではなく宣言的に書きたい。少なくともinsertとかの副作用の影響は受けない
- 主キーと外部キーは本質的ではない。方便として出してるだけ
- 主キーは単にinjectionがあればいいはず
- 従業員に整数の主キーがあるのは福沢諭吉に反する*2
- monoとpull backがあれば主キー同士の関連も作れるだろうけど、要らないでしょ
- spanを使って削除、追加、更新を
- ⊥付きの集合で自然変換を考えた方が簡単な気がする
- もちろんPartial map でも同じ
- 厳密に言うとSetsじゃ駄目。spanの圏じゃないと自然変換として定義できない
- Spivakさんの興味の中心はデータのオペレーションじゃなく、スキーマの変更
- 重複を取り除いたりする操作はRelの圏でやったりする
- コピーしたりもしてるから、multi set なんじゃないかな
- SpivakさんはベースをSetsにすることに拘っている。クライスリ構成することは気にしない
- 教育的理由らしい。オブジェクトが集合じゃない抽象的なものだとなんだかわからない
- Spivakさんは蜘蛛の糸のタンパク質とクラッシック音楽の間に関手が存在するという論文を書いたらしい(笑
- それぞれをologで記述すると同様の関係があるという話 → ologの効力のデモっぽい位置付け
- どちらも一部の破損に強い構造らしい？
Databases are categories2 by Spivakさん / @bonotakeさん
引き続き2枚目のスライドの解説です。
- データマイグレーション
- F : C → D を使って Sets^CとSets^Dを行き来する関手を作れる
- Δδ := δ・F、ΣとΠは左と右の随伴
- Πは直積やjoin、Σは直和やunion、δは射影のイメージ
- 制約が入り過ぎると随伴がうまく存在しないかもしれない
- ベースとして型付けした圏が欲しい → Haskを利用
- F:B→Haskみたいなモノがあるとして、 InstをΔ_Fで引き戻してSet^Bで考えればよい
- 型を固定した Sets^C / ΠΔV がトポスになるのは自明。トポスになった方がwhere句は考えやすい
まとめ
- 実用化は？ → しようとしているけど進んでない(？)
- 圏ではなく
RelAllegoryを使ったものは作っているので、お楽しみに (by @pokarimさん)
