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

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

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

［参照用 記事］

JSONベースの型システムとミート付きクリーネ代数

雑記／備忘

「最近のCaty：型システムとクリーネ代数」の続きです。

今朝、型システム仕様の見落としを発見したりして。この機会に少し形式的にまとめておかないといかんなー、っと。

という次第で、僕の動機は、JSONベースの型システムにおいて見落としや勘違いを起こしやすい点を洗い出して、できるだけ明確にすることです。そのために、ミート付きクリーネ代数が役に立つと思っています。

内容：

  1. 前提と注意
  2. 配列とシーケンス
  3. JSONベースの型システムとは
  4. ミート付きクリーネ代数
  5. なにが問題か

前提と注意

これから考えるJSONは、次の点でほんとのJSONを単純化してます。

  • 配列型は考えるが、オブジェクト型は考えない。
  • スカラーを文字列型（string型）とヌル型（null型）だけにする。

以下では、いちいち「単純化した」という形容詞は付けずに、単に「JSON」と呼びます。

型の名前と型のデータ領域（インスタンス集合）は区別しないと混乱することがあります。本来ならば、意味関数を【-】のような太いブラケット（スコット・ブラケットと呼ぶようです）で表して、string型のデータ領域を【string】のように書くべきでしょう。でも、めんどくさいので、型名の先頭を大文字にしてデータ領域を表します。Stringはstring型のデータ領域です。このお約束は、型名に大文字を使うと破綻してしまいますが、型名はなるべく小文字始まりとして、あとは「文脈から判断してね」ということで。

nullと（いずれ出てくる）undefinedにおいては、型名とインスタンス・リテラルが同じ表記です。まー、これも文脈から「型名かリテラルか?」は判別できるでしょうが、混同しないようにご注意ください。

配列とシーケンス

配列とシーケンスの違いと、この2つを区別する理由はわかりにくいでしょう。区別する理由はおいおい納得してもらうとして、違いを述べておきます。

JSONの構文に従って、配列はブラケットで囲まれます。例えば、["hello", "world"] です。シーケンス（列、並び）は、配列のブラケット内の "hello", "world" の部分です。どうしてもシーケンスにまとまりを付けたいときは丸括弧を使います。("hello", "world") ですね。しかし、丸括弧はあくまで便宜上のもので、シーケンスの一部を構成しません。

さて、(["helo", "world"], "greeting") は長さ2のシーケンスです。そして、(["helo", "world"]) は長さ1のシーケンスです。丸括弧は便宜上のものだったので、["hello", "world"] は長さ1のシーケンスです。しかし、["hello", "world"] の配列としての長さは2です。

まとめると：

  • 単一の配列は、配列としての長さがなんであっても、シーケンスとしての長さは1である。
  • 配列に限らず、あらゆるJSONデータ（つっても、配列以外は文字列かヌル）は長さ1のシーケンスである。

配列は入れ子にできますが、シーケンスの入れ子はありません。[["helo", "world"], "greeting"] は入れ子の配列です。一方、(("helo", "world"), "greeting") と書いてみても、丸括弧は便宜上の記号なので、("helo", "world", "greeting") と同じです。別な言い方をすると、配列ではツリー状の構造を作れますが、シーケンスは直線上の構造しか作れません。直線に並んだ1つが入れ子配列であることは、もちろんありますが。

長さがnのシーケンスの全体をSnとすると、S = S0 + S1 + S2 + ... です。そして、「あらゆるJSONデータは長さ1のシーケンスである」ので、J = S1 となります。当然ながら、J⊆S です。Array⊆J だったので、Array⊆S1⊆S となっています。

JSONベースの型システムとは

今までの定義により、集合JがJSONインスタンスデータの領域です。x∈J とは、「xがJSONインスタンスデータだ」という意味。types as sets という素朴な立場をとると、型とはJの部分集合のことです。よって、型の集合はJのベキ集合 Pow(J) となります。そこで、T = Pow(J) と定義して、Tを型の集合だとみなします。t∈T とは、「tがJSONベースの型だ」という意味ですね。x∈t は、「データxが型tに所属するインスタンスだ」と主張しています。

s, t∈T のとき、sやtは集合ですから、s∪t、s∩t が意味を持ちます。また、s⊆t という包含順序を考えることもできます。s∪t = t ⇔ s∩t = s ⇔ s⊆t です。これらのことは、Tが集合束なので当たり前だといえます。

