このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」（http://d.hatena.ne.jp/m-hiyama-memo/）のデータを移行・保存したものであり、今後（2019年1月以降）更新の予定はありません。

今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。

Catyの型システムとサイト自動生成 (1)

Caty プログラム意味論

サイトの自動生成とは何であるかを説明する前に、それを表す記号をaと決めておく。autoからa。

aは写像（関数）であり、

  • a: サイトの仕様 → 実際のサイト

となる。サイトの仕様はスキーマ（Catyのcasmとcara、いずれcambも）で与えられ、実際のサイトはアクションと状態（画面、ページ）の集まりとなる。サイトのグラフ構造はハイパーリンクグラフで視覚化される。アクションのアルゴリズム部分は忘れて表示だけを考える。すると、「状態＝画面＝ページ」だけを考えることになる。画面／ページは、テンプレートで生成されるから、「実際のサイト＝テンプレートの集まり」と単純化する。

サイトの仕様とは、スキーマのことだが、スキーマは型の集まりを定義する。結局、

  • a: 型の集まり → テンプレートの集まり

型全体の集合をType、テンプレート全体の集合をTemplとすると（後で記号法を少し変えるが）、

  • a: Type → Templ

となる。ただし、aはType全域で定義される必要はないので、部分写像である。計算科学で出てくる写像（関数）はほとんどの場合は部分写像なので、いちいちその旨を断らないこともあるので注意。

以下では、a: Type → Templ （部分写像）をどう定義するかを述べる。この機会に、背景もテキトーにまとめておく。

後から書いた注意

大文字エックス（X）、小文字エックス（x）、掛け算記号（×）が区別しにくいな。文字を変えれば良かったが、直す気力が無いのでソノママ。よく注意して識別してくださいな。

指数型と配列型を同じ記号にしたのも悔やまれる。これも注意してね。

Catyの大域モデル圏と局所モデル構造

本編の http://d.hatena.ne.jp/m-hiyama/20120302/1330676182 が事前知識。以下、一般的な背景を述べる。

大域計算モデルは圏Cで：

  1. 圏Cは、掛け算「×」と足し算「+」を持つ半環圏である。
  2. 圏Cの掛け算「×」の部分はデカルト圏となる。
  3. 圏Cの足し算「+」の部分は余デカルト圏となる。
  4. 圏Cはデカルト閉構造を持たない。
  5. しかし、いくつかの部分閉構造を許容する。http://d.hatena.ne.jp/m-hiyama/20110115/1295075311 参照。

局所計算モデルは、特定の対象U∈|C| の上に作られる。Uは普遍領域（univ）と呼ばれる。

  1. Cの任意の対象は、U上のPER（Partial Equivalnece Relation, settoid）で表現可能である。
  2. Cの対象Xに対して、U上のPER（の商集合）との同型が1つずつ割り当てられている。
  3. 対象XのPERの同値関係がU上のイコールのとき、X（に割り当てられている同型）は非退化と呼ぶ。
  4. 非退化なXは、Uの部分集合と考えてよい。
  5. 退化するX（非退化でないX）も、U→X という部分全射を持つ。この全射のセクションを正規形と呼ぶ。正規形が定まっているのが望ましいが必須ではない。

Cの対象に対応するU上のPERを、型と呼ぶ。型の全体をTypeと書く。定義より、|C| はTypeに埋め込まれる。また、非退化な型だけを考えれば、Type ⊆ Pow(U) となる。圏Cでは、対象Uに関してスノーグローブ現象が起きていることに注意。

Catyの型には、バッグ型のような退化する型もあるが、話を単純化するために非退化な型だけを考えることにする。したがって、T∈Type ⇒ T⊆U 。

局所モデルもっと

  1. Uを普遍データ領域と呼ぶ。
  2. Uの要素をインスタンスデータと呼ぶ。単にインスタンス、単にデータとも呼ぶ。
  3. Uの部分集合で型表現（type expression）で定義可能なものを型（の集合）と呼ぶ。
  4. Tが型である ⇔ T∈Type であり、Type⊆Pow(U) 。
  5. 型定数は、Typeの要素、または 1→Type の写像のことである（どっちでも同じ）。
  6. 型関数は、Type→Type、Type×Type→Type、… などの部分写像である。
  7. スキーマ（の型定義部分）は、名前が付いた型の集合を定義する。つまり、Nを名前の集合として、N→Type という写像を定義する。同じ型を異なる名前で指せるので、単射とは限らない。
  8. アンビエント（の型定義部分）は、いくつかのスキーマが定義する写像を寄せ集めた構造を持つ。アンビエント（の型定義部分）もまた、名前から型への写像である。

