SATySFiに多段階計算を入れる構想

追記： 本記事で紹介した多段階計算の言語機能はSATySFi 0.0.4にてリリースされました:tada: ただし，以下で紹介している，多段階計算と可変参照の共存により生じうる実行時エラーであるscope extrusionについては静的に検出できる仕組みにはなっていません．

概要

SATySFiに入れようと長らく思案している 多段階計算 (multi-stage programming) に関する機能のごく初歩について紹介します．多段階計算とは平たく言えば計算機言語に於けるいわゆる マクロ の機能を実現するための定式化のひとつです．LaTeXなどでの用法の「マクロ」とは必ずしも関連がないのでご注意ください（ちなみに，SATySFiの前身である Macrodown の名前もややこしいことにLaTeXの意味での「マクロ」の用法に由来していて単なる函数のことであり，ここでのマクロとは関連はありません）．

多段階計算が入ると何が嬉しいのか

どの言語でも多段階計算に相当する機能が入ると

• 事前に計算できる部分を “コンパイル時” に計算し，“実行時” の計算効率上のオーヴァーヘッドを減らす
• 函数では抽象化できないような共通の処理の記述を括り出す

などの恩恵がありますが，SATySFiでは特に重要な利点があり，それは “静的な言語内DSL” の定義に使える，という点です．DSL（＝ domain-specific language，領域特化言語）とは用途が限定された言語のことであり，言語内DSL とは或る（より汎用な）言語のコード中に埋め込んで使う言語を指します．例えばLaTeXに対してTikZは言語内DSLと言って差し支えないかと思います．現在のSATySFi（v0.0.3）でも原理的には

let-block ctx +my-own-DSL-command s =
  〈文字列で与えられたコード s を字句解析・構文解析（・型検査）にかけた後評価してブロックボックス列をつくる処理〉

などとDSLを処理するためのコマンドを定義して

  +my-own-DSL-command(`
    〈DSLコード〉
  `);

などとして使えば独自DSLのコードをSATySFiソース中で使うことができますが，問題はこのDSLで書かれたコードに対して字句解析・構文解析（・型検査）・評価が施されるタイミングがSATySFiから見れば評価中であることです．つまり，DSLで書かれたコード中に何らかのエラーが含まれている場合，それはSATySFiの評価中に報告されることになります．したがって，500ページある文書の490ページ目に書かれたDSLのコード中にエラーがあった場合，ユーザはそれ以前の490ページ分の文書内容が評価されてブロックボックス列として確定するのを待ってはじめてエラーを見ることになります．静的にエラーを報告することがSATySFiの志向するところだったはずなのに，これではSATySFi内でDSLを使うと途端に動的にエラーが出る荒涼な世界に逆戻りしてしまうことになります．これを解決し，SATySFi内DSLのコードに含まれたエラーも “実質的に静的に” 報告できるようにするのが多段階計算です．

多段階計算の基礎

多段階計算は90年代初頭頃に主として 部分評価 (partial evaluation) での 束縛時解析 (binding-time analysis) の系譜からその概念が確立され，以降さまざまな研究が蓄積されていくつかの定式化がありますが，ここでは λ° [Davies 2017] や MetaML [Taha & Sheard 1997] に近い定式化を採用します．まず構文として通常の式に

e ::= … | &e | ~e

という具合に2種類の構成方法が追加されます．&e は ブラケット (bracket)，~e は エスケープ (escape) とそれぞれ呼ばれます．多段階計算には ステージ (stage) という概念が備わっており，各部分式に自然数（0含む）がステージとして割り当てられます．ブラケットはステージを1上げ，エスケープは1下げます．この言語で書かれたプログラムは，まずステージ0で評価が進む部分がすべて評価されてステージ1のコードが生成され，続いてステージ1で評価が進む部分がすべて評価されてステージ2のコードが生成され，…… と段階的に評価されます．例えば自然数 n を受け取って n 乗函数のコードを返す函数 power は

let aux = fix aux. λn. λs.
  if n <= 0 then &1 else &(~s * ~(aux (n - 1) s))
in
let power n =
  &(λx. ~(aux n &x))

で定義でき，実際の評価例は（多少インフォーマルですが）

