Call-by-needを採用した言語のインタプリタの実装

この記事は言語実装 Advent Calendar 2016の9日目ために書かれました。

最近僕はcall-by-needに関連する研究をしており、気分を理解するためにcall-by-needを採用した言語のインタプリタをStandard MLで実装したりしました。今回はその時の事でも記事にしておきましょう。

Call-by-needとは？

Call-by-needとは、評価戦略の一種です。評価戦略と言えばcall-by-valueとcall-by-nameが有名でしょう。

Call-by-valueは最も右側のredexから簡約する評価戦略で、例えば(λx. x x) ((λx. x) (λx. x))は

(λx. x x) ((λx. x) (λx. x))
→ (λx. x x) (λx. x)
→ (λx. x) (λx. x)
→ λx. x

と簡約されます。ちなみにλの中は簡約しません。まぁ要するに普通の言語の評価戦略ですね。

一方、call-by-nameは最も左側のredexから簡約する評価戦略で、先ほどの式は

(λx. x x) ((λx. x) (λx. x))
→ ((λx. x) (λx. x)) ((λx. x) (λx. x))
→ (λx. x) ((λx. x) (λx. x))
→ ((λx. x) (λx. x))
→ λx. x

と簡約されます。こちらもλの中は簡約しません。この例だけを見るとcall-by-valueに対してcall-by-nameは優位点が無いように見えますが、 redexを適当に選んで簡約すればweak head normal form（大体値と思って差し支えない。以下、WHNF）に簡約される式はcall-by-nameによってもWHNFに簡約されるといった良い性質を持っています。

例えば、(λx y. y) ((λx. x x) (λx. x x))は適切にredexを選べばλy. yに簡約されますが、call-by-valueでは

(λx y. y) ((λx. x x) (λx. x x))
→ (λx y. y) ((λx. x x) (λx. x x))
→ (λx y. y) ((λx. x x) (λx. x x))
→ …

となってしまい、評価が停止しません。 一方、call-by-nameでは

(λx y. y) ((λx. x x) (λx. x x))
→ λy. y

となり、WHNFまで評価する事ができています。

しかしいくら良い性質があるとは言え、一般的なケースにおいてcall-by-valueに比べて評価のステップが多くなりがちなのは事実。 これは関数の引数を評価する事無く代入しているため、引数を複数回使うような関数では毎回引数を計算し直してしまうのが大雑把な理由ですが、 一度引数を評価したら値を覚えておいて使い回せば解決できると思いませんか？これがcall-by-needの基本的な発想で、deterministicかつ副作用の無い言語ではcall-by-nameと同じ評価結果になります。
評価戦略としてcall-by-needを採用した言語として有名なのがHaskellであり、このときの一度評価した値を覚えておく領域がよく耳にするthunkですね。 Haskellで書いたプログラムはメモリ消費量が世にも奇妙な事になる場合もありますが、大体この一度評価した値を覚えておく領域のせいです。

Call-by-needについてはよろしいでしょうか？多分僕の説明より[1]とかの方が分かりやすいと思うので、そちらもどうぞ。

A Natural Semantics for Lazy Evaluation

インタプリタを実装する際、natural semantics（big-step operational semanticsとも言う）で定義されたsemanticsが大変参考になります。 なにしろ、operational semantics自体が数学的にインタプリタを実装する事でプログラムの意味を定義しているようなものですし、 いちいち1つずつredexを簡約するsmall-step operational semanticsよりredexを全て一気に簡約するbig-step operational semanticsの方が効率的な実装に近い訳です。

Call-by-needを採用した言語のnatural semanticsに関する研究としては、[2]が有名です。適宜参考にしながら作っていきましょう。

[2]を読むとプログラムの意味としてなる4項関係が定義されています。 要するに環境Γの下で式eは値vに評価されて、その際に環境がΔに書き換わるよって事ですが、破壊的代入とか数式で書くのが面倒なのでこんな定義になっています。 MLではそんな事気にしなくて良いので参照で定義しといてガンガン破壊的代入すればよろしい。 また、[2]において変数名はthunkのlocationの役割を兼ねており、Barendregtのvariable conventionとか言うのに従って束縛変数をrenamingしないと正しい評価結果が得られませんが、 MLの参照を使えばlocationもよろしくやってくれるので気にしなくてよろしい。