総称型（型パラメータを含む型）は、Tn（n = 0, 1, 2, ...）からTへの関数として解釈します。例えば、項目の型がすべて型tであるリスト（JSONではリストと配列は同義語）を作る関数は List:T→T, t |→ List(t) 、型sと型tのペアを作る関数は Pair:T×T→T, (s, t) |→ Pair(s, t) です。“総称型＝型関数”の引数は習慣として山形括弧で囲むので、List<t>, Pair<s, t> とするのが普通です。0引数の型関数 F:T0→ T, <> |→ F<> は、単なる型（Tの要素）と同一視します。

型関数はいつでも全域とは限りません。例えば、「配列型の最初の要素の型」という型関数はスカラー型に適用できません。一般には、型関数の定義域は、型の集合Tの部分集合ということになります。

型の集合Tの部分集合はカインド（種；kind）と呼びます。カインドは型の集合、あるいは“型の型”です。例えば、「スカラー型」という言葉は、個別のスカラー型（例えばstrig型）を意味するときもありますが、「すべてのスカラー型からなるカインド」という意味で使われることもあります。

「すべてのスカラー型からなるカインド」をSCALARとすると：

  • SCALAR = {t∈T | t⊆Scalar}

ここでは、カインドにこれ以上深入りするのはやめておきます。

ミート付きクリーネ代数

型システムの議論は、JとTがあれば一応はできます。K = Pow(S) = Pow(J*) を考えるのは、正規表現型（regular expression types）を考えたりするときに、JとTの範囲内では不自然となるからです。型の正規表現は、いったんKのなかで解釈して、ブラケティング brk:S→J をKに拡張した Brk:K→T によりTに戻すのが自然です。

Kは、Pow（S)という形なので集合束になっています。つまりKは、クリーネ代数であると同時に分配束の構造も持ちます。クリーネ代数と分配束の定義はWikipediaにも書いてあります（ http://en.wikipedia.org/wiki/Kleene_algebra , http://en.wikipedia.org/wiki/Distributive_lattice ）。

Kにおいては、クリーネ代数の足し算「+」と束のジョイン「∨」は一致しています。新しく導入する演算は束のミート「∧」だけです。それと、定数としてミートの単位元も「∞」必要です。全部まとめると、(K, +, ・, *, ∧, 0, 1, ∞) となります。(K, +, ・, *, 0, 1) でクリーネ代数、(K, +, ∧, 0, ∞) で分配束になっているのです。これがミート付きクリーネ代数*1です。

ここまで説明してきてナンですが、僕は、型システムのモデル（セマンティックス）にミート付きクリーネ代数を使う気はあまりないです。ミート付きクリーネ代数Kの用途は、TをKに埋め込んで考えたり、ArrayとKの同型を利用したりと、どちらかというと計算の道具です。

基本的な型システムはT、総称型を入れるときは Tn→T を素材にするのですが、モデルを考えるには、もっとずっとずっと広い世界を考えないとうまくいきません。広い世界にTやKを入れて、スノーグロープ現象を利用して、外の世界をT内に写し込むような細工をします。外の世界は半環圏（semiringal category）の構造を持ちます。クリーネスターに対応する自己関手も持つので、クリーネ半環圏というべきかもしれません。

なにが問題か

まーともかく、型の集合Tと、Tを含むミート付きクリーネ代数Kが定義できたので、これをもとにした議論ができます。現実的に何が問題なのかというと、ミート付きクリーネ代数の定数 0, 1, ∞ などの実際的な意味です。JSONベースの型システムには、null, void, never, empty, any, undefined などの特殊な型が（場合により暗黙に）含まれます。これらの特殊な型は、ミート付きクリーネ代数の 0, 1, ∞ に対応すると考えられますが、それほど素直に対応するわけではありません。特殊な型をどう定義すべきか、どんな意味を持たせるべきか、演算（合併、連接、クリーネ・スター、共通部分）とどんな関係があるのか、などをハッキリさせたいのです。

なかでも面倒なのは、undefinedの扱いです。undefinedは、ソフトウェアが例外を投げるような事態を表現する値です。「そこに値がないこと」を表す値です。いかにもイヤラシソウなヤツです。しかし、undefinedは必要です。必要なんですが、ヘタに扱うと矛盾を生じます。voidやneverだって矛盾の原因になります。きちんとした意味論のなかで取り扱いを決めないとうまくないのです。

undefined, void, never などは、小さく可愛いようだが、扱いを間違えるとパニックと破綻を招く、ギズモみたいな連中です。こいつらをうまく飼いならす方法は … … あー、また続きだぁー。

*1:クリーネ束と呼ぶ人もいますが、a' を aの補元（complement）として、「a∧a' ≦ b∨b' (Kleene condition)」を満たす束をクリーネ束と言うので、ミート付きクリーネ代数（Kleene algebra with meet）のほうがいいと思います。