Catyの型システムの特異性

Catyの型システムは主流のプログラミング言語にはあまり見られない特徴があり、それのせいで処理系の開発が極端に容易になったり面倒になったりするので、ちょっとそれらの一部をまとめてみる。

未知(undefined)、無効(null)、空(never)が型として存在する 

この三者はそれぞれまったく異なる。

空オブジェクト({})、空の配列([])はいずれもれっきとしたシングルトンであると同時にオブジェクト、配列のインスタンスであり、空集合ではない事に注意。

実際にはundefinedの扱いはいろいろややこしい。

ルーズ配列がある 

以下はCatyの配列として合法なデータである。

[1, 2, 3, ,4, , , 7]

この歯抜けの部分にはundefinedが存在し、理屈の上では配列の終わったと見える後にも無限のundefinedが並んでおり、Catyの配列の長さというのは配列の先頭から最後のundefinedでないデータまでの長さである。

実装する側としては案外面倒。ただ、undefinedの存在を認める以上はこれができないのは不自然とも思える。

型へのタグ付けがある 

単なるstringxというタグを付け、@x stringなどという型を構成できる。このタグ付けされた型は元の型と異なる型として扱われる。これは構造的にはどうしても排他にならない/できないが、しかし明確に別物として扱いたいデータを表現するのに有効である。

実際にはタグ付けという行為は、適当なスカラー型と対象の型をタプリングしたものと概ね同じである。例えば先の例は["x", string]とやってることはほぼ同じで、それをもっとちゃんと体系立てて便利にした感じ。

またタグのみの型もあり、その場合はタグに使われるシングルトンとundefinedの直積だとする。

型の積集合がある 

例えば「fooとbarというプロパティを持つオブジェクト」と「fooとbuzというプロパティを持つオブジェクト」の共通部分は「fooのみを持つオブジェクト」となる。配列も同様。実際にはさらに両者のfooの積集合を取っていき、その結果が新たなオブジェクトのfooの型になる。

この時両者に共通部分がなければ結果は空集合。スキーマ属性の計算で面倒になる部分の代表。

型の直和がある 

「文字列もしくは整数」とか「文字列もしくは文字列の配列」のような型を定義できる。これらはwhen文やcase文でパターンマッチしてそれぞれの成分ごとの処理を行える。Cのunionとは全然違うので、間違っても混同しないように。どっちかっていうとAdaのUnionとかに近い。

厄介なのは型同士の直和が取れるかどうかの判定で、AとBの直和が取れるということはAとBが排他であるということであり、つまりAとBの積集合を取って空集合になればよいということになる。最近までは型同士の排他性は型名及びタグ名で簡単にチェックできたが、次のtype caseを入れてしまったので大変な事になった。

type caseがある 

俺の知る限りではCLOS, Ada, Modula-3にぐらいにしか存在しない。

case {
    integer => ...,
    string => ...,
    {"foo": string, *: any?} => ...,
    null | false => ...,
    * => ...,
}

caseの各分岐は排他でないといけないので(*は最終的にcaseの取る型変数に変換される)、ここでも排他性のチェックが必要になる。というかtype caseを入れるために直和の排他性チェックを面倒にしたのだが。

単一代入 

あらゆる変数は単一代入であり、実行時に未束縛の変数は存在しない。これは珍しくたちの良い部類の性質。

structual subtypingである 

Javaなどのようにクラスの継承やインターフェースの実装などの宣言がなく、同一のプロパティを持ったオブジェクト型や同一の要素の配列型は同じ型、あるいはサブタイプと見做される。確かOCamlなどはこれだったと思う。

nominal subtypingなら単に宣言の親子関係を辿れば良い所を毎度毎度計算するので、これは実装が面倒。duck typingに静的に型を付けているのだから当たり前か。でもこれ一度使っちゃうとやめられないんだよな。例えば複数システム同士の繋がったWeb APIとかのバリデーションにとても便利。他のシステムからの入力も最終的にJSONに変換され、Catyの型システムはJSONの拡張だからできる業でもある。

シングルトン型と列挙型がある 

これは話をややこしくしている。例えばリテラルで1とだけ書いた場合、大抵のプログラミング言語は文脈によるだろうが整数型とか実数型として扱われるものの、Catyの場合リテラルの1の属する最小の型は1であり、当然1|2という列挙型にも属する。同様に1|2|3...と続けていき、その果てにinteger型に属すると言える。当然文字列にもこれは適用されるし、オブジェクトや配列のリテラルも事情は同じ。

インスタンスに型情報がない 

あるインスタンスの属する最小の型は自身のみを含むシングルトン型であり、しかしstructual subtypingなので包含判定によってある型に属しているかが計算される。これは事情が複雑というよりは、最初からそういうシステムだったという話。

というかここから始まった結果、型システムがこうなったというか。

そもそもCatyスクリプトのリテラルは全てコマンド扱いで、例えばCatyスクリプトに1というリテラルを書いた場合、実はそれは入力型がvoid(=入力を捨てる)で出力型が1のコマンド(関数)である。オブジェクトなども同じ。

{
    "foo": 1,
    "bar": "s",
}

この時、{...}という構築子全体の型は{"foo": 1, "bar": "s"}で、例えば以下のスキーマのsubtypeと見做される。

{
    "foo": integer,
    "bar": string,
}

スキーマ属性がある 

スキーマ属性というのは、例えば「空でない文字列(文字列長が1以上)」とか「0から100までの整数」とかいうのを、型レベルで宣言できるということ。

type NEString = string(minLength=1);
type Score = integer(minimum=0, maximum=100);

これまた事情が複雑になり、実装する方は実に面倒。例えばCatyでは型同士の積集合、つまり共通部分を取れるのだが、integerとintegerの共通部分はそれはintegerに決まっているが、integer(maximum100)とinteger(minimum101)の共通部分は存在しない。よってこの二つの共通部分を取ると空集合になる。こんな調子で様々なスキーマ属性が存在する。

Catyにおける型というのは要するに集合なのだが、スキーマ属性を入れた結果、台となる集合と一変数論理式のペアからなる集合になっている。先の二つを集合っぽく書くと、

{s ∈ string | length(s) >= 1 }
{i ∈ integer | 0 <= i <= 100 }

こんな感じ。

任意の高階型を認めていない 

例えば指数型を自由に作ることはできないため、高階関数は書けないという事。仮に高階関数を認めてしまうと、

command foo<S, T, U> :: S -> T -> U

こんなどこのHaskellだよという型が書けてしまうし、当然高階型をプロパティに持つオブジェクトなども作れてしまうし、ちょっと面倒過ぎる。そもそもそこまでの複雑さが必要な処理をCatyスクリプトで書くなというのが、今現在の俺と檜山さんの主張でもある。古いCatyスクリプトで不動点演算子作ってfactrialの計算とかやってた俺が言っても説得力0だが。

ちなみに「任意の高階型」が認められていないだけなので、システムの内部は指数型だらけではある。

更新履歴 

2012-02-10
用語の誤りなどを修正
2012-02-09
用語の誤りなどを修正
2012-02-08
公開