DeBruijn変換がやっと分かった - ::Eldesh a b = LEFT a

算譜工論(DeBrujn変換) を読んでDeBruijn変換をSMLで実装してみました。＞ https://gist.github.com/eldesh/5714388
文書内の説明がほとんどMLのコードまんまなのでほとんど単なる写経なのですが。
ちなみに、これによってどんな嬉しい性質があるのかはまだ知らないのです…。誰か教えてくれてもいいのよ？

この変換を行うと、以下のような(引数に普通に名前を付けている)ラムダ式が

λx.x(λy.x y (λz.x y z))

次のような、識別子に整数を割り振った式になります。

λ.0 (λ.1 0 (λ.2 1 0))

以下に書いたSMLコードを抜粋します。(Gistには全体が張ってあります)

structure Lambda = struct
  (* 変換前の普通の式 *)
  datatype t = Num of int
             (* 変数が名前を持つ *)
             | Var of string
             (* 引数の名前を持つ *)
             | Lam of string * t
             | App of t * t
             | Let of string * t * t
             | Letrec of string * t * t
end

structure DeBruijn = struct
  (* 変換後の式 *)
  datatype t = Num of int
             (* 変数は整数番号で識別される *)
             | L of int
             (* 番号から引数がどれなのかは明らかなので陽に持たない *)
             | Fn of t
             | App of t * t
             | Let of t * t
             | Letrec of t * t

  structure E = Lambda

  (* 変数名をスタックから探して識別番号を得る *)
  fun getindex i [] v = raise Fail (concat["getindex ", Int.toString i])
    | getindex i (v'::vs) v = if v' = v then i
                              else getindex (i+1) vs v
  fun index_var vs expr =
    case expr
      of E.Num x => Num x
       | E.Var id => let val i = getindex 0 vs id
                     in L i end
       | E.Lam (v,e) => let val e' = index_var (v::vs) e
                        in Fn e' end
       | E.App (e1,e2) => let val e'1 = index_var vs e1
                              val e'2 = index_var vs e2
                          in App (e'1, e'2) end
       | E.Let (v,e1,e2) => let val e1' = index_var vs e1
                                val e2' = index_var (v::vs) e2
                            in Let (e1',e2') end
       | E.Letrec (v,e1,e2) => let val e1' = index_var (v::vs) e1
                                   val e2' = index_var (v::vs) e2
                               in Letrec (e1',e2') end

  (* De Bruijn変換 *)
  fun translate expr = index_var [] expr
end