Tagless Final

programming-paradigmtype-theory

埋め込み DSL（と副作用プログラム）を、操作を データ構築子ではなく、結果表現の型でパラメータ化した型クラス/インターフェースのメソッドとして表現する技法。解釈＝インタプリタが「型クラスのインスタンス」になる。Carette・Kiselyov・Shan「Finally Tagless, Partially Evaluated」(2007) が出典。

名前の由来 — 「tagless」と「final」

形（Haskell）

操作を型クラスで宣言し、各インタプリタをインスタンスとして与える。

class ExprSym repr where
  lit :: Int -> repr Int
  add :: repr Int -> repr Int -> repr Int

-- 項は多相: 「ExprSym のどれか」を要求するだけで AST は無い
term :: ExprSym repr => repr Int
term = add (lit 1) (lit 2)

-- インタプリタ = インスタンス（評価）
newtype Eval a = Eval { runEval :: a }
instance ExprSym Eval where
  lit n            = Eval n
  add (Eval a) (Eval b) = Eval (a + b)

-- 別解釈 = 別インスタンス（整形）
newtype Pretty a = Pretty { runPretty :: String }
instance ExprSym Pretty where
  lit n            = Pretty (show n)
  add a b          = Pretty (runPretty a ++ " + " ++ runPretty b)

term はどのインスタンスを選ぶかで評価にも整形にもなる。同じ項に複数の解釈を与えられる。

Scala / 副作用での tagless-final（実務での主流）

能力（capability）を型クラスにし、プログラムを 作用型 F[_] で抽象する。

trait Console[F[_]] { def putStrLn(s: String): F[Unit]; def readLn: F[String] }

def prog[F[_]: Console: Monad]: F[Unit] = ...   // F は IO でもテスト用 State でも

F を本番は IO、テストは State/Writer に差し替えられる。cats 系で「tagless-final スタイル」と言えば通常これ。

Initial vs Final

Initial（ADT/GADT + インタプリタ）Final（型クラス）
項の表現データ構築子メソッド/インスタンス
インタプリタfold / パターンマッチ型クラスのインスタンス
操作の追加ADT と全インタプリタを改修新しい型クラスを足すだけ
解釈の追加fold 関数を足す新しいインスタンスを足す
AST の検査/変換容易（データがある）困難（具体 AST が無い）
型付き項の安全性tagless にするには GADT が要るホスト型をそのまま使える

両軸（操作の追加・解釈の追加）を型クラスの分割で広げられ、表現問題（expression problem）への一つの解になる。

Free モナドとの対比

Free モナド＝作用の initial encoding（AST を組んで後で解釈）。tagless-final＝ final encoding（AST を作らず直接 F へ）。

利点と弱点

なぜ効くか

本質は Church/Böhm–Berarducci エンコーディング（任意の ADT は「その畳み込み関数」として表せる）を型付き DSL に適用したもの。データとして持つ代わりに「解釈の仕方」をそのまま値にするので、始代数（データ）と終象（解釈）の双対として initial/final が対になる。

関連

Graph

Backlinks