power 3
  →* &(λx. ~(aux 3 &x))
  →* &(λx. ~(if 3 <= 0 then &1 else &(~&x * ~(aux (3 - 1) &x))))
  →* &(λx. ~(&(x * ~(aux 2 &x))))
  →* &(λx. ~(&(x * ~(if 2 <= 0 then &1 else &(~&x * ~(aux (2 - 1) &x))))))
  →* &(λx. ~(&(x * ~&(x * ~(aux 1 &x)))))
  →* &(λx. ~(&(x * ~&(x * ~(if 1 <= 0 then &1 else &(~&x * ~(aux (1 - 1) &x)))))))
  →* &(λx. ~(&(x * ~&(x * ~&(x * ~(aux 0 &x))))))
  →* &(λx. ~(&(x * ~&(x * ~&(x * ~(if 0 <= 0 then &1 else … ))))))
  →* &(λx. ~(&(x * ~&(x * ~&(x * ~&1)))))
  →* &(λx. ~(&(x * ~&(x * ~&(x * 1)))))
  →* &(λx. ~(&(x * ~&(x * (x * 1)))))
  →* &(λx. x * (x * (x * 1)))

という具合です．0ステージ目で power 3 評価し，1ステージ目で使える3乗函数が生成されているというわけです．1ステージ目では評価時に（通常の多段階でない累乗函数のような）再帰を行なう必要がないため，オーヴァーヘッドが減ることが期待できます．

SATySFiでの多段階計算の利用

多段階計算をおおよそ

~(my-own-DSL-function `〈DSLコード〉`)

という形で用いることでマクロとすることを想定しています（実際にはこういった構文を直接書くのではなく， MacroML [Ganz, Sabry & Taha 2001] のような形式の，より扱いやすい糖衣構文でラップできると考えています）．こうすることで，これまでの通常の評価はステージ1の段階で行なわれ，マクロ展開に相当する，DSLコードに対する処理は，ステージ0で行なわれることになり，たとえ500ページの文書の490ページにあるDSLのコードでも通常の文書内容が評価されてブロックボックス列が構築され始めるよりも前に実施され，したがってDSL内の記述に起因するエラーが出る場合は組版処理よりも前の段階でエラーが報告できる，という算段です．

非自明な点

重要なのは型システムです．マクロを展開してから型検査をする，C++のテンプレートメタプログラミングやOCamlのPPXなどのような仕組みではマクロの実装が困難になる場面も多く，参考文献の各論文で提案されている型システムにより “マクロ定義” まるごと型検査するようにしたいと考えています．多段階計算の型システム一般については説明するとかなり長くなるのでここでは省きます．詳細は参考文献に掲げた論文をご覧ください．

しかし，多段階計算の型システムに可変参照の扱いを取り込むのが厄介です．可変参照のある多段階計算の体系は，具体的には次のような問題を引き起こします：

let r = ref &0 in
let a = &(λx. ~(r <- &x; &1)) in
!r

このプログラムをステージ0で評価すると自由変数が出現したステージ1のコードが生成されてしまいます．これを scope extrusion といい，この類いの振舞いを許すとステージ0はつつがなく評価が進む一方ステージ1で初めて評価中に破滅してしまうことになるので，できればこの望ましくないコードを生成するプログラムを型検査時に弾いてしまいたいというわけです．先行研究としては <NJ> [Kiselyov, Kameyama & Sudo 2016] がありますが，これは直接MetaMLのような構文で扱えるわけではない（ソース言語をMetaML風の言語にして中間言語として<NJ>を使うことは一応可能です）ほか，型推論アルゴリズムが可能な体系に形式化しなおすなどいくつかの重要な変更を実用上要し，現在取り組んでいるところです（或る程度の目処がつく兆しは出ています）．

参考文献

1. Rowan Davies. A temporal logic approach to binding-time analysis. In Journal of the ACM, Volume 64 Issue 1, 2017.
2. Steve Ganz, Amr Sabry, and Walid Taha. Macros as multi-stage computations: Type-safe, generative, binding macros in MacroML. In Proceedings of the International Conference on Functional Programming (ICFP’01), pages 74–85, 2001.
3. Oleg Kiselyov, Yukiyoshi Kameyama, and Yuto Sudo. Refined environment classifiers: type- and scope-safe code generation with mutable cells. In Proceedings of Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, pages 271–291, 2016.
4. Walid Taha and Tim Sheard. Multi-stage programming with explicit annotations. In Proceedings of the 1997 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation (PEPM’97), pages 203–217, 1997.