TaPLのML実装をRustでやってみるシリーズ「7章 ラムダ計算のML実装」

TAPL本(Types And Programming Language、型システム入門)の各章にある「ML実装」の例をRustにポーティングしてみるシリーズ、「7章のラムダ計算のML実装」です。4章のに比べるといきなり難易度が上がります。全体からしたら序の口でしょうが。

説明

• unstableなゲート化された機能box_patternsを1箇所で使用しているので、Rust 1.0 betaではコンパイルできず、unstable機能がerrorにならないnightly版でしかコンパイルできません。趣旨からして、おそらく1.0 release版でも実行できないでしょう。でもこれを使わずに実装することができなかったのでやむなく。(参考)
• 以下でnamed.rsは、名無し項ではなく、通常の項を表現するものです。7章には指導がないが、名無し項への変換がないと余りに不便なので作りました。
• 以下のようなλ計算が評価できます。

     println!("{:?}",
             apply(abst("a", 
                         apply(abst("b",
                                    apply(var("b"), abst("x", var("b")))),
                               apply(var("a"), abst("z", var("a")))
                               )),
                    abst("w", var("w"))
                    ).remove_names().eval());
// 結果は(lambda w. w)

気づいたことや工夫

• Termのような再帰的データ構造を実現するために、enumでowned pointerを使用すると、Box::newが頻出したりして可読性が悪化するが、enumのデータ構築子をそのまま使うのではなく、以下のような、引数にTermを受けとってBox::newを実行した上でデータ構築を行うような、簡単なラッパーを作ると構築に関しては簡潔さを維持できる。ついでに&str→String変換しておく。欲を出すと、そういう関数群を自動的deriveしてくれるようなTraitがあればいいのに。

fn abst(s:&str, t:Term) -> Term {
    Abst(s.to_string(), Box::new(t))
}

fn apply(t1:Term, t2:Term) -> Term {
    Apply(Box::new(t1), Box::new(t2))
}

• de Bruijn Indexは、数学的証明との対応がしやすい以外のメリットはたぶんなく、本当のコンパイラの実装では導入しない種類のものと思われる。まあ変数名集合の集合操作でやるよりはプログラムっぽいが。
• 何度も言うがrustのパターンマッチは難しい気がする。&,mut,ref,box,などがやっかいにしている。もっとドキュメントもしくは経験が必要だ。
• RustではHaskellやMLのように入れ子になった関数で親をアクセスするものは定義できないらしい(参考)。Closure使えばいいのだろうが、再帰呼び出しするClosureはきれいには定義できない(参考)。
• 環境変数RUST_BACKTRACEを1にするとpanic!時などにスタックトレースが表示される。env RUST_BACKTRACE=1 cargo test みたいに使うとよろし。

nameless.rs

// http://www.cis.upenn.edu/~bcpierce/tapl/checkers/untyped/
#![allow(dead_code)]
#![allow(unused_variables)]
#![allow(unused_imports)]

use std::fmt::Debug;
use std::fmt::Formatter;
use std::fmt::Error;

#[derive(Clone,PartialEq)]
pub enum Term {
    // Single Varialbe
    Var(isize, // de Bruijn Index.
        usize), // length of Context where this variable appealed.
    // Abstraction
    Abst(String, // lambda variable name
         Box<Term>), // lambda body
    // Application
    Apply(Box<Term>, // function
          Box<Term>) // argument
}

#[derive(Debug,Clone)]
pub enum Binding {
    NameBind
}

pub type Context = Vec<(String, Binding)>;

fn index2name(ctx: &Context, idx: isize) -> String {
    if idx > ctx.len() as isize-1 {
        return format!("fv{}", idx)
    }
    ctx[(ctx.len() as isize-idx-1) as usize].0.to_string()
}

use nameless::Term::*;

pub fn add_name(ctx:&Context, name:&String) -> Context {
    let mut new_ctx = ctx.clone();
    new_ctx.push((name.clone(), Binding::NameBind));
    new_ctx
}

fn pick_fresh_name(ctx:&Context, x:&String) -> (Context, String) {
    if ctx.iter().any(|&(ref var_name,_)|{*var_name==*x}) {
        //名前xがctxに存在(重複)していたら、新規名称に変更して再トライ
        pick_fresh_name(ctx, &format!("{}'", x))
    }
    else { // 重複しない名前を得たら
        // ctxにその名前を登録して、(ctx,その名前)を返す。
        (add_name(ctx, x), x.clone())
    }
}

fn print_term(ctx:&Context, t:&Term) -> String {
    match *t {
        Abst(ref var_name, ref t1) => {
            // λ var_name . t1 は、var_nameを環境ctxでユニークであるx_にした上で、
            // x_をctxに登録しそのx_を登録したctx(ctx_)の元で、t1を表示する。
            let (ctx_, x_) = pick_fresh_name(ctx, var_name);
            format!("(lambda {}. {})", x_, print_term(&ctx_, &t1))
        },
        Apply(ref t1, ref t2) => {
            format!("({} {})", print_term(ctx, &t1), print_term(ctx, &t2))
        },
        Var(x, n) => {
            if ctx.len() == n {
                format!("{}", index2name(ctx, x))
            } else {
                format!("[bad index, ctx.len={}, n={}]", ctx.len(), n).to_string()
            }
        }
    }
}

