Desk言語の再現手順書

自分以外の方が一からDesk言語を再現できるように言語の要件と構築方法を書いてみました。手順書の通りに定義もしくは実装をいくらか進めていただくとDesk言語のサブセットを作ることができます。全てのステップを終えることで現時点での完全なDesk言語が構築できます。

仕様書の草稿という体で書かれていますが、形式的な推論規則などが今は添付されていないため、作られたものによってコーナーケースでのセマンティクスなどに差異は出ると思います。しかしこの記事で書かれていることが実現されているのであればそれは１つの目的を共有した、いわばドッペルゲンガーのようなものであり、少なくともDesk言語の1フレーバーであると言えます。フレーバー同士での研鑚が十分に進んだのちにもっと具体的かつ形式的で完全に近いDesk言語仕様書の共同執筆が行われると良いのではないかと考えています。
詳細な説明はできていないので論文におけるAbstractのようなものだとご理解ください。それでもプログラミング言語の理論を踏まえた上でこれを読めばすぐに実装し始められる内容にはなっていると思います。参考になれば嬉しいです。

ちなみにわたしが今実装しているDesk言語処理系の立ち位置は参照実装というよりも「プログラミングの大衆化」という目的だけに特化した一つのフレーバーみたいなものであり、具体的には、簡単に購入できる価格帯のタブレットやラップトップのWebブラウザ上でエディタやコンパイラやファイルシステムが統合された環境が軽量に実行できることを目指しています。
また、古い仕様のままのものがまだかなり残っているため実際のところ真のDesk言語実装からは距離がある状態です。

あと肝心の型システムですがわたしの実装はComplete and Easy Bidirectional Typechecking for Higher-Rank Polymorphismという論文で形式定義されているCompleteかつSoundな双方向型付けアルゴリズムの推論規則をそのまま実装し、それをベースにしていわゆる代数的効果やユニオン型等の拡張を進めています。この型システムを使うことに必然性はなく、私がサーベイした結果、とりあえずこれを使うのが最もやりやすいだろうという感じただけです。

この文章の著作権はわたしにありますが、その内容であるところの言語仕様についてはパブリックドメインなどにする可能性があります。というよりも放棄するための著作権が手元にない（すでにパブリックドメインである）ような個人的な感覚があります。

それでは以下、なんちゃって仕様書的な手順書です。

ステータス

安定化されるまではこの仕様書の内容は常に変わる可能性がある。安定化以後には適切なバージョニングを伴って変更が行われる。
重大な問題がない限り、以前のバージョンが非推奨になることはないが、エコシステムの健全な発展のためにも最新バージョンへの移行を常に推奨する。

標準化しないもの

以下に挙げるものついてはDesk言語仕様にとってはtrivialなものであるため定義しないが、本仕様書の外側でデファクトのような定義があってもよく、それは単純・軽量・自己完結を指向するのが望ましい。

• 文法
• ASTや中間表現などのデータ構造
• その他コンパイラの実装の詳細
• ファイル形式やモジュール・依存関係等の表現方法など
• ビルトイン関数やビルトイン効果

しかし、文法がなにもなくては定義や具体例の提示が不可能であるため、ここでは簡易的な仮想の文法を用いる。
また、Desk言語では構文の少なさに重きを置いているため、高級言語的な利用やリッチな表現のためにはマクロが不可欠となる。そのためにS式のようなデータ構造に一意に変換可能な文法である必要がある。

（もし数式のように抽象性が高く曖昧性が排除された文法がお好みであればこちらのLL1文法定義をほとんどそのままお使いいただけます）

Desk言語の基本事項

以下のリストの項目に違反しないように言語構築を進める。違反した時点でそれは全くの別言語である。
ただし、低レベルな表現やランタイム等については、高レベルのセマンティクスに違反しないかつユーザーの意図しない損害をもたらさない限りにおいてはなにも禁止されない。
また、後に続く2つ条件を満たし続ける限りにおいて、最適化などのユーザーの要求を理由に低レベルでの言語のセマンティクスの逸脱が許される; 1. 名前やshort descriptionのようなユーザーが普段から目にする象徴的なものの中で、「unsafe」のような比喩なく端的に安全でないことを示す言葉を用いて、明瞭に非安全性を明示する; 2. セマンティクスの逸脱が発生する全ての条件とそれにより引き起こされうる問題について分かりやすく列挙した情報をユーザーが簡単に見つけられる方法で提供する。

• 全ての構文が式である
• 特定の例外的な型かエフェクトを用いない限りあらゆる式が純粋である
• エフェクトを用いたとしても網羅的にハンドルされていれば全体としては純粋な式である
• 特定の例外的な型を除きイミュータブルデータである
• 関数適用時や型コンストラクト時などは全てコピーセマンティクスである
• 正格評価を基本として、S式的なリストデータの並び順で遅延なく逐次評価する
• 型システムはstate-of-the-artな型推論と厳格な型検査を行う
• 構造的かつ推移的なサブタイピングが行われる
• サブタイピングによる型強制が可能な全ての場所で暗黙に行われ、型システムにより報告される
• 慣習とされるようなものであったとしても余分なサブタイピングの追加は禁止される
• 構文上に現れるユーザーによる識別子は以降の場合のみを目的とし限定される; 1. ユーザーがデータ構造を説明的にしたい場合に用いる型ラベル; 2. 同じ型のものを同時に複数扱うのが不可能な場合に用いる型ラベル; 3. 再帰型の表現のための型レベルlet式に用いる識別子; 4. Π構文・Σ構文において複数の場所で同じ型を用いたい場合に用いる型変数。
• 識別子に文字列を用いる場合、自然言語による柔軟な識別を阻害しない（予約キーワードがなく、例えば"This is a pen."がそのまま簡単に識別子として使用できる）
• 一つの言語機能に対して機能の重複する構文や本仕様書に定義された言語機能に関連しない構文を持たない
• 純粋なデータを表現するプリミティブ型を除き、本仕様で定義されたもの以外の組み込み型を持たない

