この記事は 言語実装 Advent Calendar 2017 7日目の記事です。

この記事では、私が作っているDSLの設計思想を主に書きます（実装が未完なので）。

以前、 複素関数で遊ぼう というWebアプリ（と言ってもサーバー側で状態を持たないのでほぼブラウザーアプリ）を作りました。このアプリでは、複素関数を表す数式をユーザーが任意に入力できます。

例：exp(z)

例：\sum_{n=1}^{10} z^n/n!

数式はHaskellで書いたパーサーで解釈し、JavaScriptへコンパイルしています。コンパイルしたJavaScriptはブラウザー側で実行させます。

関数のグラフを描くためには値を大量に計算する必要があるため、与えられた関数に対してなるべく効率の良いコードを生成することが一つの目標になります。

課題1：静的型をつけたい

対象が複素関数なので、扱う値というのは基本的には複素数なわけです。しかし、一部の演算に関しては、整数に対してのみ定義され、任意の複素数を渡すことはできません。

例えば、階乗や二項係数は整数（自然数）について定義されます（ガンマ関数を使えば複素数に拡張できますが、それは置いておきます）。

また、総和をとる範囲の上端と下端というのは整数であってほしいものです。

そういうわけで、式に静的な型を割り当て、型検査を行うことにします。

用意する型ですが、整数型 Int、実数型 Real、複素数型 Complex などが考えられます。純虚数型 Imaginary もあったほうがいいかもしれません。

数学的に自然な書き方ができるようにする、という目標のため、これらの型の間には部分型関係 Int <: Real <: Complex, Imaginary <: Complex を持たせるようにします。

また、関数や演算子の型は、

+ : Int -> Int -> Int /\ Real -> Real -> Real /\ Complex -> Complex -> Complex /\ Imaginary -> Imaginary -> Imaginary

という風に交差型を使って表現します。

課題2：より詳細な型づけ

平方根を返す sqrt という関数があります。この関数は正の実数の場合は値が正の実数となりますが、負の実数を与えた場合は結果は虚数になってしまいます。つまり、 sqrt 関数を実数全体で定義するには、関数の終域を複素数とする必要があります。（sqrt(-1) が NaN なのに sqrt(-1+0i) が NaN じゃない、という風にはしません）

しかし、例えば sqrt(|z|^2+1) という計算をする場合には引数は正の実数だと確実にわかるわけです。このような場合、結果の型は複素数じゃなくて実数となって欲しいものです。

そこで、「非負実数」を表す型 NNReal (non-negative real; もっと良い名前はある？) を作り、 sqrt 関数は非負実数に対しては非負実数を返すようにします。

NNReal 型を導入した後の sqrt 関数と + 演算子の型は次のようになります：

sqrt : NNReal -> NNReal /\ Complex -> Complex
 + : ... /\ NNReal -> NNReal -> NNReal

log も同様に NNReal でオーバーロードできます：

log : NNReal -> Real /\ Complex -> Complex

逆三角関数や acosh についても同様の問題がありますが、区間が [-1,1] とか [1,+∞) などと面倒なことになります。そのため、これらについては常に複素数の関数 Complex -> Complex として扱うことにします。

課題3：ユーザー定義の関数や変数

自分で変数や関数を定義できると良さそうです。

課題4：より低レベルに

与えられた式を高レベルな JavaScript の式に翻訳するだけなら簡単です。しかし、Webブラウザーで実行する場合、より低レベルな asm.js や WebAssembly にコンパイルできたら高速化が期待できます。

また、ネイティブアプリ版を作る際は、機械語へのコンパイルができると良さそうです。手間に見合うかはわかりませんが、 SIMD や GPGPU の活用も考えられます。

---

アプリをすでに公開している以上、現行の実装というものがあるわけですが、現行の実装では課題3と4は達成できていません。そこで、型付きラムダ計算をベースに新しく作り直すことにしました。

単に型付きラムダ計算と言っても色々と変種があるので、ここでは次のようなものを考えることにします：

型と演算子

組み込み型は、次を用意します：

• 自然数 Nat （0を含む）
• 整数 Int
• 非負実数 NNReal
• 実数 Real
• 純虚数 Imaginary
• 複素数 Complex
• 真理値 Bool

数学的に正確な計算をしたいというわけではないので、これらの実装には固定長整数や浮動小数点数を使います。

その他、関数型 a -> b とタプル型 (a,b) を用意します。

部分型

以下のルールで部分型関係を定めます：

• Nat <: Int <: Real <: Complex
• Nat <: NNReal
• Imaginary <: Complex
• a’ <: a, b <: b’ ならば a -> b <: a’ -> b’
• a <: a’, b <: b’ ならば (a,b) <: (a’,b’)

コンパイルの際には、部分型関係を利用する箇所に対しては型を変換するコードが挟まります。

交差型

交差型を使って、関数や演算子のオーバーロードを書けるようにします：

