檜山正幸のキマイラ飼育記 このページをアンテナに追加 RSSフィード Twitter

キマイラ・サイトは http://www.chimaira.org/です。
トラックバック/コメントは日付を気にせずにどうぞ。
連絡は hiyama{at}chimaira{dot}org へ。
蒸し返し歓迎!
このブログの更新は、Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama
ところで、アーカイブってけっこう便利ですよ。

2018-01-17 (水)

TypeScriptのはなし : ユニオン型がけっこうイイね

| 11:47 | TypeScriptのはなし : ユニオン型がけっこうイイねを含むブックマーク

TypeScriptのはなし : サンプル記述に最良の言語」に続き、「ごめんねTypeScript」シリーズ第二弾。って、シリーズにするほどの話題があるか分からんけど、TypeScriptのいい点を紹介したり褒めたりする話です。

内容:

  1. TypeScriptのユニオン型はこんなに便利
  2. TypeScriptのユニオン型はこんなことも出来る: 有限集合型

TypeScriptのユニオン型はこんなに便利

型Xと型Yのユニオン型〈union type〉は、X | Y と書かれ、“ユニオン型 X | Y”の値としてXの値でもYの値でも許されます。縦棒'|'は、集合のユニオン(合併)演算子'∪'と解釈していいです。

まず、以前の記事(事実誤認あり)でも紹介した例をもう一度挙げます。

// ユーザーIDはユーザー名とユーザー番号の
// どちらもあり得る
type UserId = string | number;

// nullも許すstring型
type nullableString = string | null;

上記のnullableString型が意味を持つのは、stringにnullが入らないことが前提ですから、コンパイルオプションstrictNullChecksを付けてください(「TypeScript、僕が悪かった、ゴメン: nullやundefinedの扱いはマトモだった」参照)。

型パラメータも使えるので、nullableStringを次のようにも書けます。

// nullも許す型 一般
type nullable<X> = X | null;

// nullも許すstring型
type nullableString = nullable<string>;

ちょっと作為的だけど、こんなん(↓)も。

// なんかの限界値の設定に使う
// (リテラルは、その値だけを含むシングルトン型を表す)
type limit = number | "unlimited";

// 三値の真偽値
type TriValLogical = boolean | undefined;

次の例題として、ツリーのデータ構造(二進木にします)を考えてみましょう。ツリーのノードをオブジェクトで表すとして、次のようなコードを書くことが多いと思います。

// 注意! 単にNodeという名前にすると、DOMのNodeと
// 名前がかぶってしまう。
interface TreeNode {}

class Branch implements TreeNode {
  left: TreeNode;
  right: TreeNode;
  constructor(left: TreeNode, right: TreeNode) {
    this.left = left;
    this.right = right;
  }
}

class Leaf implements TreeNode {
  value: string;
  constructor(value: string) {
    this.value = value;
  }
}

var helloWorld : TreeNode = new Branch(new Leaf("Hello"), new Leaf("World"));
var greeting : TreeNode = new Branch(new Leaf("greeting"), helloWorld);

この書き方はいくつか鬱陶しいところがあります。

  1. 分岐ノード〈branch node〉と末端ノード〈leaf node〉を一律に扱うために、実質的意味がないインターフェイスTreeNodeを導入している。
  2. ノードが必ずTreeNode(を実装した)オブジェクトである必要があるため、末端ノードに生の文字列や数値を使えない。
  3. オブジェクト型に必ずnullが入ってしまう仕様だと(例えばJava)、空なツリーを認めるかどうかをプログラマがコントロール出来ない。

TypeScriptのユニオン型を使ってみます。

class Branch<T> {
  left: T | Branch<T>;
  right: T | Branch<T>;
  constructor(left: T | Branch<T>, right: T | Branch<T>) {
    this.left = left;
    this.right = right;
  }
}

type Tree<X> = void | X | Branch<X>;

var helloWorld : Tree<string> = new Branch<string>("Hello", "World");
var greeting : Tree<string> = new Branch<string>("greeting", helloWorld);

ユニオン型を使わないバージョンと比較してみると:

  1. インターフェイスTreeNodeのようなものは導入してない。分岐ノードも末端ノードも一様に扱うために、ユニオン型 T | Branch<T> を使う。
  2. 末端ノードは何でもよい。特定のインターフェイスを実装する必要もないし、オブジェクト型である必要さえない。
  3. 上記の例では、空なツリー(ノードをまったく持たないツリー)はvoidとして指定している。voidを入れなければ空なツリーは除外される。(voidを入れないほうが使いやすいと思いますが、例として入れてみました。)

また、ユニオン型使用バージョンでは最初から型パラメータを入れてますが、インターフェイス使用バージョンに型パラメータを入れること(ジェネリック化)は、ちょっと面倒でした。

interface TreeNode {
}

class Branch implements TreeNode {
  left: TreeNode;
  right: TreeNode;
  constructor(left: TreeNode, right: TreeNode) {
    this.left = left;
    this.right = right;
  }
}

class Leaf<T> implements TreeNode {
  value: T;
  constructor(value: T) {
    this.value = value;
  }
}

var helloWorld : TreeNode =
  new Branch(
    new Leaf<string>("Hello"),
    new Leaf<string>("World")
  );
var greeting : TreeNode =
  new Branch(new Leaf<string>("greeting"), helloWorld);

Leafにだけ型パラメータを入れました。これだと、var helloWorld : TreeNode<string>; のような型宣言(型注釈)が書けません。TreeNodeには型パラメータがないからです。TreeNodeに単純に型パラメータを追加するとコンパイルできず、結局次のようにしました。

interface TreeNode<T> {
  value?: T
}

class Branch<T> implements TreeNode<T> {
  value?: T;
  left: TreeNode<T>;
  right: TreeNode<T>;
  constructor(left: TreeNode<T>, right: TreeNode<T>) {
    this.left = left;
    this.right = right;
  }
}

class Leaf<T> implements TreeNode<T> {
  value: T;
  constructor(value: T) {
    this.value = value;
  }
}

var helloWorld : TreeNode<string> =
  new Branch<string>(
    new Leaf<string>("Hello"),
    new Leaf<string>("World")
  );
var greeting : TreeNode<string> =
  new Branch<string>(new Leaf<string>("greeting"), helloWorld);
  1. interface TreeNode<T> {} としたかったのですが、「型パラメータTを使ってない」と怒られます*1。しょうがないので、 value?: T を入れました。
  2. 分岐ノードTreeBranchに値を持たせる気はないので、 value?: T; は書きたくないのですが、「interface TreeNode<T> を満たしてない」と怒られます。
  3. value? という書き方は、「valueはあってもなくてもいい」という意味だから、実装クラス側で省略してもインターフェイスに違反してないと思うのだけど、「書け」とおっしゃる。でも、書いたら今度は、valueの存在を許すから、僕の意図(分岐ノードに値はない)と違う。

TypeScriptは、「ツリーのノード用にオブジェクトを定義することなんて面倒くさい」というモノグサ野郎(僕です)も面倒みてくれるでしょうか? 分岐ノードとして長さ2の配列を使って、配列要素で左右のサブツリーを表すことにします。

// ジェネリック版
// >>> コンパイルエラー
type SimpleTree<X> =  X | [SimpleTree<X>, SimpleTree<X>]

// 具体的な型(string)の版
// >>> コンパイルエラー
type SimpleStringTree = string | [SimpleStringTree, SimpleStringTree];

残念ながら、型パラメータがある無しに関わらず「循環参照はダメよ」と言ってコンパイルしてくれません。typeによる定義は、単に型の別名を定義する趣旨なので、ここはそんなに頑張んなくてもいいかも知れません。

しかし、このような循環的(再帰的)型定義が絶対に処理できないわけではありません。以前、Kuwataさんと、完璧じゃないけど実用上は問題ない程度の再帰的型定義は実装したことがあります。ココラヘンに名残があります。確か、完全に処理できるアルゴリズムもあったと思います。

TypeScriptのユニオン型はこんなことも出来る: 有限集合型

有限個の値からなる型は、通常は列挙型として定義します。

// 「はい・いいえ」の返答の値
enum YesNo {
  YES,
  NO
}

// 飲食店を、
// 星ナシから星五つのあいだで評価するときに使う
enum StarRating {
  Star0,
  Star1,
  Star2,
  Star3,
  Star4,
  Star5
}

TypeScriptの列挙型は、型ごとに名前空間を持つ*2ので、その値は YesNo.NO とか StarRating.Start3 とか書きます。StarRating.3 という値を定義したり書けたりすると便利だな、と思うのですが、それは出来ません。

TypeScriptはモノグサ野郎にやさしい仕様で、次のようにしても有限集合型を定義できます*3

type YesNo = "Yes" | "No";

type StarRating = 0 | 1 | 2 | 3 | 4 | 5;

列挙型のメリットのひとつは、switch文に余分なcaseが入ってないかコンパイラがチェックしてくれる点です。例えば、次の関数は case 6: のエラーが指摘されます。

function showRating(r : StarRating) : void {
  switch (r) {
  case 0:
    console.log("no rank"); break;
  case 1:
    console.log("one star rank"); break;
  case 2:
    console.log("two star rank"); break;
  case 3:
    console.log("three star rank"); break;
  case 4:
    console.log("four star rank"); break;
  case 5:
    console.log("five star rank"); break;
  case 6: // コンパイルエラー
    console.log("six star rank"); break;
  }
}

列挙型でもユニオンによる有限集合型でも、「漏れなく」はチェックしてくれないようです。漏れじゃなくて意図的な省略もあるのでエラーにはできないでしょう。でも、defaultがなくて、caseが抜けている場合って、たいていはプログラマのミスでしょうから警告して欲しいのですが。

[追記]「漏れ」のチェックは出来ます。次のようなdefaultを書きます。

  switch (r) {
  // 省略
  default:
    const _exhaustiveCheck: never = r;
  }

列挙した残りの値の集合が空集合だというセマンティクスだけど… ウーン、しかし、これは技巧的に過ぎるよな。手でこんなん書かなくても、コンパイルオプションかなんかで漏れを検出して欲しい。[/追記]

ユニオン型(バリアント型とも呼ぶ)が巷で積極的に推奨されない理由として、型による制約がユニオン型でゆるくなったり、制約逃れの手段にユニオン型が使われるリスクがあります*4。設計がまずいせいで、ユニオン型を多用せざるを得ない、なんてこともあります。

なので、ちょっと良いか悪いか分からんのですが、次のようなこともできます。

enum Judge {
  YES,
  NO
}

type YesNo = "Yes" | "No";

// 二値の返答が色々あるんだよなー
type Answer = boolean | Judge | YesNo;

function replyToAnswer(a : Answer) : void {
  // 色々ある値を分類して処理する
  switch(a) {
  case true:
  case Judge.YES:
  case "Yes":
    console.log("Thank you!");
    break;
  case false:
  case Judge.NO:
  case "No":
    console.log("It's a pity.");
    break;
  }
}

色々ゴチャゴチャあるのを何でもいいから混ぜちゃえ、と事後対策としてユニオン型を使うのは好ましくありませんが、事前にちゃんと考えてユニオン型を使うなら、便利で役に立ってくれます。

*1:ちょっと厳しすぎる感じなので、なんらかの手段で緩和できるのか?

*2:const enumは実行時の名前空間を持ちません。

*3:既存の型の部分集合型は、たとえ有限集合であっても扱いが面倒になるので、型システムの実装者には嫌われる傾向があります。既存型の有限集合型をサポートする判断は、実用性・利便性を重視してのことなのでしょう。こういう判断をするところも僕は好きです。

*4:悪用されなくても、そもそも型が複雑になるので嫌だ、ということもあるでしょう。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20180117

2018-01-16 (火)

離散集合ってなに?

| 10:23 | 離散集合ってなに?を含むブックマーク

N君に「で、離散集合ってなんですか?」と聞かれて、どう答えていいか困ってしまいました。

対話

N君 :「実数の全体は連続集合ですよね」
檜山:「そうだね」
N君 :「自然数の全体は離散集合ですよね」
檜山:「うん、そうだね」
N君 :「有限集合は離散集合ですよね」
檜山:「はい、そうだね」
N君 :「つまり、可算集合は離散集合ですよね」
檜山:「ん? いやっ、… あれ?」

連続と離散

「連続集合」はたまに使う言葉ですが、その意味はあんまりハッキリしません。R(実数の全体)の基数(濃度)を連続濃度と呼ぶので、Rと同じ基数を持つ集合を連続集合と呼んでいるのではないかと思います。この用法だと、「連続」とはいいながら、位相とは何の関係もなくて、単に集合を基数で分類・特徴づけしているだけです。

歴史や語源を僕は知りませんが、たぶん(たぶんです)、RRn、その部分集合などを連続体と呼んでいたことから、形容詞「連続」が「連続体と同等の」という意味で使われたのでしょう。

一方の「離散集合」ですが、これは集合の基数による分類・特徴づけとは関係ないように思えます。形容詞「離散」が「自然数(またはその部分集合)と同等の」という意味で使われている気がしないのです。もちろん、言葉の使用・運用は多様なので、「離散=可算」の用例が絶対ないとは断言できませんが。

離散集合は、集合の話ではなくて、位相の文脈で使われる言葉でしょう(多くの場合は)。つまり、離散集合は離散位相空間と同義だと思われます。

「連続」と「離散」は、対になる言葉としてよく一緒に使われますが、「連続集合←→離散集合」に関しては、対としての対称性はないようです。

離散空間としての離散集合

位相空間Xが離散であることの定義は簡単で、Xのすべての部分集合が開集合になることです。連続集合であるRを離散空間にすることもできます。位相空間Xの部分集合Aが離散集合であるとは、Xの位相から誘導されたAの位相(相対位相)により、Aが離散であることです。

上記のような定義を採用すると、「有限集合は離散集合である」もあやしくなります。集合{0, 1}の開集合族を{{}, {0, 1}}と決めると、({0, 1}, {{}, {0, 1}})は離散空間にはなりません。「有限集合を台とする位相空間は離散空間である」は正しくないのです。とはいえ、我々が有限集合に想定する位相は離散位相なのだとは思います。

自然数の全体は離散集合」も同様な事情で、我々がNに暗黙に想定する位相が離散位相なのでしょう。典型的には、Rに普通の位相(詳細略)を考えて、NR からの相対位相は離散位相です。

可算集合は離散集合」と言われれると「あれ?」となるのは、この言い回しは「可算集合の上に載る位相構造は離散である」と解釈できるからです。こうなると正しくない。Rの普通の位相と QR から誘導されるQの位相は離散位相ではありません。

言葉の国語辞書的な意味や語感・印象に基いて話していると、「あれ?」な状況(アレな状況)になったりしますね。

sasa2718sasa2718 2018/01/16 10:48 自然数は順序を持ち、それが誘導する位相が離散位相になります。だから自然数は離散だと言われても私には違和感はないのですが、これが普通かと言われると全く自信がありませんね

m-hiyamam-hiyama 2018/01/16 14:51 sasa2718さん、
> 自然数は離散だと言われても私には違和感はないのですが、
僕も全然違和感ないです。多くの人が「自然数は離散だ」は納得すると思います。
自然数には、何らかの構造が暗黙に仮定されるのでしょう。
それに対して可算集合は構造が抜けるので、「可算集合は離散だ」は変な感じがするのかと。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20180116

2018-01-15 (月)

TypeScriptのはなし : サンプル記述に最良の言語

| 11:28 | TypeScriptのはなし : サンプル記述に最良の言語を含むブックマーク

先週の金曜(2018-01-12)に、「TypeScript、お前もか: nullやundefinedの扱いがイイカゲン過ぎ」という記事(後にタイトルに「【事実誤認あり】」を追加)を書いたのですが、ほぼ言いがかりでした。謝罪と修正は「TypeScript、僕が悪かった、ゴメン: nullやundefinedの扱いはマトモだった」に書いてあります。

申し訳ないことをしたので、TypeScriptに関してポジティブな話を書きます。そもそも僕はTypeScript好きなんですよ。文句を付けた記事の書き出しは、

  • TypeScriptには期待してたんだけど、ガッカリだよ。

ですが、第二の文は、

  • それでもまー、割と好きだけど。

本文中にも、

  • nullやundefinedに関しても、整合的で安全なセマンティクスをかぶせているだろう、と。「期待していた」というより、思い込んでいた、信じていたのです。

と、信頼を寄せていた心情が伝わるでしょ。早とちりで「信じていたのに裏切られた」と誤解してカッとなったのですけど。

さて、TypeScriptはJavaScript+αなのですが、もとが極めてポピュラーなJavaScriptであって、+αの機能も持っていることから、現状において、サンプルコードを書くには最良の言語だと思います。

僕は、かなり昔から「サンプルコードはJavaScriptで書こう」と決めていました。2006年1月21日に書いた次の短い記事でそう表明しています。

当時の状況も書いてあったりして、懐かしい気分になります。

実を言えば、このあいだまでJavaScriptは「なんかトンデモない言語仕様の、ひどく貧弱な言語」-- みにくいアヒルの子と捉えていたのですが、りっぱな白鳥に、でも灰色の斑点が少し残った白鳥に成長しそうですね。

という見通しはだいたい当たったようです。