0. 単純型付きラムダ計算的な何か

• λ <type> → <expr> -- 常にただ一つの引数を取る。varianceに基づき安全にサブタイピングされる
• apply <type> <0 or more exprs> -- 型名が示すカリー化された関数に複数の引数を渡す。引数が0個の場合は型名が示す値や関数がコピーされ評価される。そのスコープから参照可能で型名が完全一致する関数や値が使用され、見つからない場合は評価ができない。原則完全一致であるが、例外的にΠ構文を使った式の総積の中から完全一致する式を取り出しても良く、その操作は何度行っても良い

1. 集合論的な代数的効果

• perform <expr> ~> <type> -- 式を入力とするエフェクトを発火し、ハンドラーが継続時に渡す<type>の値に評価される
• handle <expr> <handlers> -- 式全体の型は対象の式の型と各ハンドラー式の型の総和に推論される

上のだけだと情報量がほぼゼロなのでもっと説明を書きたいのですが、必要なことは全てこちらの記事に書かれており、この内容のセマンティクスを率直に推論規則みたいなものに書き起こして、そこから実装に落とし込んだ感じです。

2.（集合的な）代数的データ型

• 型名がタグのレコード型: 唯一のコンストラクタ構文を持ちreflexive, symmetric, transitiveにサブタイピングが行われる。特に同じ型がコンストラクタ中に複数ある場合、S式の構造中で最も後ろにある値が使用される。空のときトップ型。サブタイピングのやり方が複数ある場合は最も変換距離が最も小さい唯一のものを選び、そうでない場合は型エラー
• 型名がタグの直和型: コンストラクタ構文を持たず、reflexive, symmetric, transitiveなサブタイピングが行われる。いわゆるユニオン型であり空のときボトム型。サブタイピングのやり方が複数ある場合はレコードと同様

3. 多相・項依存型・型依存型

• Σ構文: 項または型ファミリーの集合的総和
• Π構文: 項または型ファミリーの集合的総積

他の言語でいう Πx: Type. F(x)はΠ F(Type)と書く。

4. 準プリミティブ

• 型アノテーション: 主に明示的な型キャストにもちいる
• 型ラベル: 同じ型を同時に複数扱う場合に区別するためのタグ。ラベルを付ける方にも外す方にもサブタイピングできる。項でラベルを指定するとそれがそのまま型に反映されるため一種の項依存型である（文字列と対象の型の直積のようなもの）。
• let <expr> in <expr> -- スコープを作りスコープに閉じた定義を作る
• let <ident> = <type> in <type> -- 再帰型の表現に用いる

5. 制御構文

• branch式: 直和な式を型で分岐する。網羅性チェックが必須。各ブランチの式の型の総和に推論される

6. メタプログラミング

• AST型（各式を直積で表現した型の総和。他のフレーバーと共有した直積表現を用いるのが望ましい）を出力にもつ関数を型推論や評価より以前にASTのデータ構造の中でマクロ関数の実行結果をそのまま展開する（いわゆる衛生マクロではない）
• アトリビュート構文: 任意の式に対してセマンティクスとは一切の関係のないDson（Desk言語のサブセットであるObject Notation）を付与することができる。マクロ関数やエディタ支援に活用する

7. 組み込みのプリミティブ型

• nat <: int <: rat <: real となるように各数値型を定義
• text型
• vector型: 特定の例外的な型が使われない限り、内部型についてcovarianceでサブタイピングできる
• map型: いわゆるdictionary。関数と似たようなサブタイピングが行われる

オーバーフローやNaNやinfや負のゼロなどの状態は上記の数値型の値としては含まれない。それらの状況が発生する場合は直和型やエフェクトで表現する。

8. 参照型（例外的な非純粋型）

• ref型: ガベージコレクションされるイミュータブル参照データ
• mut型: ガベージコレクションされ排他ロックで読み書きする参照データ

9. 低レベルプログラミングに必要な依存型たち

• bits型: nビットinteger。Coherent性の維持に気をつけながらサブタイピングを定義する。要するにunsigned n bits <: signed n + 1 bits
• 固定長Vector型: Vector型の部分型

10. その他あると便利なもの

• コメント: 任意の式の直前に任意の個数のコメント、式中の文のような機能を持つ要素（let構文や後述のdo構文の前半）の直後に一つのコメントを書くことができる。セマンティクスには一切関係なく、マクロの入力には含まれない。
• infer型: 型を書く際に具体的な型を書かずにinfer型という特殊なものを使うことができる。型システムで推論された型に置き換えたセマンティクスとなる。推論が不可能な場合は型エラー
• hole構文: 式や型の代わりにholeと呼ばれるものを書くことができる。holeがある限りは評価は不可能であるが、パースは可能であり、holeとは関係ない部分の型推論や型チェックも行うことができる
• brand型: 特定の式の中の特定の識別子の型ラベルについて、ラベルをつける方のサブタイピング規則を省いたかたちの型推論・型検査を行う。
• do構文: 推測が暗号的に不可能な型ラベルが値に暗黙に付与されるようなlet構文と等価である。エフェクトを発火するしてその出力を無視する場合に使用される。その場合でもletと同じセマンティクスで値を評価する。
• バージョン指定子: 関数適用構文で関数の型とともにUUIDによるバージョン等を指定することができる。評価を行う際に型が合致するかつ同じUUIDが紐付く実装を使用する。UUIDが一致しない場合は評価不可能。マクロの入力に含まれる