Tagless final, First-class module, Modular implicit

はじめに

これは ML Advent Calendar 2017 の 19日目の記事です．

最近 Typed final (tagless-final) style を読みました。 このレクチャーノートではサンプルコードとして Haskell で型クラスを用いたものと OCaml でファンクターを用いたものが示されています。 このポストではそれらを OCaml の第一級モジュールと Modular implicit を使って書いてみました。 tagless final、第一級モジュール、Modular implicit それぞれについて真面目に説明するのは無理だったので簡単な説明にとどめています。

Final アプローチ

次のように代数的データ構造を定義してその上の処理を書くことがよくあると思います。

type exp = Lit of int | Neg of exp | Add of exp * exp

let rec eval = function
  | Lit i -> i
  | Neg e -> - (eval e)
  | Add (e1, e2) -> (eval e1) + (eval e2)

これに対して、コンストラクタを単に関数とすることで同じことが表現できます。

let lit i = i
let neg e = - e
let add e1 e2 = e1 + e2

前者のようにコンストラクタによって表現を埋め込む手法を initial アプローチ

後者のように関数によって表現を埋め込む手法を final アプローチ と呼びます。

しかし、上の final アプローチでは処理が複数ある場合明らかに困ったことになります。 例えば次の show のような処理を追加することを考えます。

let rec show = function
  | Lit i -> string_of_int i
  | Neg e -> "-" ^ (show e)
  | Add (e1, e2) -> "(" ^ (swho e1) ^ "+" ^ (show e2) ^ ")"

initial アプローチでは単に上の関数を追加するだけで良いのですが、 fianl アプローチでは同じ名前の別の関数を定義すること必要になるので工夫が必要です。

Haskellには型クラスがあるので次のように定義することができます。

class ExpSYM repr where
  lit : Int → repr
  neg : repr → repr
  add : repr → repr → repr

instance ExpSYM Int where 
  litn = n
  neg e = − e 
  add e1 e2 = e1 + e2

instance ExpSYM String where 
  lit n = show n
  neg e = "(-" + e + ")" 
  add e1 e2 = "(" + e1 + "+" + e2 + ")"

一方、OCaml ではモジュールとファンクターを使うことで解決することができます。 Haskell の型クラスをモジュール型、そのインスタンスをモジュールに対応させます。

module type ExpSYM = sig
  type repr
  val lit : int -> repr
  val neg : repr -> repr
  val add : repr -> repr -> repr  
end

module ExpSYMInt : ExpSYM with type repr = int = struct
  type repr = int
  let lit n = n
  let neg e = - e
  let add e1 e2 = e1 + e2
end

module ExpSYMString : ExpSYM with type repr = string = struct
  type repr = string
  let lit n = string_of_int n
  let neg e = "-" ^ e
  let add e1 e2 = "(" ^ e1 ^ "+" ^ e2 ^ ")"
end

repr は abstrac type として定義されているため、計算結果も抽象化されたままで普通に扱うことができなくなってしまうので、モジュールの定義時に with type 以下で実際の型の制約を入れています。

ファンクターを用いることで次のように使用できます。

utop # module F (M : ExpSYM) = struct 
        let tf = M.(add (lit 1) (neg (lit 2))) 
      end;;
module F : functor (M : ExpSYM) -> sig val tf : M.repr end

utop # let module M = F(ExpSYMInt) in M.tf;;
- : ExpSYMInt.repr = -1

utop # let module M = F(ExpSYMString) in M.tf;;
- : ExpSYMString.repr = "(1+-2)"

第一級モジュール

次に上の例を第一級モジュールを使って書き換えます。 第一級モジュールとはモジュールをコア言語内で扱うための機能で、これを用いれば 例えば関数の引数などにモジュールを渡すことが可能になります。

第一級モジュールについて詳しくは RWO などを参照してください。

上の例は次のように書き換えられます。

let tf1 (type a) (module M : ExpSYM with type repr = a) =
  M.(add (lit 8) (neg (add (lit 1) (lit 2))))