「サンプルをJavaScriptで書こう」と決めた第一の理由は、「誰でもどこでも使える」ことです。サンプルを試してみるのに、処理系のインストールやセットアップは不要です。ブラウザさえあればOK、最近のメジャーブラウザは[F12]でJavaScriptコンソールが使えます。そして、言語仕様も多くの人が知るところです。

JavaScriptは、無節操な(よく言えばマルチパラダイムな)言語なので、他の言語の書き方を真似しやすいのもいいですね。どんなスタイルのコードを書いても「JavaScriptはカクカクシカジカだから、その書き方はよくない」なんて話は(滅多に)出ません、もとが無節操だから。

ただ、型が書けないのはやはり辛い。例えば、

function isEmptyString(s) {
  return s.length == 0;
}

この例では、関数名が「引数は文字列だ」と強く暗示してますが、もっと素っ気なく、

function e(s) {
  return s.length == 0;
}

これだと、「引数は文字列だ」は伝わりにくいでしょう。ドキュメンテーションと型チェックを入れるなら、

function e(s/* string */) /* returns boolean */{
  if (typeof s != 'string' && !(s instanceof String)) {
    throw "Bad Arg";
  }
  return s.length == 0;
}

なんだか、みにくくなってしまいます。

TypeScriptなら、

function e(s : string) : boolean {
  return s.length == 0;
}

スッキリ書けます。

ただし、TypeScript言語処理系のインストールが必要なので、「誰でもどこでも使える」メリットは失われてしまいます。これはトレードオフなので致し方ないですけど。救いはインストールが比較的簡単なことです。node.jsとnpmのエコシステムはよく整備されていて、node.jsさえインストールしてしまえば、TypeScriptや関連ツール/ライブラリはnpm(最近ならyarnか)でインストールできます。

型がないと、説明とサンプルを書くことが困難なことがあります。2008年1月16日に書いた記事「CPS(継続渡し方式)変換をJavaScriptで説明してみるべ、ナーニ、たいしたことねーべよ」では、型パラメータが必要でした。この記事の第1節「未来のJavaScript」で、次のようなコードが書ける疑似言語を仮定しています。

function<X, Y>
makePair(first:X, second:Y):Array2<X, Y> {
  return [first, second];
}

架空の言語の代わりに、実在するTypeScriptを使って型パラメータを使った話題を書けるようになりました。

JavaScriptだけで済む話なら、「誰でもどこでも使える」JavaScriptが望ましいでしょう。ですが、型が必須の話題/サンプルはTypeScriptを使うのが現状では最善だと思います。

2018-01-12 (金)

TypeScript、お前もか: nullやundefinedの扱いがイイカゲン過ぎ【事実誤認あり】

| 09:35 | TypeScript、お前もか: nullやundefinedの扱いがイイカゲン過ぎ【事実誤認あり】を含むブックマーク

TypeScriptには期待してたんだけど、ガッカリだよ。

それでもまー、割と好きだけど。

*1

[追記]各所でご指摘いただきました(ありがとうございます)ように、コンパイル・オプション付きなら、シングルトン型のセマンティクスになります。この記事はほぼ言いがかりでした。事実誤認した経緯と、内容的修正を「TypeScript、僕が悪かった、ゴメン: nullやundefinedの扱いはマトモだった」に書きました。

この記事の本文自体はそのままにします。事実誤認も含めて記録が残ってもいいかな、と思うので。ただし、この記事だけを読む人が同じ誤認をしないように、何箇所かに修正記事へのリンクは入れます。[/追記]

内容:

  1. 特殊な型や値の扱い方はイイカゲンになりがち
  2. 特殊な型とは
  3. TypeScriptの基本型にnullは入らないと信じていた
  4. どんな伝統なんだよ
  5. TypeScriptにシングルトン型はないのか?
  6. ユニオン型は便利なんだけど
  7. never型はシッカリしている
  8. さいごに

関連:

特殊な型や値の扱い方はイイカゲンになりがち

プログラミング言語において、整数型やブール型のような普通の型の扱いがオカシイ例は知りません。しかし、null, none, nil, undefined, void, never, anyなどの言葉で呼ばれる型や値の扱いがイイカゲンで、トンチカンなことになっている例はあります。

例えば、R言語のNULLは、まともなセマンティクスを持たず、単に雰囲気で使われているため、実際にろくでもないことになります。

もっとずっと酷く、現実的に甚大な被害が生じているのは、データベースにおけるNULLでしょう。

「ヌルなんて、正常処理では使わないどうてもいい値だから」と考えるのはとんでもない間違いです。特殊な値・型も含めてちゃんと考えないと、型システムが破綻します。

特殊な型とは

ここで、特殊な型の基本をまとめておきます。

まず、シングルトン型(単元集合型)、これはその型に属する値がただ一つしかない型です。唯一の値がなんであれ、集合としてシングルトン(単元)ならシングルトン型と呼ぶことにします。例えば、C++で次のような列挙型が書けます。

enum OnlyOne {
  ONE
};

これで定義されるOnlyOne型は、値ONEしか持たないのでシングルトン型です。ONEの内部的な値は整数0ですが、次のコードはちゃんとエラーします(エラーするのが妥当な振る舞い)。g++のエラーメッセージは、"invalid conversion from 'int' to 'OnlyOne'"です。

enum OnlyOne {
  ONE
};

// コンパイルエラー
OnlyOne theValue() {
  return 0;
}

0をNULLに変えても当然ながらエラーです。

#include <stdlib.h>

enum OnlyOne {
  ONE
};

// コンパイルエラー
OnlyOne theValue() {
  return NULL;
}

NULLはlong long intとして定義されているらしく(これは環境/コンパイラ依存)、"invalid conversion from 'long long int' to 'OnlyOne'"というエラーメッセージになります。

次にユニット型。ユニット型とは、シングルトン型のなかで標準的な型を意味するとします。シングルトン型はいくらでも考えられますが、そんなかのどれかを特定したとき、それをユニット型と呼ぼう、ということです。関数型言語の場合、空タプル()だけを値とするシングルトン型をユニット型と呼ぶことが多いようです。

[補足]

集合圏Setにおいて、終対象はたくさんあります。シングルトンセット(単元集合)はなんであっても集対象です。しかし、どれかひとつのシングルトンセットを特定して、それを終対象と呼ぶのが普通です。つまり、「終対象はたくさんあるが、特定された終対象はひとつだけある」という状況になります。

任意の終対象に対応する型がシングルトン型、特定された終対象に対応する型がユニット型と考えると都合がいいでしょう。

[/補足]

それから空集合。値がひとつもない型が空集合です。空集合型を基本型に入れている型システムは少ないようですが、空集合型をサポートするときは、empty型とかnever型と呼ぶようです。

最後に何でもいいよ型。文字通りあらゆる値を許す型です。何でもいいよ型を認めると、型システムのチェックをバイパスできるので、好ましくないです。しかし、TypeScriptのように、もともと型チェックがなかった言語(JavaScript)に後付けで型システムを追加しているときは、互換性から何でもいいよ型が必要です。必要悪だけど。

TypeScriptの基本型にnullは入らないと信じていた

TypeScriptはJavaScriptの上位互換の言語になるように設計されています。また、処理系はJavaScriptへのトランスパイラとして実装されています。なので、JavaScriptのセマンティクスを大きく変えるような言語仕様は採用できません。

そうはいっても、新しく設計された言語ですから、JavaScriptの欠陥は矯正してくれてるだろう、と僕は期待してました。nullやundefinedに関しても、整合的で安全なセマンティクスをかぶせているだろう、と。「期待していた」というより、思い込んでいた、信じていたのです。ところが… [追記]裏切られた、というのは事実誤認です。[/追記]

前節のC++コードをTypeScriptに翻訳してみます。

enum OnlyOne {
  ONE
}

function theValue() : OnlyOne {
  return null;
}

これはエラー無しでコンパイル(トランスパイル)されてしまいます。[追記]これはコンパイルオプションなしの場合です。[/追記]

「えっ!?」と思って、今更ながらに小さなテストコードで試したみたら、TypeScriptの基本型(プリミティブ型)であるnumber, string, booleanはすべてnullを含んでいます。そればかりか、undefinedも含んでいます。

単一の値を持つ(はず)の列挙型OnlyOneは、実はシングルトン型になりません。3つの値を持ちます。

  1. OnlyOne.ONE
  2. null
  3. undefined

自動的に、nullとundefinedは追加されるのです。あらゆる型において、事前に、あるいは勝手にnullとundefinedが入るのです。もう、なんだよソレー。

TypeScriptはJavaScriptコードを受け入れるので、次のコードはコンパイルできます*2

function repeatString(s, n) {
  var r = "";
  for (var i = 0; i < n; i++) {
    r = r + s;
  }
  return r;
}

コンパイルできることは、もちろんいいです(互換性大事)。安全性・頑健性を増すために、引数、戻り値、変数などに型宣言(型注釈)を追加しましょう。

function repeatString(s:string, n:number) :string {
  var r:string = "";
  for (var i = 0; i < n; i++) {
    r = r + s;
  }
  return r;
}

これで、変な引数は弾いてくれと思うじゃないですか。しかし、次の関数は、コンパイルも実行も可能です。

function doRepeatString() {
  return repeatString(null, undefined);
}

JavaScriptの奇妙で強烈な型変換機能により、実行は失敗しません。nullの文字列への変換は"null"で、undefinedの数値への変換はNaNなので、上記の呼び出しは repeatString("null", NaN) と解釈されます。0 < NaN という比較もできるので、何ら問題ないわけです。

だけど、だけど、だけど、JavaScriptのワケわからんトンデモ・セマンティクスに持ち込んで解釈するのかよー!? TypeScriptの上位層では、まともなセマンティクスを保って欲しかった。基本型(プリミティブ型)や列挙型にnullとundefinedを突っ込んで何が嬉しいんだよ? 誰得?

どんな伝統なんだよ

Javaではどうなってるか、試してみます。

class Test {
  enum OnlyOne {
    ONE
  }
  OnlyOne theValue() {
    return null;
  }
}

これはコンパイル成功です。Javaの列挙型もnullを勝手に含めるようです。OnlyOneはシングルトンになりません。列挙型の実装にオブジェクトを使っているからでしょう。

Javaの基本型(プリミティブ型)にnullが…、いくらなんでも、まさか…

class Test {
  int intValue() {
    return null;
  }
}

エラーしてくれました。ホッ。String型になると、これはオブジェクトの型(参照型)なので、nullを許します。

それにしても、「オブジェクトの型には自動的にnullを含める」という習慣はどっから来たんでしょうか? 僕は由来を知りません。

単なる想像を言うと; 昔のC言語の文字列は、文字値(アスキー文字なら8ビット整数値)が並んだ配列へのポインターでした。ポインターだからNULLもあるわけです。構造体へのポインターとかでも同じくNULLがあります。仕掛け上、複雑なデータ型はポインターで指すことになるので、必然的にNULLも入ってしまう、と。「仕掛け上、そうなってしまった」を無思慮にずっと踏襲してしまった、ということじゃなかろか。

nullが自動的に入って嬉しいことなんてないけど、ひとつだけ思い当たるのは、Maybeモナドみたいなことかな。例外を使わずに、正常値と異常値ひとつを一緒にしたデータ型を使いたい、と。しかしね、これは明示的にやればいいことでしょ。例えば、Standard MLのdatatypeを使うなら:

datatype 'a nullable = Null | Just of 'a

null(上の定義ではNull*3)も許すstringが欲しいなら、string nullableという型を使います。

良き伝統、守るべき伝統というのもあるけど、たいしたメリットもなく、問題を引き起こすろくでもないnullの伝統を守るってのはどういう了見なんだか。

古き悪しきNULLポインターの系譜といえば、Javaより直系と思えるC++ですが、次のコードで、FooValue()とFooRefValue()はコンパイルエラーになります。FooPtrValue()がエラーにならないのは、ポインターのセマンティクスだからしょうがないでしょう。意図的にポインターを使わなければNULLが許されない点では、悪しき伝統を断ち切っているように思えます。

struct Foo {
  int foo;
};

// コンパイルエラー
Foo FooValue() {
  return NULL;
}

// コンパイルエラー
Foo& FooRefValue() {
  return NULL;
}

// コンパイル成功
Foo* FooPtrValue() {
  return NULL;
}

TypeScriptにシングルトン型はないのか?

TypeScriptでは、null型、undefined型、void型に関して、明白な定義とセマンティクスを見い出せなかったんじゃないのかな。null型にundefined値が含まれ、undefined型にnull値が含まれ、void型にはnull値とundefined値が含まれます。結局、値の集合としてはどれも {null, undefined} です。念のために言うと、null === undefined の値はfalseなので、{null, undefined} がシングルトンセットに潰れることはありません。二元集合です。[追記]これはコンパイルオプションなしの場合です。[/追記]

null値とundefined値の役割上の違いというと、配列の範囲外インデックスによるアクセスとか、初期化してない変数の値は、nullではなくてundefinedです。しかし、こういう目的で“値”を使う必要があるのか? と疑問も感じます。例えば、初期化してない変数を参照したとき:

  1. 初期化してない変数にアクセスしたらundefined値が正常に得られる
  2. 初期化してない変数にアクセスしたら未定義例外が発生する。

プログラマのミスを発見しやすい、という観点からは二番目のほうが望ましいでしょう。とはいえ、ランタイムがJavaScriptであるTypeScriptでは、実行時例外には介入できないし、コンパイル時の範囲外インデックス/未定義変数参照の検出も難しいので、致し方ないですね。ゴメンね。

null値とundefined値の用例をみるに、例外が起きてもよさそうな場面でundefinedが使われている雰囲気はあります。実際には例外が起きずにundefined値が返るので、正常な値にundefined値が混じるのは避けられない、したがって、すべての型にundefinedが入る -- まー、ここまでは納得できなくもないのですが、undefined型にnull値を許すのが解せない。

もし、undefined型の値の集合 = {undefined} なら、undefined型はシングルトン型であり、特定されたシングルトン型、つまりユニット型として使えたはずです。実際には、undefined型も二元集合なので、どうやってもシングルトン型を作れそうにありません。[追記]これはコンパイルオプションなしの場合です。[/追記]

そもそもシングルトン型は必要なのか? と言われると、絶対必須ではないかも知れません。しかし、ある型がシングルトンだという保証があると、型を簡略化できることがあります。例えば、ストリング型とシングルトン型のタプル(ペア、長さ2の配列)の型があると、これは安心して単なるストリング型にしてしまって大丈夫です。しかし、ストリング型とundefined型(値はnullとundefined)のタプルでは、[x, null]と[x, undefined]に意味的差があるかも知れないので同一視できません。

ユニオン型は便利なんだけど

僕がTypeScriptで気に入っていた点に、ユニオン型が簡単に書けることがあります。例えば次のようです。

// ユーザーIDはユーザー名とユーザー番号の
// どちらもあり得る
type UserId = string | number;

enum YesNo {
  YES,
  NO
}

// 返答はYesNo型かブール型
type Answer = YesNo | boolean;

既に書いたように、僕は、TypeScriptの基本型にnullは入らないと誤解していたいので、次のような型定義(型シノニム)を書いていました。

// nullも許すstring型
type nullableString = string | null;

このようにすると、HaskellStandard MLの代数的データ型(の簡略な場合)が、データ構築子なしで書けて便利だと思っていたのです。

誤解のもとになったもうひとつの先入観があります。かつて、Kuwataさんと僕で作っていたCaty型システムで、直和型(ディスジョイントユニオン型)を実装していました。構文が上記TypeScriptとまったく同じで、排他性(値集合の共通部分がないこと)のチェックをして、直和型のセマンティクスに基いて型計算/型チェックをしていたのです。

この経験から、(ディスジョイントな)ユニオン型は便利だし実装可能だから、TypeScriptもやったんだな、と勝手に納得していたのです。しかし、集合として null⊆string なので、string | null に意味はなく、TypeScriptが排他性チェックをしてないことが分かります。となると、型計算/型チェックのセマンティクスも信用できるか怪しくなります。[追記]これはコンパイルオプションなしの場合です。[/追記]

never型はシッカリしている

「型システムがちゃんとしているな」と感心する言語のひとつにStandard MLがあります。Standard MLは、“型システムいのち”みたいなところがあるので、ちゃんとしていて当然です。

そんなStandard MLでも「あれ?」という点があります。

exception Ouch

fun ouch () = raise Ouch

Ouchという例外を定義して、常にOuch例外を起こす関数ouchを定義しました。ouchの型を見ると、val ouch = fn: unit -> 'a となります。これは、ouch関数(正確には関数オブジェクト)が引数なしで、任意の型を取ることを意味します。

ouchが値を返すことは絶対にありません。「値を返さないから戻り値型は未定だ」という理屈です。おそらくこれは、論理における「矛盾が起きたら何でも証明できる」に触発されたのでしょう。しかし、オカシイです。

常に例外を起こす(投げる)関数の戻り値型は空集合型です。これは例外モナドによる例外機構を考えれば明らかです。次の記事など(古い順)を参照してください。

TypeScriptにはnever型があり、これはホントに空集合型になっています。neverには、nullもundefinedも入れません。次のコードはちゃんとエラーになります。

function neverNull() : never {
  return null;
}

function neverUndefined() : never {
  return undefined;
}

never型は、常に例外を起こす関数の戻り値型に使います。

function ouch() : never {
  throw "Ouch";
}

never型の定義と使用法では、Standard MLよりTypeScriptのほうがまっとうです。えらいぞ、TypeScript。