[2]を読むと、先ほどの4項関係の導出規則として次のような規則が挙げられています。

ちなみに、[2]ではλ計算とは少し違い、mutually recursiveなletを追加した上で関数適用の引数は変数に限定した言語のsemanticsを与えています。A正規化に似た操作で引数が変数以外であってもそのような構文に直せます。 変数名がthunkへのlocationを兼ねているのを思い出すと共にletがまさしくthunkを作っている事に注目すると、関数適用の場合には引数を評価せず、thunkを作って渡している事に他ならない訳です。

先ほどの導出規則で最も注目すべきは変数を評価した際の規則でしょう。 これはthunkに代入する中身を計算する処理に他なりませんが、環境にはrecursiveなletで定義された変数も入っているはずなのにxを取り除いても良いものでしょうか？ まぁ結論は論文に載ってるし大丈夫な訳です。Thunkの中身を評価する際に同じthunkの中身が必要になったからといって評価してしまっては無限ループしてしまいますよね。 f = λx. f xみたいに再帰呼び出しを含んでいるけど停止するやつはλのところで評価が停止してしまうので実行時エラーは避けられます。

一見貧乏臭く見えるこの規則ですが、思わぬ利益を我々に与えてくれます。let val x = x in x endのように評価が停止しない式であっても、先ほどの規則によって停止しない事を有限の時間で判定できる場合があるのです。

言語処理系の実装

構文の定義

言語処理系を実装するにあたって、とりあえず対象言語のASTを定義しましょう。

  datatype pat =
    (* constant *)
      PINT of int
    | PBOOL of bool
    | PNIL
    (* _ *)
    | PWILD
    (* x *)
    | PVAR of string
    (* p :: p *)
    | PCONS of pat * pat
    (* (p1, ... , pn) *)
    | PTUPLE of pat list

  (* abstract syntax tree of expression *)
  datatype exp =
    (* constant *)
      INT of int
    | BOOL of bool
    | NIL
    (* variable *)
    | VAR of string
    (* fn x => M *)
    | ABS of string * exp
    (* M N *)
    | APP of exp * exp
    (* let d in N end *)
    | LET of dec list * exp
    (* (M_1, ... , M_n) *)
    | TUPLE of exp list
    (* case M of p1 => N1 | ... | pn => Nn *)
    | CASE of exp * (pat * exp) list
    (* primitives *)
    | PRIM of Prim.prim * exp list
    | CONS of exp * exp
  (* abstract syntax tree of declaration *)
  and dec =
    (* val x = M *)
      VAL of string * exp
    (* val rec x1 = M1 and ... and xn = Mn *)
    | VALREC of (string * exp) list

うん、Standard MLのサブセットなんだ、すまない。 構文的にはStandard MLから参照、モジュール、レコードを除いて、datatypeはリストと組のみに制限したような言語です。 プリミティブとしては加算、減算、乗算、小なりの判定があります。

字句解析や構文解析については割愛。たまに言語処理系の本と言いつつ古典的な字句解析や構文解析に分量を割きすぎているものもありますが、僕はASTにしてからこそ言語処理系の醍醐味だと思うので。
ついでに型推論なんかも行っていますが、よくあるlet多相な言語のやつなので割愛。気になる人は[3]とか読めば良いかと。

WHNFの定義

[2]の意味論の変数をthunkのlocation、letをthunkの作成と読み替えながら実装していく訳ですが、いちいち関数呼び出しの度に代入なんてしてたら計算時間がいくらあっても足りません。 そこで、storeもどきの環境とは別に変数からthunkのlocationへの有限写像である環境を新しく導入し、代入を遅延させます。まぁいつもの環境、あるいは評価文脈ですね。 このため関数の値がクロージャになります。

  datatype value =
      INT of int
    | BOOL of bool
    | NIL
    | CONS of thunk * thunk
    (* closure *)
    | FUN of env * string * Syntax.exp
    | TUPLE of thunk list
  withtype thunk = (unit -> value) ref
  and env = thunk StringMap.map

Thunkの中身の取り出し