impl Debug for Term {
    fn fmt(&self, fmt:&mut Formatter) -> Result<(), Error> {
        fmt.write_str(&format!("{}", print_term(&vec![], self)))
    }
}

fn term_shift(d:isize, t:&Term) -> Term {
    fn term_shift_helper(c:isize, d:isize, t:&Term) -> Term {
        match *t {
            Var(x, n) =>
                if x >= c { Var(x+d, (n as isize + d) as usize) }
                else { Var(x, (n as isize + d) as usize) },
            Abst(ref x, ref t1) =>
                Abst(x.clone(), Box::new(term_shift_helper(c+1, d, &t1))),
            Apply(ref t1, ref t2) =>
                Apply(Box::new(term_shift_helper(c, d, t1)), Box::new(term_shift_helper(c, d, t2)))
        }
    }

    term_shift_helper(0, d, t)
}

fn term_subst(j:isize, s:&Term, t:&Term) -> Term {
    fn term_subst_helper(j:isize, s:&Term, c:isize, t:&Term) -> Term {
        match *t {
            Var(x, n) =>
                if x == j+c { term_shift(c, s) } else { Var(x, n) },
            Abst(ref x, ref t1) =>
                Abst(x.clone(), Box::new(term_subst_helper(j, s, c+1, t1))),
            Apply(ref t1, ref t2) =>
                Apply(Box::new(term_subst_helper(j, s, c, t1)), Box::new(term_subst_helper(j, s, c, t2)))
        }
    }
    term_subst_helper(j, s, 0, t)
}

fn term_subst_top(s:&Term, t:&Term) -> Term {
    // Apply(Abst(x, t12), v2@Abst(_,_))
    //
    //                        -1        1
    // (λ.t12) v2    →    ↑   ([0→↑  (v2)] t12)
    //
    // 「Apply(Abst(x, t12), v2@Abst(_,_))」の評価は、t12が使用して
    // いる変数x(de Bruijn index=0)をv2で置換するということである
    // (β簡約)。しかし、v2も(de Bruijn index 0)を参照している可能
    // 性があるので、単なる置換はできない。そのためには、v2の(de
    // Bruijn index 0)を(de Bruijn index 1)にする必要がある。さらに、
    // v2はもともと(de Bruijn index 1)を使用しているかもしれないの
    // で、0→1、1→2、2→3...というようにv2で使用している変数すべ
    // ての玉つきでの増加が必要。これが内側のシフト操作
    //      1
    // 0→↑  (v2) 
    // の意味である。
    // 上記より、無事v2から(de Bruijn index 0)を消去できたとして、
    // λの中にあったt12を、λ取ってその外側の中で通用する値として
    // 機能させるには、ネストレベルを一個浅くする必要がある。これが
    // 外側の
    //   -1
    // ↑
    // の操作である。これが意味するのは最内周の変数(de Bruijn
    // index 0)の削除であり、de Bruijn index 1以上の変数をそれぞれ
    // 1個インデックスが減るようにずらす。t12の(de Bruijn index 0)
    // をv2で置換した結果には、(de Bruijn index 0)は(置換されている
    // ので)もう存在していないので、これは安全に実行できる。
    term_shift(-1, &term_subst(0, &term_shift(1, s), t))
}

fn is_val(t: &Term) -> bool {
    match *t {
        Abst(_,_) => true,
        _ => false
    }
}

fn eval1(ctx:&Context, t:&Term) -> Option<Term> {
    match t {
        &Apply(box Abst(ref x, box ref t12), ref v2) if is_val(v2) => {
            Some(term_subst_top(v2, &t12))
        },
        // Apply(v1@Abst(_,_), t2)
        // (λ _._) t2
        &Apply(ref v1, ref t2) if is_val(v1) => {
            match eval1(ctx, t2) {
                Some(t2_) => {
                    // (λ _._) t2_
                    Some(Apply(v1.clone(), Box::new(t2_)))
                },
                None => None
            }
        },
        // Apply(t1, t2)
        &Apply(ref t1, ref t2) => {
            match eval1(ctx, &t1) {
                Some(t1_) => Some(Apply(Box::new(t1_), t2.clone())),
                None => None
            }
        },
        _ => None
    }
}

fn eval(ctx:&Context, t:&Term) -> Term {
    match eval1(ctx, &t) {
        Some(x) => x.eval(),
        None => t.clone()
    }
}

impl Term {
    pub fn eval(&self) -> Term {
        eval(&vec![], self)
    }
}

fn abst(s:&str, t:Term) -> Term {
    Abst(s.to_string(), Box::new(t))
}

fn apply(t1:Term, t2:Term) -> Term {
    Apply(Box::new(t1), Box::new(t2))
}

テストコードを含めたものはこちらのgistにあります。