重箱の隅をつつく話をしますが、never型を引数型とする関数はあるでしょうか? ほぼ役に立ちませんが、実はあります。任意の型(集合)Xに対して、neverからXへの関数がただ一つあります。neverの意味が空集合だとすれば、そうなります。

さいごに

シングルトン型や空集合型なんて、どうでもよさそうですが、実は大事です。特殊な型ですが、特殊なだけに型システムの要〈かなめ〉のような役割を果たしています。ちゃんと設計して実装しないと、型システムの整合性を壊してしまいます。にも関わらず、イイカゲンな設計・実装が現存しています。

壊れた型システムがまったく使いものにならないわけではありません。ワークアラウンドとして、壊れた部分を避けるような使い方でしのげます。しかし、やはり望ましくはないです。TypeScriptの場合、完全に新規な言語ではなく、色々としがらみを抱えているので、理想論も言ってられないわけですが、基本型にnullとundefinedを入れるのはやめて欲しかったなー、と。[追記]コンパイルオプションを付ければ、ちゃんとチェックします。[/追記]

TypeScript、僕が悪かった、ゴメン: nullやundefinedの扱いはマトモだった

| 18:43 | TypeScript、僕が悪かった、ゴメン: nullやundefinedの扱いはマトモだったを含むブックマーク

ごめんなさい。↑の記事、僕がうかつな事を書きました。TypeScriptのコンパイラにオプションを付ければ、nullとundefinedに関してキチンとチェックします。

きびしいチェックをするオプション付きなら、null型もundefined型もシングルトン型になります。

デフォルトでの値の集合 きびしくチェックしたときの値の集合
null {null, undefined} {null}
undefined {null, undefined} {undefined}
void {null, undefined} {undefined}

事の発端と顛末

TypeScriptの列挙型の挙動を知りたくて、enum OnlyOne {ONE} のサンプルを書いて試したら、nullが入っていて驚いた、というのが事の発端です。

このとき、単なるディレクトリ(フォルダ)に enum-test.ts を置いて、tsc enum-test.ts とやってみた、という状況。その後も、同じ“素のディレクトリ”で試していたので、コンパイラ(トランスパイラ)の挙動はオプションなしのデフォルトだったんです。

冷静に考えてみると、例えばstringにnullが入り込むならもう少し早い時点でその事実に気づいていてもよさそう。実は、以前は“素のディレクトリ”ではなくて“プロジェクト・ディレクトリ”で作業していたのでした。

プロジェクト・ディレクトリには、次のようなtsconfig.jsonが置いてありました。(存在を意識してなかったけど。)

{
  "compilerOptions": {
    "strictNullChecks": true,
    "noUnusedLocals" : true,
    "noImplicitThis": true,
    "alwaysStrict": true,
    "outDir": "./dist/",
    "sourceMap": true,
    "noImplicitAny": true,
    "lib": ["dom", "ES2017"],
    "module": "ES2015",
    "target": "ES5",
  }
}

コンパイラ・オプションはきびしいチェックになっていたので、僕の期待通りに動いていたのですよね。それゆえに、不審な事態に遭遇しなかったわけです。

実は、環境が変わったので態度が変わっただけなのを誤解して、「君って、そういうコだったんだ」「信じていたのに、今まで騙されていたんだな、俺は!」と短絡的に反応してしまいました。

すべてチェックします

下のサンプルは、コンパイラ・オプションなしだとノーエラーでコンパイルされ、きびしいオプションを付けると全部コンパイルエラーになる例です。


// void型の要素は何か?
// >>> コンパイルエラー

function NullInVoid() : void {
  return null;
}

// null型の要素は何か?
// >>> コンパイルエラー

function UndefInNull() : null {
  return undefined;
}

// undefined型の要素は何か?
// >>> コンパイルエラー

function NullInUndef() : undefined {
  return null;
}

// nullが基本型(プリミティブ型)に入るか?
// >>> コンパイルエラー

function NullInNumber() : number {
  return null;
}

function NullInBoolean() : boolean {
  return null;
}

function NullInString() : string {
  return null;
}

// undefinedが基本型(プリミティブ型)に入るか?
// >>> コンパイルエラー

function UndefInNumber() : number {
  return undefined;
}

function UndefInBoolean() : boolean {
  return undefined;
}

function UndefInString() : string {
  return undefined;
}

// 値がひつとの列挙型
enum OnlyOne {
  ONE
}

// nullがOnlyOneに入るか?
// >>> コンパイルエラー
function NullInOnlyOne() : OnlyOne {
  return null;
}

// undefinedがOnlyOneに入るか?
// >>> コンパイルエラー
function UndefInOnlyOne() : OnlyOne {
  return undefined;
}

// 文字列の繰り返し連結
function repeatString(s:string, n:number) :string {
  var r:string = "";
  for (var i = 0; i < n; i++) {
    r = r + s;
  }
  return r;
}

// 不適切な呼び出しの例
// >>> コンパイルエラー
function doRepeatString() {
  return repeatString(null, undefined);
}

*1:ロゴ画像 http://www.windward.net/blogs/a-whole-bunch-of-typescript-tips/attachment/typescript-logo/ より

*2:トランスパイラは何もしないで出力に書き出すだけです。

*3:小文字のnullも使えますが、リストが空かどうかを判定する関数がnullという名前で、この関数を隠してしまうのでマズイです。

通りすがり通りすがり 2018/01/12 13:59 コンパイルの際に--strictNullChecksを付けたらどうでしょう?

Nfm4yxnW8Nfm4yxnW8 2018/01/12 18:52 シングルトン型ってString Literal Types,Numeric Literal Typesじゃダメなんですか?(strictオプションはonで)

https://www.typescriptlang.org/docs/handbook/advanced-types.html#enum-member-types

m-hiyamam-hiyama 2018/01/12 18:54 通りすがりさん、Nfm4yxnW8さん、ありがとうございます。
ごめんなさい、修正記事書きました。今日の2番めの記事です。

2018-01-10 (水)

米田埋め込み、米田拡張、そして米田モナド

| 11:58 | 米田埋め込み、米田拡張、そして米田モナドを含むブックマーク

どうやら、米田埋め込みを単位とするモナドがありそうです。ちゃんと構成するのはけっこう大変。このモナドを定義するためのアウトラインを示します。

内容:

  1. 伝説としての米田モナド
  2. 前層構成子の上のモナド: 楽観的な導入
  3. サイズの問題とフレイド/ストリートの定理
  4. 相対モナド
  5. 相対モナドとしての米田モナド
  6. 左カン拡張の存在
  7. 残るは

伝説としての米田モナド

Cを圏として、米田埋め込み〈Yoneda embedding〉yCは、Cから“Cの前層の圏”PSh(C)への関手 yC:C→PSh(C) です。この米田埋め込みyを単位とするモナドがあるらしいという話は、キュリア(Pierre-Louis Curien)の論文で知りました。次に示す論文の第7節"Profunctors as a Kleisli category"にそのことが書いてあります。

しかし、サイズの問題があり正面からモナドを構成するのは難しいため、モナドの代わりにクライスリ構造〈Kleisli structure〉というもの*1を定義しています。

米田埋め込みを単位とするモナド米田モナド〈Yoneda monad〉と呼ぶことにします。米田モナドの存在を感じ取った人はキュリアだけではないはずです。ずっと昔、おそらくは圏論の草創期から、相当多くの人々が気づいていたであろう、という意味で「圏論フォークロアのひとつ」と言っていいでしょう。

次節で、米田モナドについて素朴に説明します。その説明どおりには事が進みません。問題を回避して、なんとか米田モナドを定義するプランをその後の節で示します。

前層構成子の上のモナド: 楽観的な導入

Cを圏とします。関手 Φ:CopSet を、C上の前層〈presheaf〉と呼びます。前層は、単に集合圏Setへの(反変)関手に過ぎません。「前層」という呼び名は歴史的な産物(遺物?)です。

関手圏[Cop, Set]を、C前層の圏〈category of presheavess〉と呼び、PSh(C)と書きます。

  • PSh(C) = [Cop, Set]
  • |PSh(C)| = |[Cop, Set]| = Functor(Cop, Set) = (C上の前層=Set値反変関手の全体)
  • PSh(C)(Φ, Ψ) = [Cop, Set](Φ, Ψ) = NatTransform(Φ, Ψ:CopSet) = (関手Φから関手Ψへの自然変換の全体)

PSh(C)は、自然変換の縦結合を結合とする圏です。したがって、CにPSh(C)を対応させる写像(大きいかも知れない写像)は、|Cat|→|Cat| を定義します(ホントか?)。PShは、「前層の圏」の構成法により圏から圏を作り出す操作なので、前層構成子〈presheaf constructor〉と呼ぶことにします。

今のところ、PShは関手ではありません。関手 F:CD に対するPSh(F)は定義されてないからです。PShを拡張する反変関手なら比較的簡単に作れます。実は、反変関手じゃダメなんですが、練習問題としてやってみましょう(オマケ扱い)。

F:CD を関手とするとき、Fopによる前層Γの引き戻し F(Γ) = Fop*Γ ('*'は図式順の関手の結合記号)は、PSh(D)→PSh(C) を定義します。Psh(F) = F : PSh(D)→PSh(C) と置くと、前層構成子PShの拡張であるPShが反変関手になることを確認できます。

いま、PShは反変関手だと言いましたが、どこからどこへの関手でしょうか? Cを小さい圏に限定すれば、小さい圏の圏Cat上でPShが定義されます。PShの行き先はCatでしょうか -- そうはなりません、先ほど |Cat|→|Cat| だとウソ言いました。Cが小さくても、関手圏[Cop, Set]が小さいとは限りません。つうか、小さくないです。

必ずしも小さくない圏も許す圏の圏をCATとします。PShCAT上なら自己反変関手になるでしょう(なるのか?)。PShは引き戻しを利用するので反変関手でしたが、PSh(Γ)を、前層Γの前送り(押し出し)で定義すれば、共変の自己関手PShもたぶん定義できるでしょう(できるのか?)。米田埋め込みは、yC:C→PSh(C) の形なので、自然変換 y::IdCAT⇒PSh:CATCAT とみなせそうです(ホント?)。

CAT上の自己関手PShと自然変換 y::Id⇒PSh は既にあります(って、あるのか?)。あと、自然変換 μ::PSh*PSh⇒PSh がうまいこと見つかれば、CAT上のモナド (PSh, y, μ) ができます。これが米田モナド(のはず?)です。

サイズの問題とフレイド/ストリートの定理

前節では、随分と楽観的でいいかげんな議論をしました。圏の圏CAT上のモナドとして、ホントに米田モナドが存在するのでしょうか? モナド乗法μの構成はなんだかよく分かりません。その前に、共変の前層関手PShはwell-definedでしょうか。そもそもCATなんて使って大丈夫なの??

Iを単一の対象と恒等射だけを持つ自明な圏とします。I∈|CAT| はいいですよね。前層構成子PShが|CAT|上に働いているとすれば、PSh(I) = [Iop, Set] ¥stackrel{¥sim}{=} Set ですから、Set∈|CAT| です。もう一度PShを作用させると、PSh(Set) = [Setop, Set] ができます。[Setop, Set]はとてつもなく大きな圏で、ホムセット[Setop, Set](F, G)も小さな集合とは限りません。

ホムセットも巨大になると、普通には扱いようがないので、ホムセットは小さい(局所小〈locally small〉)は要求したいところです。あらためて、CATは、“ホムセットは小さい圏(局所小圏)”の圏だとします。それでも Set∈|CAT| は成立します。PSh(Set)はもはやCATに収まらないので、PShをCAT上の自己関手に拡張することは出来ません。

PSh:|CAT|→|CAT| という前提は諦めざるを得ません。となると、モナドの構成も出来なくなるのですが、モナドの問題はいったん棚上げして、今は前層構成子PShの定義を確立することに集中します。

Cがなんらかの圏だとして、どんなときにPSh(C)は局所小な圏になるでしょうか? この問題に対して、フレイド/ストリート(Peter Freyd, Ross Street)の定理が答えてくれます

フレイド/ストリートによれば、次の2つの命題は同値です。

  • Cが小さい圏と圏同値である。
  • Cが局所小で、前層の圏PSh(C)も局所小である。

小さい圏と圏同値となる圏を本質的に小さい〈essentially small〉といいます。この言葉を使うと、フレイド/ストリートの(サイズに関する)定理は次の主張です。

  • Cは本質的に小さい ⇔ 圏Cは局所小、かつPSh(C)は局所小

これはかなりありがたい定理です。圏の圏Catの定義として、“本質的に小さい圏の圏”を採用しても、|Cat|上のPSh(C)は局所小にとどまります。

例えば、有限集合の圏FinSetを考えます。FinSetは小さい圏でしょうか? この世にあるすべての有限集合の集まりって集合なの? たぶん違うでしょう。しかし、圏Fを次のように定義してみます; |F| = N、ホムセットを F(n, m) := Set({1, 2, ..., n}, {1, 2, ..., m}) として定義。Fは対象が可算個、すべてのホムセットは有限集合という小規模な圏です。FinSetFと圏同値なので、本質的に小さい圏です。したがって、PSh(FinSet)も局所小な圏になります。

有限次元ベクトル空間の圏FdVectKも、同様な議論で本質的に小さいことが示せるので、PSh(FdVectK)も局所小な扱いやすい圏です。

というわけで、Catを“本質的に小さい圏の圏”としても話はうまくいきそうです。が、今日のところは無難に、Catは“小さい圏の圏”としておきます。圏同値な圏を“同じ”とみなすなら、小さい圏でも本質的に小さい圏と“同じ”で、一般性はそこなわれません*2。次がいえます。

  • Cが小さいなら、 前層の圏PSh(C)は局所小である。

これによって、PSh:|Cat|→|CAT| の存在が保証されます。

相対モナド

PSh:|Cat|→|CAT| なのは確実になりました。しかし、|Cat| ≠ |CAT| なので、PShの繰り返し適用が出来ません。通常のモナドの定義ではPShが自己共変関手になる状況を前提しているので、このままではうまくいきません。アルテンキルヒ達(Thorsten Altenkirch, James Chapman, Tarmo Uustalu)による相対モナドにより対処できます。彼らの論文タイトルは、ズバリ「自己関手じゃなくてもモナド作れるよ」です。

モナドの定義には、モノイド・スタイルと拡張スタイルがあります(「モナドの定義とか」参照)。モノイド・スタイルは関手上に載った代数系として定義するので代数スタイルと呼んだこともあります。拡張スタイルは、クライスリ拡張オペレータを中心とするもので、プログラミングで使うには便利な定義です。

相対モナドの定義は、まずは拡張スタイルで与えられます。キュリアが使っていたクライスリ構造は、相対モナドとほぼ同じものです。関手 J:CD の上に相対モナドを定義するのです。J上の相対モナド〈relative monad〉は次のもので構成されます。(T(X), J(X)をTX, JXなどと括弧無しで書いています。)

  1. 写像 T:|C|→|D|
  2. X∈|C| に対して、ηX:JX→TX in D
  3. X, Y∈C と k:JX→TY in D に対して k#:TX→TY in D

η = {ηX | X∈|C|} を単位〈unit〉、kに対するk#クライスリ拡張〈Kleisli extension〉と呼びます。