[2]の変数についての評価規則がthunkの中身の取り出しに相当する訳です。 先ほどしれっとthunkはunitを受け取ってWHNFを返す関数の参照として定義しましが、 thunkの中身を評価する際に再び同じthunkの中身を評価しようとしたかどうか判定するにはどうすれば良いでしょうか？ それにも破壊的代入の力を借りればよろしい。

  (* obtain value from thunk *)
  fun force (thunk as ref f) =
    let
      val () = thunk := (fn () => raise Bottom)
      val v = f ()
      val () = thunk := (fn () => v)
    in v end

Thunkの中身を評価する関数を取り出しておき、thunkの中身が再び評価された場合には例外を投げるように仕込んでおきます。 そしてthunkの中身を評価し、値に評価されたならばついでに覚えておく訳です。

インタプリタの実装

ひたすらthunkを作っていくところと余計な所でthunkの中身を取り出さない所に注意が必要ですが、[2]を読めばほぼ自明かと。 注意が必要なのが[2]でletに相当するval recの評価で、まずでたらめなthunkを作ってから破壊的代入で循環的なデータ構造を作っています。

  (* perform pattern matching and bind variables *)
  fun patEval env (Syntax.PINT n) v =
        (case force v of
              INT n' =>
                if n = n' then SOME env
                else NONE
            | _ => NONE)
    | patEval env (Syntax.PBOOL b) v =
        (case force v of
              BOOL b' =>
                if b = b' then SOME env
                else NONE
            | _ => NONE)
    | patEval env Syntax.PNIL v =
        (case force v of
              NIL => SOME env
            | _ => NONE)
    | patEval env Syntax.PWILD v = SOME env
    | patEval env (Syntax.PVAR x) v =
        SOME (StringMap.insert (env, x, v))
    | patEval env (Syntax.PCONS (p1, p2)) v =
        (case force v of
              CONS (v1, v2) =>
                (case patEval env p1 v1 of
                      NONE => NONE
                    | SOME env => patEval env p2 v2)
            | _ => NONE)
    | patEval env (Syntax.PTUPLE ps) v =
        (case force v of
              TUPLE vs =>
                ListPair.foldlEq (fn
                    (p, v, NONE) => NONE
                  | (p, v, SOME env) =>
                      patEval env p v) (SOME env) (ps, vs)
            | _ => NONE)

  fun thunkFromSyntaxExp env m = ref (fn () => evalExp env m)

  and evalExp env (Syntax.INT n) = INT n
    | evalExp env (Syntax.BOOL b) = BOOL b
    | evalExp env Syntax.NIL = NIL
    | evalExp env (Syntax.VAR x) =
        force (valOf (StringMap.find (env, x)))
    | evalExp env (Syntax.ABS (x, m)) = FUN (env, x, m)
    | evalExp env (Syntax.APP (m, n)) =
        let val FUN (env0, x, m0) = evalExp env m in
          evalExp (StringMap.insert (env0, x, thunkFromSyntaxExp env n)) m0
        end
    | evalExp env (Syntax.LET (dec, m)) =
        evalExp (foldl (fn (dec, env) =>
          StringMap.unionWith #2 (env, evalDec env dec)) env dec) m
    | evalExp env (Syntax.TUPLE ms) =
        TUPLE (map (thunkFromSyntaxExp env) ms)
    | evalExp env (Syntax.CASE (m, pns)) =
        let val v = thunkFromSyntaxExp env m in
          case findMap (fn (p, n) =>
            case patEval env p v of
                 NONE => NONE
               | SOME env => SOME (evalExp env n)) pns of
               NONE => raise PatternMatchFailure
             | SOME v => v
        end
    | evalExp env (Syntax.PRIM (p, ms)) =
        (case (p, map (evalExp env) ms) of
              (Prim.PLUS, [ INT m, INT n ]) => INT (m + n)
            | (Prim.MINUS, [ INT m, INT n ]) => INT (m - n)
            | (Prim.TIMES, [ INT m, INT n ]) => INT (m * n)
            | (Prim.LE, [ INT m, INT n ]) => BOOL (m <= n))
    | evalExp env (Syntax.CONS (m, n)) =
        CONS (thunkFromSyntaxExp env m, thunkFromSyntaxExp env n)

  and evalDec env (Syntax.VAL (x, m)) =
        StringMap.singleton (x, thunkFromSyntaxExp env m)
    | evalDec env (Syntax.VALREC xms) =
        let
          val xmvs = map (fn (x, m) =>
            (x, m, ref (fn () => raise (Fail "dummy")))) xms
          val env' = foldl (fn ((x, _, v), env) =>
            StringMap.insert (env, x, v)) StringMap.empty xmvs
          val env = StringMap.unionWith #2 (env, env')
        in
          app (fn (x, m, v) => v := (fn () => evalExp env m)) xmvs;
          env
        end

動作確認

- let val rec bot = bot in
  (fn x => 1) bot
end;
val it = 1 : int

- let val rec bot = bot in
  case (bot, 2) of (x, y) => y
end;
val it = 2 : int

Call-by-valueだと問題になる位置に停止しない式が含まれていても値に評価されています。

- val if_ = fn b => fn x => fn y =>
  if b then x else y;
val if_ = fn : (bool -> ('12 -> ('12 -> '12)))

- val rec fix = fn f => f (fix f);
val fix = fn : (('17 -> '17) -> '17)

- fix (fn fib => fn x =>
  if_ (x <= 1) x (fib (x - 1) + fib (x - 2))) 6;
val it = 8 : int

Call-by-needではifも関数として扱えますし、わざわざeta expansionしなくてもfixを定義できます。

- val rec map = fn f => fn l =>
  case l of [] => [] | h :: t => f h :: map f t;
val map = fn : (('7 -> '8) -> ('7 list -> '8 list))

- val rec even = 0 :: map (fn x => x + 1) odd
and odd = map (fn x => x + 1) even;
val even = (0 :: (2 :: (4 :: (6 :: (8 :: (10 :: (12 :: (14 :: (16 :: (18 :: (20 :: (22 :: (24 :: (26 :: (28 :: (30 :: (32 :: (34 :: (36 :: ( ...  ::  ... )))))))))))))))))))) : int list
val odd = (1 :: (3 :: (5 :: (7 :: (9 :: (11 :: (13 :: (15 :: (17 :: (19 :: (21 :: (23 :: (25 :: (27 :: (29 :: (31 :: (33 :: (35 :: (37 :: ( ...  ::  ... )))))))))))))))))))) : int list

- val rec zipWith = fn f => fn l1 => fn l2 =>
  case (l1, l2) of
       ([], _) => []
     | (_, []) => []
     | (x :: l1, y :: l2) => f x y :: zipWith f l1 l2
;
val zipWith = fn : (('38 -> ('39 -> '41)) -> ('38 list -> ('39 list -> '41 list)))

- val tail = fn x =>
  case x of h :: t => t;
val tail = fn : ('47 list -> '47 list)

- val rec fibs = 0 :: 1 :: zipWith (fn x => fn y => x + y) fibs (tail fibs);
val fibs = (0 :: (1 :: (1 :: (2 :: (3 :: (5 :: (8 :: (13 :: (21 :: (34 :: (55 :: (89 :: (144 :: (233 :: (377 :: (610 :: (987 :: (1597 :: (2584 :: ( ...  ::  ... )))))))))))))))))))) : int list

Haskellの醍醐味、circularなプログラムも書けます。

- val rec x = y
and y = x;
Error : infinite loop
- let
  val rec x =
    ((case x of (_, snd) => snd),
     (case x of (fst, _) => fst))
in case x of (fst, _) => fst end;
Error : infinite loop

有限ステップで停止しない事がLaunchburyのsemanticsで検出できる場合にはその旨を表示しています。

結び

評価戦略としてcall-by-needを採用した言語のインタプリタを実装できました。 実際に言語処理系を実装してみた事でsemanticsへの理解が深まったように思えます。 今回実装した言語処理系のソースコードについてはこちらをどうぞ。

参考文献

[1] Benjamin C. Pierce, Types and Programming Languages, The MIT Press
[2] http://okmij.org/ftp/ML/generalization.html
[3] John Launchbury, A Natural Semantics for Lazy Evaluation, POPL '93