カタカナで書いた「イイカゲン」の意味は、ずぼらでだらしないことですが、本来の「良い加減」つまり「適切」という意味も若干は含んでいます。僕は随分長い期間、僕のようなずぼらでだらしない性格の人に向いていて、それにもかかわらずある種の適切さ、バランスの良さを備えていて、さらに破綻しない程度には首尾一貫している型システムがないものかと探したり考えたりしてきました。
この課題はけっこう難しいもので、よい解答を得るには至っていません。でも、現時点における「こんな感じかな」を記しておこうと思います。
内容：
概念と記法の準備
データとしてJSONデータを考えます。その理由は、JSONは既に多くの人が知っているだろうし、新たに学習する負担もさほどではなく、たいていのプログラミング言語の型システムに埋め込むことができるからです。
xがJSONオブジェクト、pがプロパティ名のとき、x.p によりプロパティ値を表現します。実際のJSONでは、プロパティ名に任意の文字列が使えるので x.p という形式でのプロパティ参照が困難なときもありますが、その点は気にしないことにします。
x.p が定義されているかどうかを調べる関数（述語）を defined として、
- x.p が定義されていて有効な値を持つなら defined(x.p) は真
- そうでないなら defined(x.p) は偽
と約束します。definedを実装しにくいプログラミング言語もあるでしょうが、このdefinedは説明のために使うものと考えてください。
基本データ型として integer, number, string, boolean を採用します（JSONスキーマと同じです）。これらの型の名前は、型を判定する関数（述語）としても使うとします。つまり、integer(x) と書いたら、「xはinteger（整数型）である」という意味です。これまた、説明のために使う略記法と理解してください。基本型以外の任意の型Tについて、T(x) という形を使います。
JSONのオブジェクトリテラル記法をそのまま採用します。{a:x, b:y} のように書いたら、a, b, x, yは変数であり、実際のキー（プロパティ名）や値（プロパティ値）ではありません。a = "name", b = "age", x = "板東トン吉", y = 23 と具体化すると、{"name" : "板東トン吉", "age" : 23} という具体的データになります。
動機と目的
なぜイイカゲンな型システムが欲しいのかというと、そもそもの動機に「データを処理する関数を組み合わせたい」ということがあります。関数を安全に組み合わせるには、関数が扱うデータに型があったほうが都合がいいのです。しかし一方、静的型チェックがないプログラミング言語（僕の場合はErlangやJavaScript）を使っていると、「型なんてめんどくせーや」という自堕落な態度が身体に染み付いてしまいます。
そういうわけで、あんまりうるさいことを言わないユルーイ感じの型システムで、ある程度（多くは望まない）の型安全性を保証してくれるものがないのかなー、と思うわけです。
目標としては、JSONとの相性がよくて、タプル型（直積型）とバリアント型（ユニオン型、直和型）が実現できて、うるさ過ぎない型システムです。単に型だけではなくて、型構成に対応した関数の構成（組み合わせ方）も一緒に考えます。
キー付き型
JSON風オブジェクト（キー／値・ペアのセット）のプロパティ名を以下ではキーと呼ぶことにします。キーとして許される名前（あるいは文字列）の構文は前もって決まっているとします。
aがキーでTが型のとき、a:T も型だとします。例えば、age:integer は型です。JSONのキーは引用符付き文字列ですから、それに忠実に書くと "age":integer ですが、引用符なしの書き方も許すことにしましょう（そうでないと煩雑なので）。age:integer（正確には "age":integer）のインスタンスは {"age": 整数値, 他になにかあるかも} というパターンのオブジェクトです。例えば、{"age": 23, "name": "板東トン吉" } とか。
もう少し正確に書くと：
- x が a:T に含まれるインスタンであるとは、defined(x.a) かつ T(x.a) 。
T(x.a)は、「x.a の型が T である」ことです。xに、a以外のキー（プロパティ）があっても別にかまいません（ここらがユルイところ）。
キー付きタプル型
aとbが異なる2つのキー、S, Tが既に定義された型（SとTが同じでもよい）のとき、a:S∧b:T という新しい型を次のように定義します； x が a:S∧b:T に含まれるインスタンであるとは、次が両方とも成立することです：
- defined(x.a) かつ S(x.a)
- defined(x.b) かつ T(x.b)
例えば、{"age": 23, "name": "板東トン吉"} は age:integer∧name:string 型のインスタンスです。
このスタイルの型構成は、n個の異なるキー a1, ..., an とn個の型 T1, ..., Tn に対して一般化できて、x が a1:T1∧ ... ∧an:Tn に含まれるインスタンであるとは、次がすべて成立することです：
- defined(x.a1) かつ T1(x.a1)
- ...
- defined(x.an) かつ Tn(x.an)
例えば、age:integer∧name:string∧male:boolean という型が定義できます。
キー付きバリアント型
キー付きタプル型と同様な考え方でキー付きバリアント型を定義できます。論理アンド「∧」を論理オア「∨」に置き換えるだけです。
n個の異なるキー a1, ..., an とn個の型 T1, ..., Tn に対して、x が a1:T1∨ ... ∨an:Tn に含まれるインスタンであるとは、次のうち少なくとも1つが成立することです：
- defined(x.a1) かつ T1(x.a1)
- ...
- defined(x.an) かつ T1(x.an)
理論上は、a:S∨b:T と b:T∨a:S は同じ型であと考えるべきですが、実際の処理では順序の影響を受けてしまい、a:S∨b:T と b:T∨a:S をまったく同じとはみなせません。まー、このあたりもうるさくは言わないことにします。
キーによるガードとマーク
以下、f, gなどは1引数の関数だとします。S, Tが型のとき、f :: S→T の意味は次のとおりです。
- fは仕様上S型のデータを受け取ることになっており、S型のデータを受け取れば間違いなくT型のデータを出力する。
S型に含まれないデータインスタンスを受け取ったときの挙動は未定義で、なにが起きても文句は言えないと約束します。コロンを2つ「::」にしたのは、既にキー付き型でコロンを使っているからです。
aがキー、f :: S→T のとき、f@s :: a:S→T は次のような関数です。
- xが 型a:Sに含まれとき、f(x.a) を出力する
- そうでないときは未定義（ランタイムエラーと思ってよい）
例えば、fが(integer→boolean)型の関数のとき、f@age は age:integer型のデータを受け取ります。(f@age)({"age": 23, "name": "板東トン吉"}) = f(23) となります。f@a を、fをキーaによりガードした関数と呼ぶことにします。
bがキー、f :: S→T のとき、b:f :: S→b:T は次のような関数です。
- xが型Sに含まれるとき、{b:f(x)} を出力する
例えば、fが (x:integer∧y:integer)→integer 型の関数のとき、新しい関数 norm:f は、(norm:f)({"x":10, "y":4}) = {"norm":f({"x":10, "y":4})} のように定義されます。b:f を、fをキーbによりマークした関数と呼ぶことにします。
ガードを付ける操作とマークを付ける操作は交換可能で、b:(f@a) と (b:f)@a は同じ関数です。これを b:f@a と書きましょう。
関数のキー付きタプル
a, bがキーで、f :: S→T, g :: S→U が関数（関数はどれも1引数だとする）のとき、{a:f, b:g} という新しい関数を定義します。{a:f, b:g} という書き方は、JSONのオブジェクトリテラルと同じですが、データではなくて関数を表すことに注意してください。
- {a:f, b:g}(x) = {a:f(x), b:g(x)}
これを、関数f, gのキー付きタプルと呼ぶことにします。なんか当たり前に見えてかえって分かりにくいかも。実例を出しましょう。tを時間（秒単位）変数だと思って、三角関数
- cos(2*PI*t)
- sin(2*PI*t)
で表される2つの関数から、キー"x", "y"によりキー付きタプルを作ると、単位円を1秒で1周する円運動になります。JavaScriptで書いてみます。
function circular(t) { return {"x":Math.cos(2*Math.PI*t), "y":Math.sin(2*Math.PI*t)}; }
2つの関数f, gの引数の型が一致するときにだけ {a:f, b:g} が定義可能な点に注意してください。3つ以上のキーと3つ以上の関数に対しても同様な構成が定義できます。
関数のキー付きバリアント
a, bがキーで、f :: S→U, g :: T→U が関数のとき、[f@a, g@b] という新しい関数を次のように定義します。
- xの型がa:S のとき [f@a, g@b] = f@a
- xの型がb:T のとき [f@a, g@b] = g@b
これは一種のcase文です。[f@a, g@b] を擬似コードで書いてみると：
case x in a:S then f@a(x) x in b:T then g@b(x) end
JavaScriptなら：
// a, b はキーを表す変数 if (x[a]) { return f(x[a]); } else if (x[b]) { return g(x[b]); } else { throw "error"; }
2つの関数f, gの戻り値の型が一致するときにだけ [f@a, g@b] が定義可能な点に注意してください。3つ以上のキーと3つ以上の関数に対しても同様な構成が定義できます。
圏論的な考察
これら、関数の構成法（組み立て方）の背景には圏論があります。しかし、型システムとしてみた圏論は静的で極めて強い型付けを要求します。全然ユルイ型システムじゃなくて、やたらにキビシイ型システムです。そういう事情で、本来のキビシイ圏論ではなくてユルイ圏論風の議論を採用します。
関数fの引数の型をDom(f)、戻り値の型をCod(f)と書くことにします。例えば、Dom(f) = integer、Cod(f) = boolean ならば、f :: integer→boolean と書いても同じです。圏論では、Cod(f) = Dom(g) のときだけ結合（関数合成； composition）が可能ですが、この結合可能性の条件をゆるめて、Cod(f) ⊆ Dom(g) なら結合してもよいとします。（定式化）
記号「⊆」は、データ型の包含関係ですが、型に属するインスタンス集合の包含関係と捉えていいでしょう。例えば、
- integer ⊆ numeber
- age:integer∧name:string ⊆ age:integer
- userId:integer ⊆ userId:integer∨handle:string
などが成立しています。「∧」と「∨」は論理記号を拝借したので、同じように論理記号を使うなら「⊆」よりは「⊃」がふさわしいのですが、まーイイカゲン主義だから、こだわらないことにします。
関数のキー付きタプルとキー付きバリアントに関して、次が成立します。
- Cod({a:f, b:g}) = a:Cod(f)∧b:Cod(g}
- Dom([f@a, g@b]) = a:Cod(f)∨b:Cod(g}
Cod(f) ⊆ Dom(g) のときの結合を f;g と書くことにすると、次も成立します。
- Dom(f;g) = Dom(f)
- Cod(f;g) = Cod(g)
Cが直積と直和を持つような圏のとき*1、B⊆|C| から直積と直和により生成されたCの部分圏をDとすると、Bを基本型とするJSON風データの領域にDを埋め込むことができます。直積をキー付きタプル型に、直和をキー付きバリアント型に対応させるのです。関数のキー付きタプル構成とキー付きバリアント構成は、それぞれデカルト・ペアリングと余デカルト・余ペアリング*2に対応します。キーの選び方が任意ですから、埋め込みは一意的ではないし、たくさんの埋め込みが混じり合ったような状況になりますが、実用上はたいした問題も不便もないでしょう。
目論見
基本的な型から、キー付きタプル構成／キー付きバリアント構成で組み立てられた型S, Tに関して、S ⊆ T（論理記号を使うなら S ⊃ T）の判断はさほど難しくないでしょう。とすると、2つの関数の結合可能性も判断可能です。関数のDom、Codは計算できるので、与えられた式（関数の組み合わせ）が、ユルイ型システムから見て妥当であるかどうかも検証できるでしょう。
テンプレートに渡すコンテキストデータをパイプライン（チェーン）処理で作り出すときなどは、このような検証がけっこう有効なのではないかと考えています。型の定義にはJSONスキーマ（またはその変種）が使えます。