上記の素材 T, η, (-)# が相対モナドであるためには、次の法則を満たす必要があります。

  1. X, Y∈|C|, k:JX→TY in D に対して、ηX;k# = k
  2. X∈|C| に対して、(ηX)# = idTX
  3. X, Y, Z∈|C|, k:JX→TY, ℓ:JY→TZ に対して、(k;ℓ#)# = k#;ℓ#

Jがところどころ挿入されている以外は、普通のモナドの定義と同じです。この定義からはじめて、クライスリ圏やアイレンベルグ/ムーア圏を構成できます。また、相対モナドもモノイド(類似構造)として代数的にも定義できます。詳細はアルテンキルヒ達の論文を見てください。

相対モナドとしての米田モナド

米田モナドを相対モナドとして定義しましょう。前節の定義に出てきた素材が、米田モナドでは何に相当するかまとめてみます。

相対モナドの定義 米田モナド
C Cat
D CAT
関手 J:CD 包含関手 CatCAT
写像 T:|C|→|D| 前層構成子 PSh:|Cat|→|CAT|
単位射 ηX:JX→TX in D 米田埋め込み yC:C→PSh(C) in CAT
クライスリ拡張 k#:TX→TY 米田拡張 K#:PSh(C)→PSh(D)

クライスリ拡張とは、モナドの理論のなかで使われる用語です。それに対して米田拡張〈Yoneda extension〉は圏の一般論での用語です。米田拡張についてはnLabに記事があります。

米田モナドにおけるクライスリ拡張が米田拡張になっています。また、米田拡張は、米田埋め込みとカン拡張により構成されます。関手Jは包含関手なので自明です。前層構成子PShと米田埋め込みyは定義済みです。となると、米田モナドの定義問題は、米田拡張(-)#の構成と分析に集約されます。

上の表で列挙した米田モナドの素材が、実際に相対モナドになるためには、先に挙げた法則を満たす必要があります。しかし、法則が等式で成立することは期待できず、up-to-iso(isoは自然変換で与えられる)での法則になります。

  1. C, D∈|Cat|, K:C→PSh(D) in CAT に対して、yC*K# ¥stackrel{¥sim}{=} K
  2. C∈|Cat| に対して、(yC)# ¥stackrel{¥sim}{=} IdPSh(C)
  3. C, D, E∈|Cat|, K:C→PSh(D), L:D→PSh(E) に対して、(K*L#)# ¥stackrel{¥sim}{=} K#*L#

左カン拡張の存在

カン拡張〈Kan extension〉に関しては、nLabの項目がけっこう詳しい解説になっています。

nLab項目と同じ記号を使うとします。p:CC' という特定の関手があったとして、F:CDC'D まで拡張しましょう、という話です。G:C'D が p*G = F ('*'は図式順の関手結合)を満たすなら「pに沿ったFの拡張」と言えますが、拡張のなかで普遍的なもの(最良な近似)がカン拡張です。カン拡張には左カン拡張〈left Kan extension〉と右カン拡張〈right Kan extension〉があります。

米田拡張では、pとして 米田埋め込み yC:C→PSh(C) を取ります。F:CD の、yCに沿った左カン拡張が米田拡張でした。左カン拡張がいつでも存在するわけではありません。したがって、米田拡張も存在するとは限りません。

nLab項目のなかで、左カン拡張が存在する条件について述べられています。nLab項目のProposition 2.8によると、次の条件が満たされるなら F:CD の左カン拡張が存在します。

  1. Cが小さい圏である。
  2. Dは余完備〈cocomplete〉である。

Cが小さいことは前提にしていました。Dが勝手な圏とするなら、余完備性は保証できません。しかし、米田モナドにおいては、F:C→PSh(D') で、D'も小さい圏の場合しか考えません。Dは勝手な圏ではなくて、D = PSh(D') の形に書けるということです。

小さい圏D'をあらためてDと置き直して、F:C→PSh(D) とします。小さい圏Dに対してPSh(D)が余完備かどうかが問題になります。

前層の圏の性質として次があります。

The category of presheaves PSh(C) is the free cocompletion of C.


前層の圏PSh(C)は、Cの自由余完備化である。

前層の圏がもとの圏の余完備化になっているので、PSh(D)は余完備です。

Cが小さい圏で、PSh(D)は余完備なので、F:C→PSh(D) のyCの沿った左カン拡張は存在します。それをF#と置きます。F |→ F# という対応は厳密〈strict〉な一意対応ではありませんが、up-to-isoで一意とは言えます。

残るは

Cat、圏CAT、前層構成子 PSh:CatCAT、F:C→PSh(D)に対する米田拡張 F#:PSh(C)→PSh(D) の存在は、なんとかなりました。後は、先に挙げた3つの等式(up-to-isoなので同型式と言うべきか)です。

が、僕はカン拡張の計算がろくに出来ないので、3つの等式がよく分かりません、ザンネン。ちゃんと計算している資料も見つからない(あまり熱心に探してないけど)。しかし、状況証拠は揃っているし、キュリアも米田モナドを仮定した議論をしているので、“幻のモナド”ってことはないでしょう。

困った時の米田頼み、ご利益ツールズ」で述べたように、米田埋め込みだけでも強力な道具になっているので、米田モナド(正確に言うと相対疑モナドかな)の全体を使うともっと強い事を言える可能性があります。

*1:M. Fiore, N. Gambino, M. Hyland, G. Winskel によるアイディア

*2:でも、本質的に小さい圏をそのまま扱うほうがいいとは思います。圏同値で同一視するのは荒っぽすぎて、何かを見失うような心配があります。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20180110

2018-01-09 (火)

まともな型クラス への入門: 関数型とオブジェクト指向の垣根を越えて

| 08:48 | まともな型クラス への入門: 関数型とオブジェクト指向の垣根を越えてを含むブックマーク

2016年9月に次の記事を書きました。

タイトルからして引き続く記事を予告しているのですが、その予告を実行することができませんでした。タイトル中の「何か」とは「型クラス」のことです。上記の記事の最後の部分は:

関数型プログラミングにもオブジェクト指向にも関係があって、今後重要度を増すであろう「型クラス」ですが、今述べた(愚痴った)ような事情で(あと、C++のコンセプトは宙ぶらりんだし)、説明の方針も題材も定まりません。でも、いつか、何か書く、かも。

今回この記事で、予備知識をあまり仮定しないで型クラスの説明をします。言いたいことの1/3くらいは書きました。1/3でも長い記事なので、ぼちぼちと読んでもらえれば、と。書き残したことは最後に触れます。いつか、1年はたたないうちに(苦笑)、続きを書くつもりです。

内容:

  1. Haskellの型クラスは無視しよう
  2. CoqとStandard ML、それとこの記事での型クラスの書き方
  3. 壮絶な車輪の再発明と混乱を極める用語法
  4. 指標(型クラス)とはこんなもの
  5. 指標(型クラス)のインスタンスとはこんなもの
  6. 無名の指標、無名のインスタンス
  7. ユニット型と引数なし関数と定数値
  8. インスタンスとデータインスタンス
  9. 状態遷移と隠蔽型、メイヤー先生登場
  10. よりオブジェクト指向
  11. 関数と関数オブジェクト
  12. 言い残したことなど

Haskellの型クラスは無視しよう

型クラスを知りたい人は、Haskellの型クラスから勉強をはじめようとするかも知れません。それはやめましょう

型クラスという言語機能を導入し華々しく応用した最初のプログラミング言語は、確かにHaskellです。しかし、今となってみれば、Haskellの型クラスは失敗作です。Haskellの型クラスが分かりにくいのは、分かりにくいようになっている、つまり設計が歪〈ゆが〉んでいるからです。

失敗であることを認識しなかったり、欠陥品になんか深い意味があると勘ぐったりするのは健全な態度ではありません。失敗の状況や原因を分析するか、あるいは、興味がないなら単に無視しましょう。この記事では、Haskellの型クラスは無視します。失敗の状況や原因に興味があるなら、次の記事を参照してください。

  1. 入門的ではない型クラスの話:Haskellの型クラスがぁ (´^`;)
  2. オーバーロードは何故にかくも難しいのか:Haskellの成功と失敗
  3. Haskellの型クラスに関わるワークアラウンド
  4. JavaScriptで説明するオーバーロード解決

Haskellの型クラスのダメな所は、“オーバーロード(名前・記号の多義性)機構”と“構造の記述”という2つの別々なことを、一緒に実現してしまった点です。当初は、「一粒で二度おいしい」と嬉しかったのですが、時間がたてば問題点が現れてきます*1

この記事のタイトルにある「まともな型クラス」とは、オーバーロード機構は除外して、構造の記述だけを目的とした記法と概念のことです。オーバーロードは、構造の記述とは切り離して別に考えるべきなのです(この記事ではオーバーロードは扱いません)。この記事が「まともな『入門記事』」かどうか怪しいけど、「僕が思う『まともな型クラス』を解説する記事」です。

CoqとStandard ML、それとこの記事での型クラスの書き方

型クラスが何であるかの説明をまだしてませんが、とりあえず目を慣らす意味で、CoqとStandard MLの型クラスの書き方を眺めておきましょう、眺めるだけでいいです。Coqでは実際に「型クラス〈type class〉」と呼んでますが、Standard MLでは「指標〈signature〉」という呼び名です。

Class Collects := {
  e: Type;
  ce: Type;
  empty : ce;
  insert : e -> ce -> ce;
  member : e -> ce -> bool
}.
signature Collects = sig
  type e
  type ce
  val empty : ce
  val insert : e -> ce -> ce
  val member : e -> ce -> bool
end

よく似てますが、書き方は微妙に違います。その違いを列挙します。

Coq Standard ML
型クラスのキーワードClass signature
束縛を作る記号 := =
ブロック構造 { と } sig と end
宣言の区切り記号 セミコロン 空白・改行
型の宣言 名前 : Type type 名前
値の宣言 名前 : 型 val 名前 : 型
型クラス定義の終端記号 ピリオド なし

けっこう事細かに指摘しましたが、違いが重要なのではありません。重要なことは、

  • そんな違いなんてどうもいい!

ということです。

プログラミング言語は、それぞれに違った構文を持つので、その違いにどうしても目が行きがちですが、概念を理解するときは、構文的な違いに拘るのは得策ではありません。「どうでもいい」と考えることがとても重要です。

さて、この記事では、CoqでもStandard MLでもなく、その中間くらいの記法を採用します。

signature Collects := {
  type e;
  type ce;
  value empty : ce;
  value insert : e -* ce -* ce;
  value member : e -* ce -* bool
}

これは、概念としての型クラスを説明するための擬似言語です。Coq、Standard ML、擬似言語の構文を比較すると:

Coq Standard ML この記事では
型クラスのキーワードClass signature signature
束縛を作る記号 := = :=
ブロック構造 { と } sig と end { と }
宣言の区切り記号 セミコロン 空白か改行 セミコロン
型の宣言 名前 : Type type 名前 type 名前
値の宣言 名前 : 型 val 名前 : 型 value 名前 : 型
関数型構成子の記号 -> -> -*
型クラス定義の終端記号 ピリオド なし なし

一番違和感があるのは、矢印'->'の代わりの'-*'でしょう。これについては最後のほうで説明します。宣言を区切る記号はセミコロン';'ですが、空な宣言を認めるとして、次のように余分なセミコロンを書いてもいいとしましょう*2

signature Collects := {
  ;
  type e;
  type ce;
  ;
  value empty : ce;
  value insert : e -* ce -* ce;
  value member : e -* ce -* bool;
}

壮絶な車輪の再発明と混乱を極める用語法

オーバーロード機構を切り離した「構造を記述する記法と概念」としての型クラスは、多くのプログラミング言語の言語機能やプログラミング技法(デザインパターン)として既に実現されています。要するに、大して珍しいものではないのです。

しかし、それぞれの言語の文化圏において特有な形で型クラスが実現されているので、ほぼ同一の概念・機能がまったく別物のように見えてしまいます。型クラス関連のキーワードを、Standard MLHaskellJavaから拾って並べてみましょう。

Standard ML Haskell Java
型クラス signature class interface
型クラスのインスタンスstructure instance class
型クラスのあいだの変換 functor 特になし*3 Adaptorパターン

横に並んだ概念達(1行目なら signature, class, interface)は、まったく同じとは言いませんが、とても似ています。その類似性と多少の違いをこの記事でハッキリさせます。

車輪の再発明:「広く受け入れられ確立されている技術や解決法を知らずに(または意図的に無視して)、同様のものを再び一から作ること」

*4

オブジェクト指向でのクラス〈class〉を、Haskellではインスタンス〈instance〉、Standard MLではストラクチャ〈structure | 構造体〉と呼ぶあたりは、なかなかにややこしくて混乱を招く可能性が高いです。この記事内では、「型クラス」よりむしろ「指標」を使うのは、少しは混乱が減るかと思ってです。

「型」「クラス」「インスタンス」などと言う言葉は、何か特定のモノ・概念を指すのではなくて、ある文脈において、モノ・概念の役割を表す言葉に過ぎません。文脈が変われば異なる解釈になります。特定プログラミング言語でのキーワードや記号、特定コミュニティ内での用語法(所詮は隠語です)には拘らない、ここでもう一度叫びましょう。

  • そんな違いなんてどうもいい!

しかしそれでも、この記事内でどんな言葉を使うかは決めないといけないので、次のようにします。

Standard ML Haskell この記事では
型クラス signature class signature
型クラスのインスタンスstructure instance instance
型クラスのあいだの変換 functor 特になし transformer

指標(型クラスのこと)のあいだの変換をStandard MLではfunctor〈関手〉と呼んでいます。この変換はとても重要です。圏論用語functorをそのまま使うのはどうかな? と思うのでtransformer〈トランスフォーマー〉とします。が、今回トランスフォーマーまで説明できません。いつか続きの記事で……

[補足]

Standard MLで"functor"という言葉を使うのは、割と合理的な根拠があります。実際に、圏論的な関手を誘導するからです。しかし、この状況を説明するとき「functorはfunctorを誘導する」では意味不明なので、プログラミング言語機能の名前はfunctor以外にしておいたほうが無難だと思います。

ちなみに、Prologでは、関数呼び出しの形をした構造体の名前部分をfunctor〈関数子〉と呼んでます。C++では、関数オブジェクトをfunctorと呼ぶようです。言葉の選び方/使い方とはこういうもんです。いちいち文句を言っていたらきりがない、しょうがない。

[/補足]

指標(型クラス)とはこんなもの

この記事でtypeと書いた場合、それは単に集合の意味です。type X と書いたら、「名前'X'は集合を表すつもり」という意味です -- それ以上余計なことは考えないように。

次の指標定義を見てましょう。

// とある2つの型
signature TwoTypes := {
  type X;
  type Y
}

これは、「集合を表す2つの名前'X', 'Y'がある」という意味しかありません。そのような2つの名前をまとめてTwoTypesと名付けているので、指標定義全体の意味は:

  • 集合を表す2つの名前'X', 'Y'をまとめて、それをTwoTypesと呼ぼう。

もうひとつ指標定義をみてみましょう。

// とある1つの関数
signature OneFunction := {
  type X;
  type Y;
  function f: X -> Y
}

この指標定義は、次の意味です。

  1. 集合を表す名前'X'がある。
  2. 集合を表す名前'Y'がある。
  3. 関数を表す名前'f'がある。
  4. 'f'が表す関数の引数の型(値の集合)は'X'で、戻り値の型(値の集合)は'Y'だとする。
  5. 'X', 'Y', 'f'をまとめてOneFunctionと呼ぼう。

指標とは、名前の集合と、それらの名前達が何を表すかの約束のことです。名前が表すものは二種類しかありません。〈type〉か関数〈function〉です。二種類ですよ、二種類。もう一度言います。

  • 指標内の名前が表すものは型〈type〉か関数〈function〉のどちらか。

指標定義に現れるキーワードは、typeとfunction、そしてsignatureです。基本はこの3つだけです。その他の記法はすべて、便利な略記法(構文マクロ)として導入されます。

指標(型クラス)のインスタンスとはこんなもの

指標は名前に関する約束に過ぎません。名前の実体はまったく決まってません。そこで、名前に実体を割り当てたものを考えて、それを当該指標のインスタンスと呼びます。

signature OneFunction := {
  type X;
  type Y;
  function f: X -> Y
}

// 1つの関数の具体例:二乗する関数
instance SquareFunction of OneFunction := {
  X := int;
  Y := int;
  f := (x:X):Y => x*x
}

指標のインスタンスでは、指標で宣言されたすべての名前に実体を与えます。指標で宣される名前は型か関数を表すので、実際の型と実際の関数を名前に割り当てることになります。

上記インスタンス定義で、intは整数型を表します。intは単なる名前ではなくて、実体としての集合(整数値の集合)を表しています。intの他に、real(実数型)、bool(ブール型)、unit(ユニット型、後述)などは組み込みの型だとします。よく知られた算術演算や論理演算も、システム組み込みで最初から入っているとします。組み込みの型と関数は、いつでもどこでも使えるとします。

インスタンスにおける関数(ユーザー定義関数)の実体は、アロー関数記法で書きました。最近のJavaScriptではアロー関数記法が使えます。さらにTypeScriptでは型宣言*5も付けられます。簡潔で、Standard MLにも近い記法なので、これを使うことにします。アロー関数記法、おススメだよ。

Standard MLならば、上記の擬似コードをそのまま書けます(若干の構文の違いは翻訳して)。

signature OneFunction = sig
  type X
  type Y
  val f: X -> Y
end

structure SquareFunction : OneFunction = struct
  type X = int
  type Y = int
  val f = fn x => x*x
end

TypeScriptで書いてみましょう。“そのまま”ってわけにはいかないです。

interface OneFunction<X, Y> {
    // type X;
    // type Y;
    f(x:X) : Y;
}

class SquareFunction implements OneFunction<number, number> {
    // type X = number;
    // type Y = number;
    f = (x:number):number => x*x;
}
  1. インターフェイス内で型の名前だけを宣言できないので、型パラメータに変更。
  2. int型はないので、number型に変更。
  3. 意味的には、fは静的関数(static)だが、staticを付けるとエラーになるのでインスタンス関数としている。

指標のインスタンスは、TypeScriptのクラス〈class〉より、ネームスペース〈namespace〉(旧内部モジュール)に近いと思います。

namespace SquareFunction {
  type X = number;
  type Y = number;
  let f = (x:X):Y => x*x;
}

しかし、ネームスペースをインターフェイスに対してチェックすることはできません。

[補足]

ネームスペース内の名前に関する約束をインターフェイスでは書けませんが、TypeScriptの型定義構文によってある程度は書けます。

declare namespace SquareFunction {
  function f(x:number):number; // 関数fの引数型と戻り値型の宣言
}

でも型定義構文では、指標としての表現力が足りません。

[/補足]

無名の指標、無名のインスタンス

最近のプログラミング言語では無名の関数(so-called ラムタ式 or クロージャ)をサポートすることが多いですよね。関数名なんて要らないことがあるからです。signature TwoTypes := {type X; type Y} という書き方は、指標に'TwoTypes'という名前を付けています。しかし、いつでも名前が必要なわけではありません。無名の指標を次の形で書くことにします。

signature {type X; type Y}

先の名付け構文は、上記の無名指標と名前'TwoTypes'を':='を使って束縛(結びつけ)していますから、次でも同じです。

TwoTypes := signature {type X; type Y}

名前TwoTypesが指標の名前であることを最初に明示したいなら、

signature TwoTypes := signature {type X; type Y}

signatureが2つも要らないから、右辺側を落とせば:

signature TwoTypes := {type X; type Y}

あっ、最初に戻りました。結局のところ、書き方は次のどれでもいいのです。

TwoTypes := signature {type X; type Y}
signature TwoTypes := signature {type X; type Y}
signature TwoTypes := {type X; type Y}
  • そんな違いなんてどうもいい!

無名のインスタンスも instance of TwoTypes {X := int; Y := int} のように書きましょう。TwoTypesは指標の名前なので、名前の代わりに指標そのものをインラインで書いてしまえば:

instance of signature {type X; type Y} {
  X := int;
  Y := int
}

インスタンスに名前を付ける構文は、次のどれでもいいとします。

IntInt := instance of TwoTypes {X := int; Y := int}
instance IntInt := instance of TwoTypes {X := int; Y := int}
instance of TwoTypes IntInt := {X := int; Y := int}
instance IntInt of TwoTypes := {X := int; Y := int}
  • そんな違いなんてどうもいい!

しつこく繰り返しますが、書き方や呼び名の違いで、同一(またはほとんど同一)の概念を別物だと思いこんでしまうのは不幸なので、「どうもいい」のオマジナイで表面上の違いを吹き飛ばしましょう。

ユニット型と引数なし関数と定数値

C言語のような古い言語でもvoid型という型があります。「voidは値がないことを示す」というのはウソです。そうじゃなくて、voidはただ一つの値を持つ型です。その値が何であるかを知る必要がないだけです。(void型に関する詳しい分析は「void型とunit型とoneway呼び出し」を参照。)

関数型言語では、void型をユニット型と呼ぶことが多いです。そして、ユニット型のただ一つの値は空タプル()だとする習慣です。void型/ユニット型の唯一の値は「これだ」と決めれば何でもいいのです。値が何であるかはどうでもよくて(また「どうでもいい」だ)、値が決めてないのが困るのです。JavaScriptだと、特殊な値としてnullとundefinedがあるので、void型の値をどっちにするか悩むところです。TypeScriptの実装を見ると、voidの値はnullとundefinedの両方を許しているようです。唯一に決めてねーじゃん、それダメだよ*6

さて、我々の擬似言語ではユニット型をunitと書くことにします。指標内に関数のプロファイル(引数の型と戻り値の型)を書くとき、f:unit -> X を f: -> X と書いていいことにします。「引数の型が書いてなかったらunit型とする」という約束です。

次の指標を考えましょう。

// oneという名前の関数
signature One := {
  function one : -> int
}

指標Oneのインスタンス*7を無名インスタンスとして挙げます。

instance of One {
 one := () => 1
}

oneは引数なしの関数なので、普通は one() のように呼び出します。プログラミング言語によっては one だけで呼び出せるかも知れません。引数なしの関数呼び出しと定数記号はどう違うのでしょうか? その答は、

  • そんな違いなんてどうもいい!

です。引数なしの関数は定数と同じとみなしてもいいので、function one : -> int を、value one : int と略記することにします。指標Oneとそのインスタンスは次のように書き換えられます。

// oneという名前の値
signature One := {
  value one : int
}

instance of One {
 one := 1
}

valueは単なる略記で、functionの特別なケースであることに注意してください。

引数なしの関数と定数の違いはどうでもいいのですが、それでもウジウジと詮索したい場合は次の記事を参照してください。


インスタンスとデータインスタンス

指標とは、名前に関する約束でした。名前の種類は、“型の名前”と“関数の名前”だけです*8。関数の特殊な形を値〈value〉と呼ぶのでした(前節)。

となると、次も立派な指標です。(realは実数型とする。)

// 2次元の点
signature Point2D := {
  value x : real;
  value y : real
}

指標のインスタンスとは、指標に出現する名前に実体を割り当てるので、例えば次がインスタンスです。

instance of Point2D {x := 4.7; y := -1.0}

これって、単にデータ型とデータインスタンス(オブジェクトデータ)です。普通はデータインスタンスをこんなに丁寧に書かないで、Point2D {x := 4.7; y := -1.0} で済ませるでしょう。JSON風の構文なら Point2D {x : 4.7, y : -1.0} かな。裸のタプル (4.7, -1.0) で代用することさえできます。でも、書き方なんでどうでもいいです。指標(型クラス)とそのインスタンスの概念は、通常のデータ型(構造体型)とデータインスタンスの概念も含むのです。

次の例は、指標の内部に型名も含まれるものです。インスタンスでは、型の具体化(型名への実際の型の割り当て)も値の具体化も行います。

// 座標値がとある型である2次元の点
signature Point2D := {
  type T;
  value x : T;
  value y : T
}

instance of Point2D {T := int; x := 5; y := -1}

状態遷移と隠蔽型、メイヤー先生登場

副作用を伴う関数は純関数ではない、と言われます。まー、定義上そうなのでしょう(純関数=副作用がない関数)。しかし、副作用が状態を変化させることだとすれば、その状態遷移を純関数で表せないこともありません。次の例をみてみましょう。(boolはブール型とする。)

// ONとOFFの2状態を持つトグルスイッチ
signature ToggleSwitch := {
  type State;
  function isOn : State -> bool;
  function isOff : State -> bool;
  function toggle : State -> State
}

状態遷移を引き起こす関数toggleは、Stateの値を引数に受け取って、新しいStateの値を返すとします。毎回新しいState値を作るのか、それとも既存の値を上書きするのか、とかはメモリ管理や最適化の問題なので、ここでは「どうでもいい」とします。([追記]この節の最後に補足があります。[/追記]

状態遷移を関数で表せたのですが、やはり状態は特別扱いしたい気持ちもあるので、hiddenという修飾子を導入しましょう。状態を表す型の前にhiddenを付けます。(なんでhidden(隠れた)かは、すぐ後でわかります。)

signature ToggleSwitch := {
  // Stateは状態の型
  hidden type State;
  function isOn : State -> bool;
  function isOff : State -> bool;
  function toggle : State -> State
}

これだけでは何も嬉しいことがありません。次の約束を導入します。

  1. hiddenな型を“第1引数に持つ関数”の第1引数を省略してよい。ただし、functionの代わりにqueryと書く。
  2. hiddenな型を“第1引数と戻り値に持つ関数”の第1引数を省略し、戻り値型はunit(voidと同じ)にしてよい。ただし、functionの代わりにcommandと書く。

この約束にしたがって指標を書き換えると:

signature ToggleSwitch := {
  hidden type State;
  query isOn : -> bool;
  query isOff : -> bool;
  command toggle : -> unit
}

おおおー、こっ、これは…。そうです、メイヤー先生ご推奨のCommand-Query分離されたインターフェイスです。

さらに次の約束をします。

  • signatureの前にhiddenを付けると、自動的に決まった名前('This'とする)のhidden typeが宣言される。

hidden typeは省略され、表面に現れることはない(ゆえにhidden=隠れている)ので、明示的に宣言する必要はありません。上記の約束のもと、自動宣言に任せます。この形の指標を隠蔽指標〈hidden signature〉と呼びます。

hidden signature ToggleSwitch := {
  // hidden type の宣言は不要
  query isOn : -> bool;
  query isOff : -> bool;
  command toggle : -> unit
}

隠蔽指標ToggleSwitchの無名インスタンを書いてみましょう。Unitはunit型の唯一の値だとします。

instance of ToggleSwitch {
  This := bool;
  isOn := (this:This) => this == true;
  isOff := (this:This) => this == false;
  // タプルの第一成分が新しい状態、第二成分はコマンドの戻り値(常にUnit)
  toggle := (this:This) => ((this ? false : true), Unit)
}

これはもはや、オブジェクト指向のインターフェイスとクラスなので、TypeScriptで書けます。

interface ToggleSwitch {
    isOn() : boolean;
    isOff() : boolean;
    toggle() : void;
}

class ToggleSwitchImpl implements ToggleSwitch {
  private _ : boolean;
  constructor() {this._ = false;}

  isOn = () => this._ == true;
  isOff = () => this._ == false;
  toggle = () => {this._ = (this._ ? false : true); undefined}
}

微妙な構文的・意味的な調整が入ってますが、だいたい hidden signature → interface、instance of → class implements と置き換えただけです。

[追記 補足]

状態を、関数の引数と戻り値として受け渡すのは効率が心配で夜も眠れない人がいるかも知れません。

理想的な状況は、我々人間はホントに「状態か値かを気にしないで済む」ようになることです。大きなデータのコピー/新規作成はコストですが、賢いコンパイラが、共有/上書きして大丈夫かを判断して、コピー/新規作成を抑制してくれたら嬉しい。

しかし現実には、そこまで賢いコンパイラを作るのは難しいです。値(データ実体)そのものではなくて、値の場所を示す参照〈reference〉(安全性を増したポインター)を導入して、状態は参照型を使って受け渡す方法があります。データの操作も参照経由で上書きします。これなら効率の問題は解消されます。代償として、意図せぬデータ破壊のリスクは生じます。

ひとつのプロセスが、自分専用のデータを上書き更新し続けるような状況は、末尾再帰で処理できます。末尾再帰の最適化で、スタックフレームを新設せずに再利用します。スタックフレームまたはスタックフレームから参照される自分専用データなら、上書きしても他人に迷惑がかかりません。Erlangのサーバーは、そんな形で実装されます。

[/追記 補足]

よりオブジェクト指向

XとYが型(の名前)だとして、その直積型〈direct product type | ペア型 | タプル型〉を X*Y で表します。HaskellStandard MLも'*'で直積型を表しています。数学の記法では X×Y です。

2引数(2変数)の関数のプロファイルは、f:X, Y -> Z のように書き、1つのペアを引数にする関数のプロファイルは f: X*Y -> Z と書くことにします。「2引数の関数」と「1つのペアを引数にする関数」はどう違うでしょう? 多くの場合は「そんな違いなんてどうもいい!」のですが、カリー化が絡むと注意が必要です。注意は後で述べます。今は、「2引数の関数」と「1つのペアを引数にする関数」は同じだと思ってください。

XとYが型(の名前)だとして、その直和型〈direct sum type | disjoint union type〉は X | Y とします。X | Y は、XまたはYの意味で、XとYに共通する(両方に入る)値はないとします。'*'と'|'は、型から型を作り出す演算子なんで、型構成子〈type constructor〉と呼ぶことがあります。

前節で、Command-Query分離されたインターフェイスとその実装(インスタンス)を示しました。Command-Query分離するのは望ましい習慣ですが、そうもいかないときもあります。Commandとは限らないメソッドの表現法を示しましょう。

スタックの例を使います。popが、状態遷移と同時に値も返すとします。errorはエラーを表す特別な値を含む集合(型)とします。

signature Stack := {
  hidden type State;
  type Elem;
  function top : State -> Elem | error;
  function push : State * Elem  -> State;
  function pop : State  -> State * (Elem | error);
}

function top は query top に、function push は command push にできますが、popはqueryにもcommandにもなりません。引数側と戻り値側に出てくる隠蔽型(この場合はState)を消して、functionをmethodに変えます。次のように書けます。

signature Stack := {
  hidden type State;
  type Elem;
  query top : -> Elem | error;
  command push : Elem  -> unit;
  method pop : -> Elem | error;
}

commandをmethodと書いてもかまいません。hiddenをsignatureの前に移して、Stateを隠蔽しましょう。次のようになります。

hidden signature Stack := {
  type Elem;
  query top : -> Elem | error;
  method push : Elem  -> unit;
  method pop : -> Elem | error;
}

型Elemを型パラメータに置き換えれば、この隠蔽指標はTypeScriptインターフェイスで次のように書けます。

type error = null;

interface Stack<Elem> {
  top() : Elem | error;
  push(e : Elem) : void;
  pop() : Elem | error;
}

別な例として、先ほど例に出したPoint2Dを隠蔽指標に直して、メソッドを追加してみます。query x : -> real を field x : real と書く略記も使うことにします。「フィールド」か「プロパティ」か「データメンバ」か? んなことはどうでもいいでしょうが。

hidden signature Point2D := {
  // x座標とy座標
  field x : real;
  field y : real:
  // 引数で指定された移動量(ベクトル)だけ移動する
  method moveBy : real, real -> unit
}

これは、さまざまな略記が使われているので、略記無しで書けば次のようです。This * unit は事実上Thisと同じであることに注意してください。

signature Point2D := {
  hidden type This;
  function x : This -> real;
  function y : This -> real:
  function moveBy : This, real, real -> This * unit
}

hiddenという修飾子は導入しましたが、最初に言ったとおり、指標で使うキーワードはtype, function, signatureの3つだけです。シンプルな概念に基づき、便利な略記を導入するくらいで、関数型からオブジェクト指向までカバーできます。守備範囲を広げるコツは、どうでもいい違いに惑わされないことです。

ここで、今までに導入した略記規則をまとめておきましょう。(注意:2引数と1タプル引数は区別しない、This * unit は This と同じ。)

略記 略記を展開すると
function 名前 : -> 型 function 名前 : unit -> 型
value 名前 : 型 function 名前 : unit -> 型
query 名前 : -> 型 function 名前 : This -> 型
command 名前 : 型 -> unit function 名前 : This, 型 -> This * unit
method 名前 : 型1 -> 型2 function 名前 : This, 型1 -> This * 型2
field 名前 : 型 function 名前 : This -> 型

この表から、我々が、同じモノを色々な違った名前で呼びたがる傾向があることが読み取れるでしょう*9

関数と関数オブジェクト

「どうでもいい違いに惑わされないようにしよう」と言ってきたのですが、皆さんがあまり区別してない違いでどうでもよくないものもあります。そのひとつに関数と関数オブジェクトの違いがあります。

手短な説明をするので、この節は分かりにくいかも知れません。分かりにくいときは飛ばして、ラムダ計算や関数型言語を学習した後でまた読んでください。

C言語Javaなどの伝統的プログラミング言語で関数と呼ばれるもの、あれは確かに関数だとしましょう。副作用があるから関数じゃない、って? それはどうでもいいです。

型構成子(型=集合に関する演算)記号として、直積記号'*'と直和記号'|'を導入しました。もうひとつの型構成子記号として'-*'を導入します*10。数学的記法との対応は:

型構成子記法 数学的記法
X * Y X×Y
X | Y X + Y
X -* Y YX

YXは、集合Xから集合Yへのすべての関数からなる集合です。数学的記法に掛け算、足し算、累乗の記号が使われているのが納得できないなら、次の記事を読んでみてください。

HaskellStandard MLなどで使われる矢印記号'->'は、関数のプロファイル(引数型と戻り値型の組み合わせ)ではなくて、型構成子です。数学的なYXを X -> Y と書いているのです。これは事情を分かりにくくするので、型構成子記号'->'を'-*'に変更しました。我々の矢印'->'は、あくまで関数のプロファイルです。

Standard MLの val f: X -> Y を我々の記法で書くと value f : X -* Y です。valueは特別なfunctionの略記だったので、

  • function f : -> (X -* Y)

さらにunitも明示的に書いてみれば:

  • function f : unit -> (X -* Y)

HaskellStandard MLで言っている関数とは、データオブジェクトとみなした関数 -- つまり関数オブジェクトです。関数オブジェクトの名前fとは、“集合(X -* Y)の値を取る引数なし関数”です。引数なしの関数とは値〈value〉と同じことなので、fは“関数オブジェクト値の定数”です。

次のStandard MLの宣言だとより事情がハッキリします。

  • val g: X -> Y -> Z

これは、我々の書き方では次の意味です。

  • value g: unit -> (X -* (Y -* Z))

gは、集合(X -* (Y -* Z))の要素を指し示す名前です。Xの要素aに対して、g a と書くと、今度は集合 (Y -* Z) の要素を指し示します。Yの要素bをとって g a b と書くと、集合Zの要素を指し示すことになり、あたかも2引数の関数を呼び出したように振る舞うのです。

g a b と書いたときの空白がくせ者で、空白が評価関数〈eval function | evaluator〉を呼び出しているのです。我々の書き方で、

  • Eval_1 : (X -* (Y -* Z)), X -> (Y -* Z)
  • Eval_2 : (Y -* Z), Y -> Z

とすると、g a b は次の式を意味します。

  • Eval_2(Eval_1(g, a), b)

HaskellStandard MLでは、このようなメカニズムを意識させないように巧みな構文糖衣〈シンタックスシュガー〉でくるんでいますが、かえって目眩〈めくら〉ましになっているかも知れません。HaskellStandard MLでは、関数は現れず、関数オブジェクト(値としての関数)だけなんです。関数オブジェクトを関数として働かせているのは、評価演算子〈evaluator〉(または適用演算子)である“空白”です。

この節の説明は舌足らずでしたが、事情をシッカリ把握するにはラムダ計算のデカルト閉圏によるモデルを勉強するのがよいでしょう。

言い残したことなど

次のような話題がまだ残っています。

  1. トランスフォーマー
  2. 指標に対する様々な操作
  3. 相対指標、部分インスタンス、指標のパラメータ化
  4. プロファイル推論/指標推論
  5. データストアオブジェクト
  6. さらにオブジェクト指向
  7. データベーススキーマ
  8. メイヤー流の契約モデル
  9. 名前構造と名前管理
  10. 表明付きの指標
  11. 高次の指標

このなかで最も重要なのはトランスフォーマーStandard MLのfunctor相当)です。これ、ホントゥに重要なんです。トランスフォーマーは、ある指標ともうひとつの指標を繋ぐ変換です。トランスフォーマーは、他の概念(2番目以降の項目)を統一的に説明する基礎となります。また、トランスフォーマーは、「良いプログラミングとは何か」に強い示唆を与えます。

指標を操作対象とする操作があります。例えば、指標に出現する名前のリネームとか、指標の一部分だけを取り出すとかです。2つの指標を一緒にする演算(マージ)も重要です。モジュールに対する演算や、オブジェクト指向の継承などは、指標に対する操作によりスッキリ説明できます。

最近のプログラミング言語は、“ジェネリクス”として型パラメータをサポートしますが、指標のパラメータ化は、通常の“ジェネリクス”よりさらに一般的な機構です。ただし、パラメータ化でもまだ機能不足や問題点があるので、相対指標と部分インスタンスという概念を導入して再定式化したほうがいいでしょう。

人間がいちいち型を書かなくても済む機能として型推論があります。同様に、人間がいちいちプロファイルや指標を書かなくてもいいようにするのがプロファイル推論/指標推論の機能です。現実には、ソフトウェアが推論してくれないと「やってられない」程度に面倒になると思います。

データストアオブジェクトという、特別な種類の指標とインスタンスを導入すると、状態遷移やオブジェクト指向のオブジェクトを説明しやすくなります。データストアオブジェクトは、オブジェクト指向に限らず至る所に出てくる概念です。

データベースのテーブルスキーマは特殊な指標です。テーブルが隠蔽型、カラムが関数です。データベースのライブラリやORマッパなどは、トランスフォーマーだと考えられます。指標とトランスフォーマーを使ったデータベース理論は、関手データモデルに近いものです。

Command-Query分離で名前を出したメイヤー先生は、契約による設計〈design by contract〉でも有名です。ソフトウェア仕様技術の根本を、権利と義務という比喩で極めて的確かつ鮮やかに描き出してくれました。指標はメイヤーの意味での契約書とみなせます。利用者の権利と実装者の義務を記述したものが指標=契約書です。メイヤーの契約モデルは単なる比喩にとどまらず、理論的分析にも大変に有効です。僕は、普通の証明の話でもメイヤー・モデルを使っています→「証明の“お膳立て”のやり方 2: 証明の顧客・業者モデル

現状のプログラミング言語では(HaskellにしろCoqにしろ)、型クラス(指標)に関連する名前の扱いがうまくいってないようです。名前をどのように構造化/管理するかも考えるべき課題です。オーバーロード問題も名前の問題ですね。(「ハイコンテキストな定数・記号の解釈」も参照。)

今回扱った指標は、“名前に関する約束”ですが、それらの名前(型名または関数名)が満たすべき条件を表明〈アサーション〉として追加すると、正確な仕様記述、ソフトウェアの“テスト”/“正当性の証明”につながります。ソフトウェアの話に限らず、表明を普通の論理式とみなせば、証明支援系/証明検証系もまた型クラスをヘビーに使います(例えば「Coqで半環:アンバンドル方式の例として」参照)。

指標に出現する名前は、型名か関数名だと言いました。指標を図示すると、型名はノードのラベル、関数名は辺のラベルとなる有向グラフになります。有向グラフは1次元の図形ですね。これを2次元以上の図形にして、対応する表現を考えると高次の指標になります。表明付きの指標は、2次元の指標の特別なものです。

今回説明したように、型クラス=指標は、かなり単純な概念です。幾つかの名前を、その使い方を添えて集めただけのものですから。にも関わらず、関数型言語からオブジェクト指向言語まで、あるいは仕様記述言語などまでカバーする強力な概念装置なのです。現存する言語は、この概念装置のパワーを十分には利用しきれてないように思えます。もう少し型クラス=指標と深く付き合ってみてはどうでしょう -- と言ってこの記事を締めます。


一年数ヶ月もあいだが空かないで続きが書けるといいのですが…

*1:問題点を解決するのは無理でしょう。もとがダメだから。

*2:余分な区切り記号を認めない構文だと、最後の1行の削除で構文エラーが起きて辛い!

*3:僕が知らないだけで、Standard MLのfunctorのような仕掛けが何かあるかも知れません。

*4:By Pearson Scott Foresman - Archives of Pearson Scott Foresman, donated to the Wikimedia Foundation このファイルは以下の画像から切り出されたものです: PSF H-450005.png, パブリック・ドメイン, https://commons.wikimedia.org/w/index.php?curid=3237459

*5:TypeScriptでは、型宣言を型注釈と呼ぶようです。

*6: (void 0) === undefined は真ですが、(void 0) === null は偽です。よって、voidの値はundefinedにすべきだと思います。が、nullを、voidの値のように取り扱ってきた悪しき伝統があるので、致し方なくnullもvoid値に認めたのでしょう。

*7:"instance"が「例」だから、「インスタンス例」って日本語は変かも。

*8:指標の名前もありますが、指標内に出現する名前は(今回は)型名と関数名です。

*9:違った名前を使われると、同じモノであることを認識しにくくなるので困ったことです。が、これはどうにもならない気がします。違った名前を付けたがるのは、人間の本能的欲求みたいです。おそらく、集団を形成したいという本能の一部なのでしょう。

*10:これは圏論的指数演算の記号なのですが、どんな記号にするか、毎回頭を痛めます。「圏の指数のための中置演算子記号」参照。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20180109

2017-12-28 (木)

圏論的宇宙の対象化原理

| 16:03 | 圏論的宇宙の対象化原理を含むブックマーク

ここのところ3日間、圏論的宇宙〈categorical universe | category theoretic universe〉について書きました。

初回のタイトルに「ファンタジー」が入っているくらいに、ボヤッとした話です。天文学的宇宙の話が、楽しいけど実際にこの目で確認できないのと同じような感じですね。今回もボヤッとした仮説について述べます。ある次元の宇宙(のスライス)が、1次元高い対象になるだろう、という仮説です

内容:

  1. 原理?
  2. 対象化原理
  3. 正次元の対象化原理
  4. 対象化と論理

原理?

(-2)以上のすべての整数nに渡って、すべてのn-圏を寄せ集めた総体が圏論的宇宙です。圏論的宇宙には、圏論的実体(対象、射、圏、関手、自然変換、etc.)が一切合切〈いっさいがっさい〉入っています。圏論的宇宙と個々のn-圏の構造を探るための指導原理に反転原理を使いました。

反転原理は、「原理」とは呼んでいますが実際には仮説です。「圏論的宇宙と反転原理と次元付きの記法」では「経験則」と書いています。

これ[反転原理]は、単一のn-圏の構造は、圏論的宇宙の構造を反転させた姿をしているようだ、という経験則です。

反転原理は、経験則 -- 観測された事実らしきものです。何でそうなるかの説明はできません。いつか、もっと基本的な事実から証明されるかも知れないし、「そういうものなんだ」と受け入れるしかないのかも知れません。反転原理が実際は成立してない可能性だってあります。

とはいえ、反転原理を主張する命題は、そこそこ厳密な形で述べることができるでしょう。これから述べる対象化原理は、主張の定式化も曖昧です。真偽のほどはともかくとして、厳密な定式化が出来たらそれで大したもんだ、という感じです。

対象化原理

「対象化」は"objectification"(動詞なら"objectify")のつもりです。対象化とは、ナニカを圏論の意味での対象〈objet〉にすることです。ナニカは、宇宙のひとつの階層です。

対象化原理の一番分かりやすい例は、「次元(-1)の階層全体を次元0の対象にする」ところです。出来上がる対象が0次元対象なので、0-対象化と呼びましょう。

次元(-1)の階層全体とは、(-1)-Catのことです。(-1)次元の対象が真偽値(TrueまたはFalse)だったので、(-1)-Cat = {True, False} です。{True, False}は二元の集合なので、明らかに集合圏の対象です。集合圏は0-Catでした。この事実は、次のように書けます。

  • 0-対象化: (-1)-Cat ∈ |0-Cat|

今出てきた次元(-1)と0を、他の整数に置き換えると、それらが全体として対象化原理〈objectification principle〉になります。

(-1)-対象化は次の形です。

  • (-1)-対象化: (-2)-Cat ∈ |(-1)-Cat|

(-2)-Catは「無」を表す記号*だったので、

  • (-1)-対象化: * ∈ |(-1)-Cat|

これは、*をTrueとみなして、True∈{True, False} のことだと解釈できます。

(-1)-対象化、0-対象化のケースにおいて、対象化で出来た対象はTrueとBoolです。真偽値のなかの真、集合圏のなかのブール集合は特別な役割をになっています。なんというか、基準や規範を与える特別な対象、そんな感じです。

正次元の対象化原理

さて、正の次元に対する 1-対象化, 2-対象化, … を考えてみます。とりあえずは、形式的に次元を代入してみます。

  • 1-対象化: 0-Cat ∈ |1-Cat|
  • 2-対象化: 1-Cat ∈ |2-Cat|

0-Catは集合圏Setで、1-Catは通常の圏の圏Catですから、

  • 1-対象化: Set ∈ |Cat|
  • 2-対象化: Cat ∈ |2-Cat|

うーん、頭が痛いことになりました。僕は、圏のサイズの問題をいつも避けて通っているのですが、ここでは避けられないなー。Setは巨大な圏なのですが、そのSetをひとつの対象として含むCat? 普通はCat小さい圏の圏です。CatSetを入れることは出来ません。

考え方はたぶん2つあるでしょう。

  1. Setは巨大だが、それのアバター〈化身〉である小さな圏setがあり、set∈|Cat| である。
  2. Catは、Setより“もっと巨大”な2-圏なので、Setをそのまま対象として格納できる。

どっちにしても難しいな。集合論反映原理というのがありますが、状況は少し似てるのかもしれません(よく知らんけど)。(n-1)-Cat ∈ |n-Cat| と書くときの後ろめたさを幾分かは緩和するために、対象化で得られた対象を小文字だけで書いて (n-1)-cat ∈ |n-Cat| とします。

  • 0-対象化: (-1)-cat = bool として、bool∈|Set|
  • 1-対象化: 0-cat = set として、set∈|Cat|
  • 2-対象化: 1-cat = cat として、cat∈|2-Cat|

対象化と論理

集合圏におけるブール集合(bool∈|Set|)、圏の圏における集合圏(set∈|Cat|)はなんか似てるところがあります。先に「基準や規範を与える特別な対象」と言いましたが、bool, setはその点で共通しているのです。

任意の集合Sに対して、1-ホム集合Set(S, bool)をとると、それは集合S上の述語の集合になります。Set(S, bool)は外部ホム(集合圏の外から見たホム)ですが、集合圏では内部ホムを作れます。内部ホムは、[S, bool]とかboolSとか書きます。

次元を上げて、任意の圏Cに対して、1-ホム圏Cat(Cop, set)をとると、それは圏C上の前層の圏になります。Catでも内部ホムを作れて、[Cop, set](あるいはsetCop)が内部的な前層の圏です。

述語と前層はなんか似ていて、前層(あるいは層)の理論が述語論理の圏化のように思えます。ニ項の述語は関係ですが、関係の全体は [S×T, bool] in Set と書けます。次元を上げた類似物はプロ関手〈profunctor〉です。[C×Dop, set] in Cat です。プロ関手が関係の類似物であることはしばしば指摘されます。

述語と関係(二項述語)の理論(つまり論理)を前層とプロ関手の理論に系統的に“持ち上げる”方法があるのかもしれません。あるいは、次元によらない共通の枠組みがあるのかもしれません。

とまー、ほぼ「わかんない」のですが、圏論的な宇宙がのっぺらぼうではなくて、階層や階層をまたいだ構造を持つだろう、とは予測できます。そして、断片的な状況証拠からもある程度の知見が得られると思います。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20171228

2017-12-27 (水)

有界な圏論的宇宙と圏論的パス式

| 13:27 | 有界な圏論的宇宙と圏論的パス式を含むブックマーク

集合論でも圏論でも、宇宙は無限の彼方へと拡がっています。でも、適当な場所で限界を設けて、その限界の内側だけで十分なことが多い気がします。そのような狭い世界のなかでは、ファイルシステムやWebと同様に、パスにより実体を指し示すことができます。

昨日の記事「圏論的宇宙と反転原理と次元付きの記法」を前提とします。

内容:

  1. ワーキング宇宙
  2. 有界圏論的宇宙
  3. 圏論的パス式
  4. おわりに

ワーキング宇宙

現場の集合論としての有界素朴集合論」において、有界な宇宙Uというものを導入しました。Uには限界があります。銀河と呼ばれる集合(複数も可)がUの最上位にあり、銀河を越えて外に出ることはできません。

どこまでもどこまでも限りなく拡がる宇宙は魅力的ですが、たいていはご近所界隈で事が済むのではないかと思うのですよ。これは、無限に拡がる宇宙が存在しないとか、不要だと主張しているのではありません。現実的に何かの作業をするとき、全宇宙の情報や構造が必要なことは稀で、宇宙の一部を切り取ってくれば事足りるケースが多いだろう、ということです。

上記の事情を明白に表現するために、ワーキング宇宙〈working universe | 作業宇宙〉という言葉を導入しましょう。これは文字通り、何かの作業で必要とされる小宇宙(大宇宙の一部)です。

集合論の宇宙だけではなくて、圏論の宇宙においても、有界なワーキング宇宙を設定してみます。圏論の大宇宙では、(-2)-Cat, (-1)-Cat, 0-Cat, 1-Cat, ... と、いくらでも高い次元のn-圏が並んでいます。適当な整数kを固定して、幾つかのk-圏と、kより小さい次元の圏達があれば十分な状況を想定します。

必要とするk-圏を含む(k+1)-圏をひとつ選んで、これを我々の銀河Gとします。ひとつの銀河Gとその内側がワーキング宇宙となります(単銀河小宇宙)。Gに含まれるモノ(論理的に許容されるモノ)を何でもかんでもワーキング宇宙に入れる必要はありません。我々が選んだモノだけをワーキング宇宙に入れます。

有界圏論的宇宙

圏論的宇宙(大宇宙)の全体像は、おぼろげながら次の記事で述べています。

大宇宙のなかで圏論的ワーキング宇宙を構成しますが、話を具体的にするために、k = 2 とします。つまり我々は、幾つかの2-圏を必要とします。そうなると、幾つかの2-圏を収めている親の圏(それが銀河)G2-Catの部分圏とみなせます。もう少し正確に言うと、Gは3-圏であり、2-Catへの忘却関手(忠実関手)を持ちます。この忘却関手は3-圏のあいだの関手なので3-関手ですが、'3-'は気にしないことにします。

Gは入れ物であって、我々が作業のために必要としている2-圏はKLだとします。K, L∈|G| ですね。KLのあいだに関手(2-関手) F:KL があれば、それもGのなかのモノです。しかし、Gの外側は考えません。Gは我々の唯一の銀河であり、銀河の外は一切見えないとします。

圏(n-圏を含む)、対象、射(n-射を含む)、関手(n-関手を含む)、自然変換(n-自然変換を含む)など、圏論で出てくるモノ一切合切〈いっさいがっさい〉を圏論的実体〈categorical entity〉と呼ぶことにします。圏論的実体とは、圏論的宇宙のなかの存在物です。逆に言うと、圏論的宇宙は(大宇宙であれ、ワーキング宇宙であれ)圏論的実体から構成されます。

圏論的な大宇宙は茫漠としていますが、銀河Gで限界を設定されたワーキング宇宙のなかはシッカリと把握したいものです。把握の第一段階として、銀河Gで限られたワーキング宇宙の内部にある圏論的実体を名指しする方法を考えます。

圏論的パス式

パス式〈path expression〉は、コンピュータやインターネットではお馴染みの表現です。例えば、コンピュータのなかにあるファイルは、/home/hiyama/ProjectX/docs/Overview.md のようなパス式で名指しされます。インターネット上のドメインやリソースも、http://www.chimaira.org/misc/index.html のようなURLで示します。メールアドレス hiyama@nakame.chimaira.org もパス式の一種と言えるでしょう。

ローカルファイル名 /home/hiyama/ProjectX/docs/Overview.md では、左から右に向かって「大分類→小分類」となっています。ドメイン名 nakame.chimaira.org では逆で「小分類→大分類」です。両方の方式、あるいはそれらを混ぜた方式が実際に使われています。

圏論的パス式は、圏論的実体(リソースに相当)を指し示す階層的名前です。ファイル名方式(左が大分類)とドメイン名方式(右が大分類)の両方を使います。ドメイン名方式は既に出てきています。「圏論的宇宙と反転原理と次元付きの記法」で紹介したプロファイル表記がドメイン名方式のパス式です。

ここでは、ファイル名方式の圏論的パス式を導入します。基本的に、プロファイル表記を左右ひっくり返して書くだけです。分かりにくいと思ったらプロファイル表記に書き直してみてください。

今まで述べてきた事例で説明します。ワーキング宇宙には、2-圏KLがありますが、これはトップレベル(ルート直下)にあるので、/K, /L のように書きます。銀河Gも明白に書きたいなら //G/K, //G/L とします。'//'はスーパールート記号で、ワーキング宇宙全体を示すと思えばいいでしょう。Gは、ファイルシステムで言えば「ドライブ、ボリューム、デバイス」などと呼ばれるものに相当します。

//G/K は2-圏なので、対象を持ちます。その対象は、//G/K/A のように書きます。この書き方も階層的ファイルシステムと同じです。ファイルシステムと違うのは、ホムシングもパス式で書けることです。//G/K/(A, B) は、Hom1K(A, B) を表します。丸括弧はなくても大丈夫なので、//G/K/A,B のように書いていいとします。

//G/K/A,B は2-圏Kの1-ホムシングなのでホム圏です。よって対象を持つので、その対象は //G/K/A,B/f のように書けます。プロファイル記法に直せば:

  • f:A→B in K in G

'in'が2つ並んでますが、2つのプロファイルの略記だと思ってください。

  1. f:A→B in K
  2. K in G

先のアドバイス「分かりにくいと思ったらプロファイル表記に書き直してみてください」を思い起こしましょう。

//G/K/A,B/f,g/α に対するプロファイル記法は、

  • α::f⇒g:A→B in K in G

複数のプロファイルに分解すれば:

  1. α::f⇒g:A→B in K
  2. K in G

もっと細かく分解すれば:

  1. α::f⇒g in K
  2. f, g:A→B in K
  3. A, B in K
  4. K in G

あるいは、

  1. α∈Hom2K(f, g)
  2. f, g∈Hom1K(A, B)
  3. A, B∈Hom0K
  4. K∈Hom0G

パス式を用いることによって、圏論的実体のプロファイル情報がコンパクトに表現できることが分かるでしょう。

カンマを使ったホムシングを、トップレベルで使うこともできます。F, Gを2-圏KからLへの関手(2-関手)、ξをFからGへの自然変換(2-自然変換)だとして、ξを表すパス式は次のようになります。

  • //G/K,L/F,G/ξ

プロファイル記法に書き直せば:

  • ξ::F⇒G:KL in G

おわりに

僕が有界なワーキング宇宙に拘るのは、際限もなく拡がる大宇宙は超越的過ぎて我々人間が太刀打ちできる気がしないからです。限界が設定されて、個々のモノ(圏論的実体)が構成的に定義され、圏論的パス式でモノ達を名指しができる小宇宙なら、神ならぬ我々でも把握ができるでしょう。

とは言っても、有界なワーキング宇宙でさえ実際の構成は難しく、超越的大宇宙と完全に切り離して議論もできません。例えば、SetCatのように、存在すると信じられているお馴染みの圏/2-圏をワーキング宇宙に取り込むにはどうしたらいいのでしょう?

もしホントに反転原理が成立しているなら、個々のn-圏は圏論的大宇宙の構造を反映しているはずです。したがって、有界なワーキング宇宙を探るにも大宇宙の知識が必要となります。んー、まだファンタジーの世界みたい。

2017-12-26 (火)

圏論的宇宙と反転原理と次元付きの記法

| 18:10 | 圏論的宇宙と反転原理と次元付きの記法を含むブックマーク

ファンタジー: (-1)次元の圏と論理」の最後の一文:

このファンタジーに、リアリティが加わるといいんですけど…

圏論的宇宙をチャンと理解するのはなかなかに難しいですが、記法を整備するくらいはできるので、やっておきましょう。

内容:

  1. 圏論的宇宙と反転原理
  2. プロファイル記法
  3. n-射の形状
  4. ホムシングとモーシング
  5. 任意のnに対する記法と略記

圏論的宇宙と反転原理

公理的集合論の宇宙〈universe〉は非常に単純化されていて、この世に存在するすべてのモノは集合と考えます。要素という概念はありますが、ふたつの集合の関係性において、片方が果たす役割を要素と呼んでいるだけです。

アトム〈atom | 原子〉を導入すると、アトムは要素にしかなれないので絶対的要素である、と言ってもいいでしょう。銀河〈galaxy〉を導入すると(銀河については「現場の集合論としての有界素朴集合論」を参照)、銀河は要素になり得ないので絶対的集合だと言えます。

アトム/銀河を導入しても、集合論的宇宙は比較的シンプルです*1。では、圏論的宇宙はどうでしょう。高次圏も含めたn-圏達の全体が圏論的宇宙なんですが、そもそも、n-圏の生態が分かってない*2ので、宇宙の構造もハッキリしません。ごくラフな(詩的な)描像は、昨日「ファンタジー: (-1)次元の圏と論理」で述べました。

昨日の記事で反転原理(または反転仮説)というものを提案したのですが、これは、単一のn-圏の構造は、圏論的宇宙の構造を反転させた姿をしているようだ、という経験則です。

「反転」の意味を説明しましょう; 圏論的宇宙は、(-2)-圏の階層、(-1)-圏の階層、0-圏の階層、1-圏の階層、… のように、圏の次元により階層化されています。一方で単一のn-圏は、0-射の階層、1-射の階層、2-射の階層、… のように射の次元により階層化されています。この2つの階層のあいだに次のような関係があります。

宇宙の階層 n-圏Kの階層
(-2)-Cat Homn+2K
(-1)-Cat Homn+1K(α, β)
0-Cat HomnK(f, g)
(n-1)-Cat Hom1K(A, B)

なんかゴチャゴチャしているので、次元(整数値)だけを取り出すと:

宇宙の階層 n-圏Kの階層
-2 n+2
-1 n+1
0 n
n-1 1

「…」の部分を一般的に書けば:

  • j ←→ n - j (-2 ≦ j < n)

次元のあいだの関係は単純で、たしかに反転しています。ゴチャゴチャしている部分を以下で説明し、同時にゴチャゴチャを整理する記法を導入します。

プロファイル記法

圏論のなかでは、f:A→B という記法がまず間違いなく使われます。見たことあるでしょ。この書き方の A→B の部分をfのプロファイル〈profile〉と呼びます。プロファイルとホム集合〈homset | ホムセット〉は次のように関係しています。

  • f:A→B in C ⇔ f∈C(A, B)

このとき、AとBはCの対象ですが、A(あるいはB)がCの対象であることを A in C と書きます。A:C と書く人もいますが、この書き方は採用しません。その理由は後で述べます。

  • A in C ⇔ A∈|C|

次に高次圏を考えます。いきなり一般のn-圏は難しいので、Kは2-圏だとします。Kの対象はA, Bなど、射はf, gなど、2-射はα, βなどで表します。対象と射については普通の圏(1-圏)と同じ書き方をします。

  • A in K ⇔ A∈|K|
  • f:A→B in K ⇔ f∈K(A, B) ん、これでいいのか?

2-圏において、K(A, B)は単なる集合ではなくて圏でした。ホム圏と呼ぶのでした昨日の記事参照)。fは、ホム圏K(A, B)の対象なので、

  • f:A→B in K ⇔ f∈|K(A, B)|

となります。

αがfからgへの2-射のとき、2-射らしくコロンを2つ、二重の矢印を使います。

  • α::f⇒g

fとgは共通の域・余域を持っていて、f, g:A→B です。この事情まで書くと:

  • α::f⇒g:A→B in K

ホム圏との関係は次のよう。

  • α::f⇒g:A→B in K ⇔ ( α∈Mor(K(A, B)), dom(α) = f, cod(α) = g, (f, g∈|K(A, B)|), A, B∈|K| )

同値の右辺の記述が煩雑なので、これは後で整理することにします。

もし、Kが3-圏ならば、3-射もあるので、それを次のように書きます。

  • Ψ:::α≡>β::f⇒g:A→B in K

もうお分かりですね。3個のコロン、三重の矢印です。

一般に、n-射のプロファイルはn個のコロン、n重の矢印です。n個のコロンを :n 、n重の矢印を →n と書くことにすれば、n-射σのプロファイルは、

  • σ :n x →n y

n = 0 のときは0-射=対象のプロファイル、0個のコロンなので、:0 なんですが、これは空になってしまうので、:0 の代理にキーワード'in'を使うことにしています。先の3-射のプロファイルを累乗(上付きの指数)形式で書き直せば:

  • Ψ :3 α →3 β :2 f →2 g :1 A →1 B :0 K

見やすくはないのですが、nがどんな大きな数でも、コロンと矢印の系列としてn-射のプロファイルを書けます。

n-射の形状

ここでちょっとした注意事項をはさみます。

現状、n-圏の定義は色々あって、異なる定義が同値なのか否か? どれが適切なのか? そもそも適切性の基準があるのか? などが分かっていません。n-圏を構成するn-射として、どういう“形状”を選ぶかで、異なる流儀になります。n-射の形状としては次があります(もっと他もあるかも知れません)。

  1. 球体〈globe〉
  2. 単体〈simplex〉
  3. 方体〈cube〉
  4. マルチトープ〈multitope〉
  5. オペトープ〈opetope〉
  6. デンドレックス〈dendrex〉
  7. テータ・セル〈theta cell〉

このなかで、最も簡単そうに思えるのが球体です。証明支援系Globularの名称は、球体の"globe"から来ています。実際、Globularは球体モデルを採用した高次圏ソフトウェアです。

前節で紹介したn-射のプロファイルの書き方は、n-射の形状がn-球体であることを前提にしています。球体以外の形状を採用するアプローチだと、プロファイルはもっと複雑になります。

僕は、一番扱いやすいという理由で球体アプローチを支持しています。他の形状を否定はしませんが、難しいので、とりあえずは球体アプローチでやってみよう、という態度です(けっこう安易)。

n-圏への球体アプローチの雰囲気は次の記事で書いています。

ホムシングとモーシング

圏の定義も幾つかの流儀がありますが、たぶん一番よく使われている定義は、圏Cの対象〈object〉の集合(または類)Obj(C)と、圏Cの射〈morphism〉の集合(または類)Mor(C)から出発するものでしょう。

Mor(C)から始めた場合、Cのホム集合〈homset | ホムセット〉は次のように定義します。

  • HomC(A, B) := {f∈Mor(C) | dom(f) = A, cod(f) = B}

Obj(C)は|C|と略記され、HomC(A, B)はC(A, B)と略記されます。

以下、集合と類(集合より大きいかも知れない集まり)を区別せずに単に集合と言います。Obj(C)をObjC、Mor(C)をMorCと下付き添字で書くことにします。MorCを、圏Cモー集合〈morset | モーセット〉と呼ぶことにします。「モー」はmorphismの"mor"です。

n-圏に対して、そのホム集合、モー集合を定義したいのですが、また2-圏の例から始めます。Kを2-圏とします。まずは、0-ホム集合と0-モー集合を対象集合として定義します。この定義がベースとなります。

  • Hom0K = Mor0K := |K|

より高次のホム/モーを定義していきますが、それらは必ずしも集合ではないので、ホムシング〈homthing〉、モーシング〈morthing〉と言い換えることにします。実は、モーシングはほとんどの場合集合で、(n + 2)次元のときだけモー値となります。

モーシングより先にホムシングを考えます。反転原理により、2-圏Kの1-ホムシングは1-圏です。よって、1-圏(普通の圏)の対象集合をとれます。その対象集合が1-モーシングです。

  • Mor1K(A, B) := |Hom1K(A, B)|

このモーシングは、2つの対象A, Bでパラメータ付けられた集合の族です。モー集合達を全部寄せ集めてパラメータなしのモーシング(モー集合)を定義します。

  • Mor1K := ∪{A, B∈Mor0K | Mor1K(A, B)}

この定義の右辺は、集合族の総合併を意味します。

2次元のホムシングは2-射の集合(つまりホム集合)です。

  • Hom2K(f, g)

fとgの両端が同じ(共端)でないと、2-射は存在しないので、f, gの共通するプロファイルを添えておけば:

  • Hom2K(f, g:A→B)

モーシングはホムシングの対象部分をとります。

  • Mor2K(f, g) := |Hom2K(f, g)|

2-ホムシングHom2K(f, g)は単なる集合でした。集合Sに関してその対象部分|S|はその集合自身(|S| = S)なので、次のように書いても同じです。

  • Mor2K(f, g) := Hom2K(f, g)

パラメータ付きのモーシング(モー集合)達を全部寄せ集めてパラメータなしの2-モーシングを作るので、

  • Mor2K := ∪{f, g∈Mor1K | Mor2K(f, g)}

ここまでは普通の構成です。3次元((2 + 1)次元)と4次元((2 + 2)次元)のホムシング/モーシングの構成には、負次元の圏に対する反転原理を使います。圏論的宇宙のビッグバン以前の状況(昨日の記事参照)が、3次元と4次元のホムシング/モーシングに反映します。

2-圏Kの3次元のホムシングは真偽値(つまりホム値)です。

  • Hom3K(α, β) (これはTrueかFalseのどちらか)

αとβに共通するプロファイルを添えておけば:

  • Hom3K(α, β::f⇒g:A→B)

モーシングはホムシングの対象部分…、いやっ、真偽値にはもはや対象部分という概念がないので、値そものをとります。

  • Mor3K(α, β) := Hom3K(α, β)

パラメータなしの3-モーシングは、真偽値True, Falseの寄せ集めでブール集合になります。

  • Mor3K := ∪{α, β∈Mor2K | Mor3K(α, β)} = {True, False}

次元4は、圏論的宇宙が始まる前の状態を反映するので、真も偽もなく、個体と全体の区別さえない状況で考えます*3

  • Hom4K = Mor4K = *

'*'は何もないことを示す目印です。集合論的宇宙でも圏論的宇宙でも、「はじめに無ありき」から出発するのは面白いですね。

任意のnに対する記法と略記

前節では、Kを2-圏として話をしました。2を任意のnとしても、同様にホムシング/モーシングを構成できます。0-ホムシング、0-モーシング、対象集合は同じものだとして、整数jを 1 ≦ j ≦ n とします。j次元のモーシングは次のように定義されます。

  • MorjK(x, y) := |HomjK(x, y)|
  • MorjK := ∪{x, y∈Morj-1K | MorjK(x, y)}

j = n + 1, j = n + 2 に関しては、いつでも同じで、

  • Morn+1 = {True, False}
  • Morn+2 = *

です。

jを大きい方から順に n + 2, n + 1, n, ..., 1 と見ていくと、圏論的宇宙の歴史を再現します。j = 0、つまり対象集合は特殊で、n-圏Kのなかに(n - 1)-圏がどのくらい含まれるかをコントロールするインデックスの領域のようです*4

通常の圏論において、対象集合とホム集合に略記がありました。

  • |C| := Obj(C)
  • C(A, B) := HomC(A, B)

高次圏でも同様な略記を導入しましょう。

  • |K|j := MorjK (0 ≦ j ≦ n + 2)
  • Kj(x, y) := HomjK(x, y) (x, y∈Morj-1K、1 ≦ j ≦ n + 1)

これらの略記を使えば、n-圏の階層的構造をかなりスッキリと表現できます。

*1:構造がシンプルというだけであって、やさしいわけではありません!

*2:有限のnだけでなく、∞-圏もあります。∞-圏はもっと分かりません。

*3:開闢以前の世界は混沌であり虚無であったわけです。なんか仏教ぽい香りがしますね。

*4:対象集合の特殊性を何かうまく解釈できないかと考えているんですけど、今のところよく分かりません。

2017-12-25 (月)

ファンタジー: (-1)次元の圏と論理

| 13:09 | ファンタジー: (-1)次元の圏と論理を含むブックマーク

しばらくブログを更新してなくて「死んでるんじゃないか?」と思われているので、なんか書きます。

クリスマスらしく(?)、詩的(ポエティック)な話をします。「詩的」を悪い意味にとれば、曖昧でハッキリしない話となります。良い意味にとれば、楽しいファンタジーが含まれる、ってことです。

内容:

  1. The Power of Negative Thinking (by バエズ)
  2. 高次圏の話
  3. 2-圏の例:圏の圏
  4. (-1)-圏とは何か
  5. n-圏の(n + 1)-射
  6. 地下室と屋根裏部屋に潜む論理
  7. 等式的代数構造
  8. 宇宙創生と反転原理

The Power of Negative Thinking (by バエズ)

随分と前(2006年)ですが、ジョン・バエズ(John Baez)が"The Power of Negative Thinking"の話をしてました。ネガティブシンキングは、ポジティブシンキングにあやかったんだか皮肉ったんだか? いずれにしても、「ネガティブに考えるといいよ」って話で、次の講義録の第2章のタイトルです。

バエズの言うネガティブシンキングは、正の次元だけではなくて“負の次元も考える”ということです。(-1)次元、(-2)次元とかです。この記事では、(-1)次元の圏に注目します。

で、まったくの余談を挿入するんだけど、ネガティブならぬポジティブシンキングというと、ジイさんの僕は1990年代に一世を風靡した故・斎藤澪奈子さんを思い出しますね。さかんに「ポジティブシンキング」とおっしゃっていました*1。一方、"Power of Negative Thinking"で検索すると、ジョン・バエズより先にジーザス&メリー・チェインというバンドのCDが引っかかります。

Power of Negative Thinking: B-Sides & Rarities

Power of Negative Thinking: B-Sides & Rarities

高次圏の話

ポジティブ=上昇志向で考えると、0次元のモノ、1次元のモノ、2次元のモノ、… と、次元は正の方向に昇っていきます。ネガティブ=下降志向で考えると、0次元のモノ、(-1)次元のモノ、(-2)次元のモノ、… と、次元が下降していきます。このときの次元は、高次圏の文脈で考えます。というわけで、負次元のモノを語る前に、高次圏の話をザッとしておきます。

n次元の圏を単にn-圏〈n-category〉と書くことにします。n ≧ 2であるn-圏は高次圏〈higher category〉と言ったりします。n = 1 のときは普通の圏です。高次圏の一般論はとても難しくて、どう定義すればよいのかも分かっていません(「n-圏の難しさについて」とそこから参照されている記事群を参照)。比較的に扱いやすい種類として厳密なn-圏〈strict n-category〉があります。いま、「厳密」の定義はしませんが、国語辞書に載っている「厳密」とは違います

かつての用語法では、厳密なn-圏を単にn-圏と呼んでいて、必ずしも厳密とは限らない一般のn-圏に別な呼び名を与えていました。

n 厳密なn-圏 一般のn-圏
2 2-category bicategory
3 3-category tricategory
4 4-category tetracategory

最近では、形容詞strict(またはstrong)とweakを付けて区別することが多いと思います。

n 厳密なn-圏 一般のn-圏
2 strict 2-category weak 2-category
3 strict 3-category weak 3-category
4 strict 4-category weak 4-category

ここでは、高次圏としては一番次元が低い2-圏を主に扱います。strictかweakかはあまり突っ込まないことにします。

2-圏の例:圏の圏

2-圏の例で、もっともポピュラーなのは“圏の圏”Catでしょう。Catは2次元の圏なので、0次元, 1次元, 2次元の射を持ちます。

  • 0次元の射とは、対象のこと。つまり、(小さい)圏が0次元の射。
  • 1次元の射とは、関手のこと。
  • 2次元の射とは、自然変換のこと。

Catを1次元の圏(普通の圏)と考えるならば、C, D∈|Cat|に対してCat(C, D)は関手の集合になります。しかし、2次元の圏だと考えれば、Cat(C, D)は単なる集合ではなくて圏です。よって、Cat(C, D)はホムセットではなくてホム圏〈homcategory〉と呼ぶべきです。

集合以外のホムを考えることは重要です。例えば、豊饒圏〈enriched category〉の文脈では、距離空間は圏とみなせますが、そのときのホムは非負実数値なので、ホム値〈homvalue〉と呼ぶのがふさわしいでしょう(豊饒圏や距離空間の話は、例えば「モノイド圏、豊饒圏、閉圏と内部ホム」、「移動のコストとしての距離」参照)。ホム集合に限らず、ホム圏やホム値もあるので、一般的にはホムシング〈homthing〉と呼ぶことにします。

さて、Catの話に戻ります。0-射の集まりもホムシングだと考えましょう。すると:

  • 0-射の集まり=0-ホムシング は、対象達の集合(あるいは類)だからホム集合
  • 1-射の集まり=1-ホムシング は、関手と自然変換からなる圏だからホム圏
  • 2-射の集まり=2-ホムシング は、自然変換のからなる集合(あるいは類)だからホム集合

各次元のホムシングを明示的に表すために次の記法を導入します。

  • Hom0Cat = |Cat| = (Catの対象の集合=圏の集合)
  • Hom1Cat(C, D) = (CからDへの関手と自然変換がなす圏)
  • Hom2Cat(F, G:CD) = (CからDへの関手F, Gを繋ぐ自然変換がなす集合)

0次元のホムシングは1個しかありませんが、高次のホムシングはたくさんあります。次元が高くなると、ホムシングはどんどん細分化されます。0次元のホムシングはこれといった構造を持たない集合(あるいは類)ですが、1次元のホムシングは圏という豊かな構造を持ちます。次元が上がった2次元のホムシングは再び無構造になります。

0次元のホムシングは無構造で、1次元ではホムシングが構造を持ち、ホムシングの次元が上がると構造が失われる傾向があります。この傾向性を探る(つうか眺める)のがこの記事の目的です。

なお、もっと2-圏の例を知りたいなら、「モナド論をヒントに圏論をする(弱2-圏の割と詳しい説明付き)」に10個の例を挙げています。

(-1)-圏とは何か

冒頭で触れたバエズのネガティブシンキングの話、負(マイナス)の次元を持つ圏について、まずは結論を言ってしまいましょう。(-1)次元の圏とは、真偽値〈真理値 | truth value〉です。真偽値とは真または偽のことですね。

この唐突な主張に対して、バエズは幾つかの根拠を示しています*2。僕は、そのうちのひとつしか覚えてないので、根拠をひとつだけ述べます。

負の次元にいく前に、0次元の圏(i.e. 0-圏)とは何でしょうか。n-圏は、n-射まで持つ圏なので、0-圏は0-射まで、いや0-射しか持たない圏です。0-射とは対象のことでした。となると、0-圏は単なる集合です。

  • 0-圏とは集合
  • 0-圏の0-射は集合の要素

これはいいですよね。

n-圏に対する一般的な法則として次があります。

  • n-圏の1-ホムシングは、(n - 1)-圏である。

n = 2, n = 1 のときに確認してみます。

  • 2-圏の1-ホムシングは、(2 - 1)-圏である。2 - 1 = 1 だから、1ホムシングは1-圏。
  • 1-圏の1-ホムシングは、(1 - 1)-圏である。1 - 1 = 0 だから、1ホムシングは0-圏、つまり集合。

形式的に、n = 0 を代入してみます。

  • 0-圏の1-ホムシングは、(0 - 1)-圏である。

もし、この世に(-1)-圏が在るなら、それは0-圏の1-ホムシングとして観測されるはずです。0-圏とは単なる集合だったので、集合の1-ホムシングを定義できれば、それが(-1)-圏となります。

Sを単なる集合として、a, bをSの要素(対象、0-射)とします。Hom1S(a, b) って何だろう? -- これが課題です。

単なる集合は何の構造も持たないのですが、集合が集合であるための最低限の条件があります。それは、要素が区別できることです。なにかの集まりSからaとbを取り出したとき、a = b か、それとも a ≠ bかを判定できなくてはなりません。無構造の集合といえども、要素の同一性(or 非同一性)という“構造”は備えています。

要素の同一性/非同一性の記述として、次のような定式化はどうでしょうか。

  • a = b のとき、Hom1S(a, b) = True
  • a ≠ b のとき、Hom1S(a, b) = False

集合の1-ホムシングとして、TrueまたはFalseのホム値をとるとします。すると、ホムシングは次のようになります。

n n圏の1-ホムシング 1-ホムシングとなるモノの全体
2 ホム圏 圏の圏Cat
1 ホム集合 集合圏Set
0 ホム値 ブール集合{True, False}

n-圏の(n + 1)-射

強い説得力はないかも知れませんが、0-圏より低い次元の存在物があってもいいかな、くらいは感じていただけたでしょう。前節の議論は、次のことを指導原理にしていました。

  • n-圏の1-ホムシングは、(n - 1)-圏である。

これは一般化できて、

  • j≧1 に対して、n-圏のj-ホムシングは、(n - j)-圏である。

n = 2 の場合で言えば:

  • 2-圏の1-ホムシングは、(2 - 1)-圏である。1-圏は圏なのでホム圏。
  • 2-圏の2-ホムシングは、(2 - 2)-圏である。0-圏は集合なのでホム集合。

ここで、j = 3 を代入すると、

  • 2-圏の3-ホムシングは、(2 - 3)-圏である。(-1)-圏は真偽値なのでホム値。

2-圏の3-ホムシングは真偽値らしいのですが、本来3-ホムシングとは何であるべきでしょうか。3-ホムシングは3-射の集まりと考えるのが自然です。もし(Catとは限らない)2-圏Kにも3-射があるとすれば、2-射 α::f⇒g, β::f⇒g に対して Ψ:::α≡>β::f⇒g のような形をしているはずです。

もともとは2射までしかない2-圏に3-射を導入するとすれば、2-射の恒等くらいしか候補がありません。つまり、3-射 Ψ:::α≡>β::f⇒g が存在するのは α = β のときに限り、Ψ = Idα と考えます。結局、2-圏Kに対して以下の命題はどれも同じ意味になります。

  • Ψ:::α≡>β::f⇒g in K
  • α = β, Ψ = Idα in K
  • Hom3K(α, β) = (α = β ならTrue, α ≠ β ならFalse)

やっぱり2-圏の3-ホムシングは真偽値のようです。その真偽値は、2-射の等しさを表現します。

地下室と屋根裏部屋に潜む論理

2-圏でオフィシャルに認められた射は、0-射, 1-射, 2-射です。ホムシングも、0-ホムシング, 1-ホムシング, 2-ホムシングは明確に定義されています。それに対して、(-1)-圏や3-ホムシングは無理にひねり出した印象があります。そうだとしても、結果は真偽値というよく知られた概念なので、排除すべき理由も見当たりません。

真偽値といえば、論理の中心的概念です。論理では真偽値が主役として最初から登場します。トポスのような、論理の圏論的定式化でも、ブール集合に相当するサブオブジェクト・クラシファイアがあり、真偽値は終対象からサブオブジェクト・クラシファイアへの射として定義されます。いたってまっとうな扱いです。

論理における真偽値の主役級の扱いに較べて、今回の真偽値の登場の仕方はどうでしょう。本来は人が住むべきではない地下室と屋根裏部屋に隠れていた得体の知れない生き物を引きずり出したら真偽値だった、と、そんなストーリーでした。

0-圏の1-ホムシングとしての(-1)-圏、n-圏の(n + 1)-ホムシングという奇妙な出自を持つ彼ら(TrueとFalse)は、論理的な働きをしてくれるのでしょうか。

等式的代数構造

我々がよく知っている代数構造、例えばモノイドを考えます。モノイドの構成要素は次のものです。

  • 集合 M
  • 写像 m:M×M→M
  • 要素 e∈M

集合圏とは限らないデカルト圏(終対象1を持つとする)Cでモノイドを考えるなら、

  • Cの対象 M
  • Cの射 m:M×M→M
  • Cの射 e:1→M

二項演算も単位元もどちらも射として定式化します。

これだけだと演算の法則性が何もないので、モノイドの法則(公理)を導入します。

  • ∀x, y, z:M. m(m(x, y), z) = m(x, m(y, z))
  • ∀x:M. m(e, x) = x
  • ∀x:M. m(x, e) = x

上記の法則記述には集合概念を使っているので、一般的なデカルト圏で通用するようにしましょう。射の等式(可換図式と同じ)で書き直します。話を簡単にするために、左単位律だけを扱います。特定の a:1→M in C を選んだとき、次の等式は一般のデカルト圏で意味を持ちます。

  • <e, a>;m = a : 1→M in C

このような等式をたくさん(無限個かも知れない)並べれば、∀x:M. m(e, x) = x の代用になります。前節の議論から、等式は圏の2射とみなすことができます。すると、モノイドのような等式的な法則を持つ代数構造は、次のモノ達で構成できます。

  • Cのひとつの0-射 M
  • Cのふたつの1-射 m:M×M→M と e:1→M
  • Cのたくさんの2-射

たくさんの2-射の一例が、LeftUnitEqa::(<e, a>;m)⇒a:1→M in C です。結合律、右単位律も、たくさんの2-射で表現できます。等式の性質(反射性、対称性、推移性)は、恒等2-射、2-射の可逆性、2-射の結合演算によって保証されます。

圏(普通の圏=1-圏)の等式的理論とは、実はたくさんの2-射を使った議論となります。2-圏で等式的理論をしたいなら、0-射, 1-射, 2-射以外に、3-射(等式と同じ)をたくさん使えばよさそうです。

宇宙創生と反転原理

話はさらに詩的(ポエティック)になります。

前節で述べたことは、n-圏の(n + 1)-射、あるいは(n + 1)-ホムシングを使えば、等式的理論は構成できて、モノイドのような等式的代数構造は、その枠組に包摂できるだろう、ということです。

しかし、我々は普通、等式/等号を集合圏の2-射/2-ホムシングと捉えたりはしません。集合S上の等号は、外延としては対角集合 ΔS = {(x, y)∈S×S | x = y}、内包としてはブール値をとる述語関数 eq:X×X→Bool, eq(x, y) = if (x = y) True else False と考えます。ここで、Bool = {True, False} です。

ブール集合(真偽値の全体)Boolは、最初から我々がいる世界Setのなかにあり、最初から見えています。屋根裏部屋に隠れているわけではありません。このギャップがとても気になります。僕が考えた(夢想した)詩的解釈は、僕らが見ているあのBoolはアバター〈化身〉であり、実身は集合圏Setの外に居るのだろう、というものです。

上記の詩的解釈を説明するには、集合圏だけではなくて、すべてのnに対するn-圏を総体として考える必要があります。その総体は、いわば圏論的宇宙です。n-圏の全体をn-Catと書くことにします。n = 0 のとき、0-圏は集合だったので、0-圏の全体0-Catは集合圏Setに他なりません。1-Catは、普通の圏の圏なので、1-Cat = Cat です。

今までの話から、(-1)-圏はTrueまたはFalseなので (-1)-Cat = {True, False} です。ただし、今のところ {True, False}∈|Set| とは考えていません。(-2)-圏には触れませんでしたが、(-2)-圏とは“なにか1つの値”と考えられます。その値を仮にアスタリスク('*')で表しましょう。(-2)-圏では、個と全体の区別もなく、(-2)-圏の全体も*です。

  1. (-2)-Cat = *
  2. (-1)-Cat = {True, False}
  3. 0-Cat = Set
  4. 1-Cat = Cat
  5. 2-Cat = (すべての2-圏達)
  6. ...

(-2)から始まることになったのは、我々が次元の付け方を間違えてしまった、ということでしょうが、致し方ありません。-2, -1, 0, 1, 2, ... という次元(番号付け)をこのまま使います。

(-2)-Cat, (-1)-Cat, 0-Cat, 1-Cat, 2-Cat, ... と次元で番号付けられた系列の全体が圏論的宇宙です。次元が増えるにしたがって、複雑さが増す階層になっています。また、次元番号を“時間”と解釈すると、宇宙創生の歴史がこの系列にエンコードされているとも思えます。

太古、宇宙には個も全体もなく、ただ「無」(*)だけが在りました。その後、真と偽の区別が生まれ、そしてビッグバンにより、今ある集合の全てが生まれたのです。その後は、次元を増やす射の概念により、宇宙にどんどん複雑なモノが追加され続けます。

このような宇宙の構造を見ていると、次の事実に気が付きます。

  • j次元の圏の全体は、(j + 1)次元の圏とみなせる。

簡単な例は j = -1 で、「(-1)次元の圏の全体は、0次元の圏とみなせる」です。言い方を変えれば、

  • 真偽値の全体は、集合とみなせる。

(-1)次元の圏(真偽値)の全体である(-1)-Catが、Boolという名前を与えられて、Bool∈|Set| となるのです。これが、「僕らが見ているあのBoolはアバター〈化身〉」と思う根拠です。アバターの実身はもちろん(-1)-Catです。

j = -2 で考えると、

  • (-2)次元の圏の全体は、(-1)次元の圏とみなせる。

(-2)次元では個と全体の区別がなく、(-2)次元の圏の全体も*です。ですから、

  • *は、真偽値とみなせる。

このみなし方は、*をTrueとみなすことでしょう。(-1)-Catのなかに棲む住人達は、自分たちが見ているTrueは、1次元低い世界にいる*のアバターだと捉えることでしょう。

さて、j = 0 ではどうでしょうか。

  • 0次元の圏の全体は、1次元の圏とみなせる。

これは、

  • 集合圏は、圏とみなせる。

ですから、お馴染みの主張です。とはいえ、直接的に Set∈|Cat| と言ってしまうのは問題があります。Catのなかに入り込めるようなSetのアバターが必要です。あるいは、Setを直接格納できるほどに巨大なCatを考えるべきかも知れません。まー、技術的な困難はありますが、j≧0 に対する「j次元の圏の全体は、(j + 1)次元の圏とみなせる」は首肯できる命題でしょう。

ここまでは、あらゆるモノを含む宇宙、マクロコスモスの話でした。宇宙のなかから特定のn-圏をひとつ取り出して眺めてみます。このn-圏Kも構造を持ち、ミクロコスモスを形成しています。Kのホムシングはn次元より上、(n + 1), (n + 2)にもあるとして順に見ていくと:

  • Homn+2K = *
  • Homn+1K(α, β) = True(α = β のとき) または False(α ≠ β のとき)
  • HomnK(f, g) = ( (n - 1)射fとgを繋ぐn-射の集合 )
  • ...
  • Hom0K = |K|

「...」で省略した部分には、複雑な構造を持つホムシングが並ぶかも知れません。

ミクロコスモスKの構造を見ると、マクロコスモスである圏論的宇宙の歴史を、次元が高いホムシングから次元が下降する方向に再現しています。これは、「マクロコスモスの時間発展が、発展方向が反転する形でミクロコスモスのなかにエンコードされている」と言ってもいいでしょう。発展方向とは、次元番号が増える方向です。仮に、宇宙の反転原理とでも呼んでおきましょう。

圏論的宇宙=マクロコスモスと、特定のn-圏=ミクロコスモスは、反転原理によってお互いを写し合っているようです。


(-1)次元の圏を契機に、圏論的宇宙の景色が少しは見えたような気がします。断片的ではありますが、他にも面白い景観や現象があります。このファンタジーに、リアリティが加わるといいんですけど…

*1:僕は、彼女のルックスが訳も無く嫌いで、何の興味も抱かなかったので実はよく知らんのですけどね。

*2:主たる動機は、圏論的周期律表〈periodic table〉を完全に埋める、ということだったみたい。