+ : Nat -> Nat -> Nat /\ Int -> Int -> Int /\ NNReal -> NNReal -> NNReal /\ Real -> Real -> Real /\ Imaginary -> Imaginary -> Imaginary /\ Complex -> Complex -> Complex
abs : Int -> Nat /\ Complex -> NNReal
sqrt : NNReal -> NNReal /\ Complex -> Complex

交差型は、主に関数の型を記述するのに役立ちます。関数以外の型についての交差型も考えられますが、それを認めるかどうかは、未定です。

関数の「オーバーロード」と書きましたが、なるべくどのオーバーロードを選んでも結果が同じになるようにするのが自然だと思われます。例えば、整数 1 と 2 に対しての 1 / 2 は 0.5 とします。C言語のような 1 / 2 == 0 とはしません。

交差型を持つ関数を自分で定義できるような文法も用意するつもりです。例えば、 double = \x. x + x という関数に適切な注釈を加えて Int -> Int /\ Real -> Real という型を持つようにします。

無限ループ阻止

うっかり無限ループを書いてしまってアプリが操作不能になるのは嬉しくないので、計算能力は制限します。

具体的には、不動点演算子や let rec のような、再帰関数を書くための機構は排除します。

繰り返し自体はできるようにしたいので、「指定された回数だけ関数を適用する」というプリミティブを導入します。チャーチ数的なやつです。

型は iterate : Nat -> (a -> a) -> a -> a という感じになります。

実装を簡単にしたいので、アキュムレーターの型 a として、関数（およびそれを含むタプル型）は使えないようにします。

多相

微妙なところです。交差型との相性が悪そうな気がします。

型推論

型推論は、難しそうなので、しません。

ただ、関数の引数の型を全て書かないといけないのはだるいので、デフォルトの型を幾つか用意しておくことによって関数の引数の型を省略できるようにする、という案は考えられます。

一応確認しておきますが、 let a = 123 という風に変数（定数）を定義する際に型を明示する必要がないという特徴は、ここでは「型推論」とは呼びません。

先行事例

整数から複素数まで、様々な種類の数を混在して扱えるのを、プログラミング言語 Scheme では numerical tower （数の階層）と呼ばれています（雑な理解）。そこで、 numerical tower に型をつけた既存の体系があれば、私が作ろうとしている物体の参考になると思われます。

軽く調べたところ、 Scheme の派生言語である Racket に型をつけたもの (Typed Racket) がそういう体系のようです。この記事で考えている体系と Typed Racket との違いとして、我々は非負実数を特別扱いするのに対し、 Typed Racket には正負を対等に扱います。また、 Typed Racket には有理数型 (Exact-Rational) があります。

The Typed Racket Reference – Type Reference

 

実装

理念だけ書いて実装を載せないというのは良くないので、一応作業中のものを晒しておきます。

https://github.com/minoki/polestar

コードネームは polestar です。私が作った複素関数関連の物体（「複素関数で遊ぼう」「たのしい複素積分」「わくわく解析接続」）には複素解析関連のコードネーム (conformality, singularity, analytic continuation) をつけていますが、今回は pole というわけです。（そんな解説はどうでもいいですね）

作りたい体系は部分型も交差型もありますが、いきなりそこから低レベルコードに落とすのは大変そうなので、中間として単純型つきの体系（Polestar.Core; 後で名前を Polestar.Simple に変えるかも）も実装しています。

交差型の方は、以前ある程度実装してみたので、後回しでいいだろうという判断です。

交差型 (intersection types)

 

単純型付きの方を試すには、

$ stack build
$ stack exec CoreRepl
This is Polestar.Core REPL.
Press Ctrl-D to exit.
> addInt 1 2
Type is Int.
Evaluation:
addInt 1 2
--> 3.
> addNat 0%N 1%N
Type is Nat.
Evaluation:
addNat 0 1
--> 1.
>

という感じにやります。部分型がないので、数値リテラルにはサフィックスとして %N, %Z, %R をつけて型を明示します。

ターゲット：asm.js と WebAssembly

Webブラウザーで高速な実行をするためには、 asm.js もしくは WebAssembly を利用することになります。

両者の違いとして、 asm.js は64ビット整数が使えないという点があります。他の違いとして、asm.js では Math.exp などの数学関数（の一部）が用意されているのに対し、 WebAssembly ではそういう数学関数を自分で用意してやらなくてはなりません（C言語等からコンパイルする際はlibcもリンクするので問題になりませんが）。

筆者にとって JavaScript の文法が既知なこと、数学関数が幾つか使えることなどから、当初は asm.js を吐き出す予定です。

というわけで asm.js をターゲットにするために asm.js の仕様を探っていたら、 asm.js の仕様バグとV8のバグに気づきました。 asm.js の仕様の更新は止まっているので前者は放置、後者はバグレポを投げてあります。asm.js の詳細については以前書いた Qiita を見てください：

asm.js: 仕様と実装の今 – Qiita

進捗

そういう風にまだまだ道半ばで、やるべきことはたくさん残っています。

ただ、最近は「週刊 代数的実数をつくる」をやっているので、こっちの方は放置しています。代数的実数の方がひと段落したら再開するかもしれません。