型関数（型演算）として、タプリングや排他的ユニオンなど（その他いっぱい http://d.hatena.ne.jp/m-hiyama-memo/20110510/1305003789）があるが、指数型（ベキ型、関数型）を作ることはできない。XとYの指数 X->Y は型ではなくてIOプロファイルと呼ばれる。IOプロファイル X->Y の意味は、モデル圏Cのホムセット C(X, Y) で、宣言 f::X->Y は、f∈C(X, Y) を意味する。

コマンド

大域モデル圏Cの射がコマンドだが、コマンドはパタメータを持つので、正確に定義したかったら多圏モデルとなる。

ストレージアクセスなどの副作用を扱うには、基本モデル圏Cをモナド類似物で拡張しなくてはならない。多圏モデル（あるいはシーケント計算）とモナド類似拡張をどう折り合いを付けるかは、まだ完全には解決してないが、インデックス圏に対するクライスリ類似構成をすれば良さそう。

曖昧な話だから、この話題はオシマイ。

デカルト閉構造

モデル圏Cはデカルト閉圏ではない。が、完全なデカルト閉圏Dがあって、Cはデカルト閉なDの部分圏と考えることができる。ではなぜ最初からDで考えないのか？ CatyScriptを高階と多相を扱える立派な言語にする気がまったくないから。

とはいえ、言語処理系の実装では、Dに属する概念が出てくる。デカルト閉圏Dを持ちださないで実装を語るのは難しい。Dにおける指数演算を [X, Y] と書く。この記法は、Catyの配列型と同じなので混乱に注意。[X->Y] とか YX を使うといいが、メンドクサイ。|C|に関数型はないので、X, Y∈|C| でも、[X, Y] は|C|に入らないので、|D|内でしか意味がない。

デカルト閉圏Dの評価射をevとする。evX,Y:X×[X, Y]→Y in D となる。evはホンモノのインタプリタ（実行エンジン）を意味し、実装上の概念となる。指数型 [X, Y] の要素は、CatyScriptコードのコンパイル済みデータとなる。入力としてXのインスタンスを与えれば評価可能で、出力（評価結果）は型Yのインスタンスとなる。

例外や無限走行などの異常事態を表す値を⊥とする。テキスト（文字列と言っても同じ）データの型をTextとする。Catyのコマンドevalは、U×Text -> U というプロファイルを持つ。evalは、Textをスクリプトコードとみなして評価するコマンド。失敗する可能性を明示的に書けば、eval : U×Text -> (U | ⊥) となる。Catyの宣言構文なら（ここでは、[, ]は配列型！）、eval :: [univ, string] -> univ throws Exception; （Exceptionはもっと特殊化したほうがいいけど）。

スクリプトコード（テキスト）をコンパイルする関数は（今度の[, ]は指数）、compileX,Y: Text → ([X, Y] | ⊥) となる。コンパイルの失敗（⊥）が起きないようにするなら、ScriptTextX,Yを正しいスクリプトコードの集合として、compileX,Y: ScriptTextX,Y → [X, Y] とすればよい。

コマンドevalを型総称化（多相化）すると（次の[, ]は配列だーー）、eval<X, Y> :: [X, ScriptText<X, Y>] -> Y となる。この eval<X, Y>（evalX,Yとも書く）は、コンパイラとインタプリタを使って次のように書ける。

  • evalX,Y(x, s) := evX,Y(x, compileX,Y(s)) Compile and Go!

s∈ScriptTextX,Y であるかどうかの判定は、パーザー（構文解析系）と型解析系で行える。なので、compileX,Y は、パージングと型解析が済んだ後の純粋なコード生成系とみなせる。実際の言語処理系では、s∈ScriptTextX,Y の判定とコード生成はそれほどスッキリ分離しない。

テンプレート言語のデカルト閉構造

コンテキストの型がXであるテンプレートコードのテキストの集合を TemplTextX とする。TemplTextX もテキストの集合なので、TemplTextX⊆Text 。

テンプレート展開を行うコマンドを expand として、型総称化して expand<X> または expandX と書くことにする。

  • expandX : X×TemplTextX → Text

expandコマンドのエンジンとして、evalのエンジンであるevを使うことにする。compileX,Y: ScriptTextX,Y → [X, Y] と同様に考えて、

  • templcompileX: TemplTextX → [X, Text]

となる。よって、expandの定義は、

  • expandX(x, t) := evX,Text(x, templcompileX(t))

t∈TemplTextX の判定は、テンプレートパーザーと型解析系が行う。

templcompileXは、[X, Text] を直接吐くが、TemplTextX → ScriptTextX,Text のテキストレベル・トランスレータを準備してもよい。このときは、

  • templcompileX(t) := compileX,Text(translateX(t))

となる。

いずれの方法でも、構文処理だけを準備すれば、型解析と実行はスクリプトとテンプレートで共通のモノを使える。


続きは (2)。