依存型による単純型付きλ計算(STLC)のインタプリタ
PoPLの論文(Intrinsically-Typed Definitional Interpreters for Imperative Languages)についての輪講で、発表の際に使用したスライドの供養(ブログ用に多少修正は加えている)
ソースコードはこれ github.com
Agdaを知らなくても、Haskellの入門程度の知識と、コードを読む力と気合いがあればわかります。
この手の話に興味がある人は面白く感じることでしょう。
参考: - What is Agda? -- Agda docs
1. Introduction
ある言語のインタプリタを他の言語を使って書く場合、 対象言語の評価規則をホスト言語で定義する。 scalaの例
// scala // 講義:プログラミング言語処理系より簡略化して掲載 def eval (e: Exp): Value = e match { case IntExp(i) => IntVal(i) case BOpExp(op, e1, e2) => { val v1 = eval(e1) val v2 = eval(e2) (op, v1, v2) match { case (PlusOp, IntVal(i), IntVal(j)) => IntVal(i + j) // ...中略 } } }
eval関数が評価規則を定義しています。
ある言語の型規則を定義するには、 1つの方法 : 型検査器を書く
// scala // 講義:プログラミング言語処理系より簡略化して掲載 def tcheck (e: Exp) : Ty = e match { case IntExp(i) => IntTy case BOpExp(o, e1, e2) => { val t1 = tcheck(e1) val t2 = tcheck(e2) (o, t1, t2) match { case (PlusOp, IntTy, IntTy) => IntTy // ...中略 } } }
型検査器とインタプリタを別々に書くと
- 利点
- それぞれ独立に実行できる
- 欠点
dependently-typed definitional interpreter
依存型を使用することにより
- 型安全性の証明作業をホスト言語の型検査器に任せる (別個の型検査器が不要)
- 簡潔に書ける
- テストが簡単
この論文は
現実的に役に立つ言語のインタプリタを 依存型アプローチで書くことができるのか？
について実装しながら論じている。
依存型とは(あまり厳密ではない説明)
- 値をパラメータとして持つことができる型
- (例:) 2
3 行列の型 = Matrix 2 3
- (例:) 長さ 5 のリストの型 = List 5
依存型を使えば、行数・列数の条件も考慮した行列積を定義することができる。
-- 依存型なし product : Matrix -> Matrix -> Matrix -- 依存型 product : ∀ {i k j} -> Matrix i k -> Matrix k j -> Matrix i j
依存型はもっと強力な機能を持っていて、定理自動証明にも使われている。それは後に明らかになるだろう。
2. 単純型付きλ計算(STLC)のインタプリタ
ここからは最初に貼ったgithubリポジトリの src/STLC/Semantic.agda を見ながら読むことをおすすめする。
型と型環境の定義
bool型を加え拡張してみた。
-- Boolean open import Data.Bool -- 型 data Ty : Set where unit : Ty _⇒_ : (a b : Ty) → Ty int : Ty bool : Ty -- 型環境 Ctx = List Ty
STLCにおける型をAgdaでTy型の値として定義している。 型環境は名前で参照せず、de Bruijn indicesの番号に従う。
de Bruijn indices
- ラムダ計算において変数名を使わず引数を参照する記法
- 引数は、その引数をとるλ式が何階層外側にあるかを表す自然数の番号で表記する。 λz. (λy. y (λx. x)) (λx. z x) は λ (λ 1 (λ 1)) (λ 2 1) となる。
- 型環境はこの番号に対応する。
STLCの式
bool演算と比較演算とif式を加えて拡張してみた。
data Expr (Γ : Ctx) : Ty → Set where unit : Expr Γ unit -- () var : ∀ {t} → t ∈ Γ → Expr Γ t -- 変数 ƛ : ∀ {a b} → Expr (a ∷ Γ) b → Expr Γ (a ⇒ b) -- ラムダ式 _·_ : ∀ {a b} → Expr Γ (a ⇒ b) → Expr Γ a → Expr Γ b -- 関数適用 num : ℤ → Expr Γ int -- 整数 bool : Bool -> Expr Γ bool -- 真偽値 iop : (ℤ → ℤ → ℤ) → (l r : Expr Γ int) → Expr Γ int -- int演算 cop : (ℤ → ℤ → Bool) → (l r : Expr Γ int) → Expr Γ bool -- 比較演算 if : ∀ {t} → Expr Γ bool → Expr Γ t → Expr Γ t → Expr Γ t -- if式
見ての通り式の定義だ。
intrinsically-typed expression
訳: "本質的に型付けされている"
- 式自体が型を持っている。
値expがExpr Γ t型である
式と型導出の対応
例
_·_ : ∀ {a b} → Expr Γ (a ⇒ b) → Expr Γ a → Expr Γ b
このようにAgdaの型検査で、STLCの型規則の導出が自動で行われる。(すげえ！)
Scala
依存型がないScalaでの実装例
trait Exp case class IntExp(i: Int) extends Exp case class BoolExp(b: Boolean) extends Exp case class PlusExp(e1: Exp, e2: Exp) extends Exp // e1 + e2
Scalaでは
PlusExp(IntExp(1), VarExp(x))
がScalaの型検査を通ってしまう!
(もしx = boolだったら…? こんなに恐ろしいことはない)
- evalを実装するとき、このような例外を考慮しなければならない
- できることなら評価前(型検査)の段階で処理したい
依存型を使えば
iop _+_ (num 1) (var x)
が型検査の段階でエラーになる！(型環境によりvar xに型がつくので)
なんとすばらしい
intrinsically-typed values
値の定義です。 unit, 整数, 真偽値、関数だけです。
-- 相互再帰 mutual data Val : Ty → Set where unit : Val unit ⟨_,_⟩ : ∀ {Γ a b} → Expr (a ∷ Γ) b → Env Γ → Val (a ⇒ b) num : ℤ → Val int bool : B -> Val bool Env : Ctx → Set -- Γ内の各Ty値をValへインデックスさせたリストのようなもの Env Γ = All Val Γ
値環境のEnv型が型環境Γに依存している。
(All Val ΓとはΓ に map (t -> Val t)したようなものである。)
なる Val t型の値を値環境から調べることができる
(値環境から値を取り出した時、それがちゃんと型付けされている)
fuel argument
無限ループ対策
(Agdaには実行前に無限ループを検出してエラーを吐くことができます。
STLCは停止性を持つことが証明されていますが、
論文執筆当時のAgdaではそれを検出できなかったと思われます。今はどうなのかは検証して更新します)
eval n exp
- nがfuel argument
- evalが再帰的にevalを呼ぶとき、n-1を渡す
- eval 0 _ = timeout (燃料切れ)
燃料切れによる終了に対応するため、 evalの結果にはMaybeを使用する。
M : (Γ : Ctx) → (A : Set) → Set M Γ A = Env Γ → Maybe A -- (just a) >>= f == f a _>>=_ : ∀ {Γ a b} → M Γ a → (a → M Γ b) → M Γ b return : ∀ {Γ a} → a → M Γ a -- x -> just x getEnv : ∀ {Γ} → M Γ (Env Γ) -- 現在の環境を取得する usingEnv : ∀ {Γ Γ' a} → Env Γ → M Γ a → M Γ' a -- 指定した環境で計算実行 timeout : ∀ {Γ a} → M Γ a -- Nothing
評価関数 eval
評価規則を定義します。
eval : ℕ → ∀ {Γ t} → Expr Γ t → M Γ (Val t) eval zero _ = timeout -- 差分のみ eval (suc k) (bool b) = return (bool b) eval (suc k) (cop f l r) = eval k l >>= λ{ (num vl) → eval k r >>= λ{ (num vr) → return (bool (f vl vr)) }} eval (suc k) (if c e1 e2) = eval k c >>= λ { (bool true) → eval k e1 ; (bool false) → eval k e2 }
src/STLC/Examples.agda
-- テスト test-if : eval 5 (if (bool true) (num (+ 1)) (num (+ 2))) [] ≡ just (num (+ 1)) test-if = refl
なんとこのコードを型検査するだけでテストができてしまう。すげえ
何が起きているのか詳しい解説はここを読むといい。依存型がなんとなくわかっていれば読めるはずだ。
自己満足 list 拡張
差分のみ
data Ty : Set where list : Ty -> Ty data Expr (Γ : Ctx) : Ty → Set where nil : ∀ {t} → Expr Γ (list t) -- [] _cons_ : ∀ {t} → Expr Γ t -> Expr Γ (list t) -> Expr Γ (list t) data Val : Ty → Set where nil : ∀ {t} -> Val (list t) _cons_ : ∀ {t} -> Val t -> Val (list t) -> Val (list t) eval (suc k) nil = return [] eval (suc k) (x cons xs) = eval k x >>= λ{ v → eval k xs >>= λ{ l → return (v cons l)) }}
自己満足 match式
listの[] x::xs のパターンのみ
data Expr (Γ : Ctx) : Ty → Set where match : ∀ {t t'} → Expr Γ (list t) -> Expr Γ t' -> Expr (t ∷ ((list t) ∷ Γ)) t' -> Expr Γ t eval (suc k) (match e e1 e2) = eval k e >>= λ { nil -> eval k e1 ; (x cons xs) -> getEnv >>= λ E → usingEnv (x ∷ xs ∷ E) (eval k e2) }
中身の要素が一致していないlist
list型に中身に対応する型のリストを持たせます。
data Ty : Set where list : (List Ty) -> Ty data Expr (Γ : Ctx) : Ty → Set where nil : Expr Γ (list []) _cons_ : ∀ {t T} → Expr Γ t -> Expr Γ (list T) -> Expr Γ (list (t ∷ T)) head' : ∀ {t T} -> Expr Γ (list (t ∷ T)) -> Expr Γ t tail' : ∀ {t T} -> Expr Γ (list (t ∷ T)) -> Expr Γ (list T) data Val : Ty → Set where nil : Val (list []) _cons_ : ∀ {t T} -> Val t -> Val (list T) -> Val (list (t ∷ T)) eval (suc k) (head' e) = eval k e >>= λ { (x cons xs) -> return x } eval (suc k) (tail' e) = eval k e >>= λ { (x cons xs) -> return xs }
長くなりましたが、ここまで読んでくれた人、本当にありがとうございます。この先は難しいらしいですが、続きもやる予定なので、できる限り供養していきます。
