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
にあります。
参考
Typed final (tagless-final) style
- Tagless fianl について丁寧に解説されています。
-
- Modular implicit の論文です。
Sep 25, 2017 - First-Class Modules and Modular Implicits in OCaml
- 第一級モジュールを用いたアドホック多相からModular Implicitへの流れが分かりやすいです。