ExpSYM 内で abstract type として定義されている repr がエスケープしないように locally abstract type で注釈しています。

次のように使用できます。

top # tf1 (module ExpSYMInt);;
- : int = 5

utop # tf1 (module ExpSYMString);;
- : string = "(8+-(1+2))"

final アプローチの利点として、既存の部分に触れることなく表現を拡張できることがあります。

例えば、上の表現に mul を加えることを考えます。 initial アプローチではまず exp の定義に Mul of exp * exp を加え、eval、show もそれに合わせて書き換えることになります。一方 fianl アプローチでは次のコードを追加するだけで、既存の部分に手を加える必要はありません。

module type MulSYM = sig
  type repr
  val mul : repr -> repr -> repr
end

module MulSYMInt : MulSYM with type repr = int = struct
  type repr = int
  let mul e1 e2 = e1 * e2
end

module MulSYMString : MulSYM with type repr = string = struct
  type repr = string
  let mul e1 e2 = "(" ^ e1 ^ "*" ^ e2 ^ ")"
end

使用例は次の通りです。

let tfm1 (type a) (module S1 : ExpSYM with type repr = a) (module S2 : MulSYM with type repr = a) = 
  let open S1 in
  let open S2 in
  add (lit 7) (neg (mul (lit 1) (lit 2)))

utop # tfm1 (module ExpSYMInt) (module MulSYMInt);;
- : int = 5

utop # tfm1 (module ExpSYMString) (module MulSYMString);;
- : string = "(7+-(1*2))"

期待通りに動きますが、引数で渡す第一級モジュールが少し煩わしくなってきます。

Modular Implicit

上の例では第一級モジュールを引数に渡すことで処理をディスパッチしていました。 しかし、型からどう使われるかが分かればわざわざ引数として与えてやる必要がない気がします。 これを実現するのが Modular implicit という機能です。 Modular implicit が乗ったコンパイラは opam switch 4.02.0+modular-implicits で試せます。

Modular implicit を用いると上の例は次のように書けます。

module type ExpSYM = sig
  type repr
  val lit : int -> repr
  val neg : repr -> repr
  val add : repr -> repr -> repr  
end

implicit module ExpSYMInt : ExpSYM with type repr = int = struct
  type repr = int
  let lit n = n
  let neg e = - e
  let add e1 e2 = e1 + e2
end


implicit module ExpSYMString : ExpSYM with type repr = string = struct
  type repr = string
  let lit n = string_of_int n
  let neg e = "-" ^ e
  let add e1 e2 = "(" ^ e1 ^ "+" ^ e2 ^ ")"
end

let tf1 {S : ExpSYM} k =
let open S in
add (lit 8) (neg (add (lit 1) (lit 2)))
|> k

let eval : int -> int = fun x -> x
let show : string -> string = fun x -> x

第一級モジュールが来ていた位置の引数が波括弧に変わっています。 これは Modular implicit 用の構文で、この引数には型に合わせてコンパイラが選んだモジュールが暗黙に渡されます。その際 implicit をつけて定義したモジュールが候補になります。

また、型を合わせるためにその後の処理を継続の形で渡しています。

# tf1 eval;;
- : int = 5

# tf1 show;;
- : string = "(8+-(1+2))"

mul で拡張すると次のようになります。

module type MulSYM = sig
  type repr
  val mul : repr -> repr -> repr
end

implicit module MulSYMInt : MulSYM with type repr = int = struct
  type repr = int
  let mul e1 e2 = e1 * e2
end

implicit module MulSYMString : MulSYM with type repr = string = struct
  type repr = string
  let mul e1 e2 = "(" ^ e1 ^ "*" ^ e2 ^ ")"
end

let tfm1 (type a) {S1 : ExpSYM with type repr = a} {S2 : MulSYM with type repr = a} (k : a -> a) = 
  let open S1 in
  let open S2 in
  add (lit 7) (neg (mul (lit 1) (lit 2)))
  |> k

