2023 03 29 - qnighy/umo GitHub Wiki

近況

VMを少し進めた。

nominal typing と structural subtyping を組み合わせる

Rustはnominal typingで部分型を持たない。一方TypeScriptはstructural subtypingを採用している。両者はそれぞれの利点を上手に引き出している。

  • Rustのnominal typingは型を単なる性質以上のものとして使うために大いに役に立っている (Church-style typing)
    • たとえばレシーバーの型にもとづいてトレイトとメソッドが選択される
  • またRustのtypingは部分型を持たない(※正確に言うと、ライフタイムに関する部分型しか持たない)ため、型推論のヒューリスティックスが比較的少なく、安定的に動作する。
  • TypeScriptはsubtypingを持つことによって言語の表現力を大きく増している。特に、束構造を活かした表現ができることでRustでは難しいようなユースケースにも対応できている。
    • ASTの表現などではよく大きなADTが必要になるが、そのバリアントの任意の組み合わせを型として表現できる。
    • DBから取得したレコードを表すための型。ロジックが複雑になると、はじめに取得したレコードを複数のヘルパー関数に渡すようなシチュエーションが出てくる。このとき、各ヘルパーが要求するカラムは異なるかもしれない。すると、各ヘルパーはそれぞれに自身が要求するカラムを型として表現し、DBから取得するときも利用可能なカラムを型として表現したくなる。これもまた束構造であり、部分型がないとかなり迂遠な表現にならざるを得ない。

当然、これらを止揚して最強の型システムを考えてみたくなるというもの。

さて、上の例ではTypeScriptがsubtypingを持つことの強みを伸べたが、実はここで想定した事例はいずれも上界がはっきりしている。ASTの表現であればベースとなるNode型があるはずだし、DBであればベースとなるFooRecord型があるはずで、それより大きなunionを取る必要は原則としてない。正確に言うと null や undefined が例外的に出現することはあるが、これはOptionで置き換えられる。

ということは、決まったベース型の中でのsubtypingのみを考えて、それらのベース型自身はnominalに判定されるような型システムにすれば、もしかしたら両者のいいとこ取りができるのでは？ という気がしてくる。

…… といっても、実はこのシステムは篩型システムに他ならない。

ただ、篩型といっても、 { n: Int | n >= 0 } のように複雑な条件式を扱う必要はない。上のユースケースを考えてみると、これらはいくつかのアトミックな述語のboolean combinationだけでも何とかなりそうだし、それは要するにTypeScriptでいうところの & や | で表現されているものと同等ということになる。これなら人間にとってもコンパイラにとっても難しすぎない範囲内で扱える余地は…… 多少はあるのではないだろうか？

ちょうどいい篩型

さて、この制限された篩型システムの利点を最大限に活かすには何が必要だろうか？ まず、Rustの型がnominalでnon-subtypedであることによる恩恵を逃すわけにはいかない。これは以下のような制約で表されるのではないかと思う。

  • ベース型の型推論はベース型だけで完結する。

つまりベース型の型推論と篩型の型推論の相互依存を断ち切りたい。

さてこの制約はどのような場面で出てくるかというと、基本的には同じベース型でのオーバーロードは同じベース型しか返せないという形で登場するだろう。たとえば、TypeScriptで

function save(isBinary: false): string;
function save(isBinary: true): Uint8Array;

というシグネチャは同じ boolean というベース型に対して異なる戻り値を与えているが、これはベース型の型推論がベース型で完結しない。また、

type Node =
    { type: "add", lhs: Node, rhs: Node }
  | { type: "dot", lhs: Node, rhs: string };

というシグネチャは rhs のベース型がバリアントごとに異なるからこれも困る。

逆に言えば、このようないくつかの(それほど窮屈ではない)制約を課せば、うまく具合に篩型の良いところを取ってこれる可能性があるということになる。気がする。

また述語は基本的にアトミックなものの組み合わせとして考えたい。 (上級者向け機能としてより複雑な述語 --- たとえば n >= 0 --- を考える余地はあるかもしれないが、基本機能としてはアトミックなものを考えたい)

述語

アトミックな述語は以下の2つに分けられそう:

  • 透過的な述語。これはADTのバリアントに由来する。
  • 非透過的な述語。これはいわゆるnewtypeの亜種で、仮にnewsubtypeとでも呼んでおく。たとえば、 newsubtype str = [u8]; であれば、述語の具体的な内容は指定せず、 [u8] の部分型である str を定義するということになる。
    • この場合、 str 自体の可視性とは別に、 [u8] を str にキャストする能力 (述語のアサーション) に対する可視性が定義されることになる。

ADTのバリアントに由来する述語として例えば次のような例がある。

type Node =
  | { type: "Add", lhs: Node, rhs: Node }
  | { type: "Sub", lhs: Node, rhs: Node }
  | { type: "Macro", args: Node[] };

type ExpandedNode = Extract<{ type: "Add" | "Sub" }, Node>;

この場合、マクロ展開後のASTからはMacro nodeは消滅しているはずで、それを表現している。

ただ、いきなり最初の例で原則を破るのもアレだが、この例では本当は再帰的に述語を適用したい。

そんなわけで、実際には単なるatomic predicateのboolean combinationという枠をはみ出て、再帰的な述語に対してもある程度のサポートをしたくなりそうかなと思っている。

ADTはどうなる

RustとTypeScriptはADTに対して異なるアプローチを取っている。先ほどのNodeの例を考えたい。

type Node =
  | { type: "Add", lhs: Node, rhs: Node }
  | { type: "Sub", lhs: Node, rhs: Node }
  | { type: "Macro", args: Node[] };

この場合 Node はtagged unionと呼ばれ、実態はunionにすぎず、それぞれのプロパティはstructuralに比較される。たとえば以下のように複数のバリアントにまたがるプロパティをまとめて取得できたりする。

if (node.type === "Add" || node.type === "Sub") {
  return node.lhs;
}

バリアントをstructural subtypingの仕組みに統合するのであれば、こちらの方式のほうが自然で利便性も高いのでは？ という気がしている。

そうすると、Rustで面倒な気持ちになりがちなstruct-enumパターンもはじめから1個の宣言で書ける。

algebraic struct Node {
  // 共通フィールド
  loc: Location,
  // 各バリアントごとのフィールド
  variant Add {
    lhs: Node,
    rhs: Node,
  }
  variant Sub {
    lhs: Node,
    rhs: Node,
  }
  variant Macro {
    args: Node[],
  }
}

しかしこの場合、variant tagとは一体何者なのか？ なぜstructに対してvariant tagは1個なのか？ 別に複数あってもいいのでは？ みたいなところの疑念も解決する必要が出てきそうだ。

flow type 超面倒くさい問題

こういう形式のsubtypingをやり始めるとtype stateとかflow typeとか、時系列で型が変わるようなタイプの構成が欲しくなってくるし、実際TypeScriptはそれを持っている。

だいたい予想がつくところだが、これは超面倒くさい。TypeScriptはサボっている。

たとえば以下のコードを考える。

let x = 42;
something(() => {
  x = "foo";
});
const y = x;

y の型はなんだろうか？ それは something の挙動によって異なる…… というのが本来あるべき姿だが、TypeScriptはoptimistic type narrowingといって適当にクロージャの呼び出しタイミングに対して仮定を置いて推論してしまう。

まあTypeScriptならそれは許されてしまうが、正しくはないので何とかする必要がある。

さいわい現代の言語ではライフタイムみたいな難しいことをやっても許されるので、おおむねそれに便乗する形になるだろう。