# tfm1 eval;;
- : int = 5
# tfm1 show;;
- : string = "(7+-(1*2))"

複数のモジュールを用いる際も引数としてそれぞれ渡す必要が無くなっています。

initial アプローチと final アプローチの関係

initial アプローチと final アプローチは互いに変換することも可能です。

type exp = Lit of int | Neg of exp | Add of exp * exp

implicit module ExpSYMExp : ExpSYM with type repr = exp = struct 
  type repr = exp
  let lit n = Lit n
  let neg e = Neg e
  let add e1 e2 = Add (e1, e2)
end

let initialize : exp -> exp = fun e -> e

let rec finalize : type a. {S : ExpSYM with type repr = a} -> exp -> a =
fun {S : ExpSYM with type repr = a} x ->
  let open S in match x with
    | Lit n -> lit n
    | Neg e -> neg (finalize e)
    | Add (e1, e2) -> add (finalize e1) (finalize e2)

let finalize : type a. {S : ExpSYM with type repr = a} -> (a -> a) -> exp -> a = fun {S : ExpSYM with type repr = a} f x ->
  let rec aux : type a. {S : ExpSYM with type repr = a} -> exp -> a =
    fun {S : ExpSYM with type repr = a} x ->
      let open S in match x with
        | Lit n -> lit n
        | Neg e -> neg (aux e)
        | Add (e1, e2) -> add (aux e1) (aux e2) in
  aux x |> f

# tf1 initialize;;
  - : exp = Add (Lit 8, Neg (Add (Lit 1, Lit 2))) 
# tf1 initialize |> (finalize eval);;
- : int = 5
# tf1 initialize |> (finalize show);;
- : string = "(8+-(1+2))"

Tagless Final

最後に　Tagless Final 形式での整数付きの STLC を書いてみます。

module type Symantics = sig
  type 'a repr
  val int : int -> int repr
  val add : int repr -> int repr -> int repr
  val lam : ('a repr -> 'b repr) -> ('a -> 'b) repr
  val app : ('a -> 'b) repr -> 'a repr -> 'b repr
end

type 'a r = R of 'a
let unR = function R x -> x

implicit module SymanticR : Symantics with type 'a repr = 'a r = struct
  type 'a repr = 'a r
  let int x = R x
  let add e1 e2 = R (unR e1 + unR e2)
  let lam f = R (fun x -> R x |> f |> unR)
  let app e1 e2 = R (unR e1 (unR e2))
end

type 'a s = S of (int -> string)
let unS = function S x -> x

implicit module SymanticS : Symantics with type 'a repr = 'a s = struct
  type 'a repr = 'a s
  let int x = S (fun _ -> string_of_int x)
  let add e1 e2 = S (fun h -> "(" ^ unS e1 h ^ "+" ^ unS e2 h ^ ")")
  let lam e = S (fun h -> let x = "x" ^ string_of_int h in
                          "("^x^" -> "^ (unS (e (S (fun _ ->x)))) (h+1) ^")")
  let app e1 e2 = S (fun h -> "(" ^ unS e1 h ^ " " ^ unS e2 h ^ ")")
end

let th1 {M : Symantics} f = 
  M.(app (lam (fun x -> add x x)) (int 21)) |> f

let eval = unR
let show x = unS x 0

# th1 eval;;
- : int = 42
# th1 show;;
- : string = "((x0 -> (x0+x0)) 21)"

型がつかない項が書けないことも確認できます。

# let th2 {M : Symantics} f = M.(app (int 4) (int 3)) |> f;;
Error: This expression has type int M.repr
       but an expression was expected of type ('a -> 'b) M.repr
       Type int is not compatible with type 'a -> 'b

まとめ

全体としてまとまり無く不親切な感じになりましたが、tagless final を modular implicit を使って書きました。

このポストでは触れていない部分を含めたコード全体は

ML Advend Clendar 2017 · GitHub

にあります。

参考