依存型を使った、型安全なMutable Stateを扱うインタプリタ(STLC+Ref)
PoPLの論文(Intrinsically-Typed Definitional Interpreters for Imperative Languages)についての輪講で、発表の際に使用したスライドの供養(ブログ用に多少修正は加えている)
初めての人は前回のおはなしをまず読んで欲しい
ソースコードはこれ github.com
正直この章はめちゃくちゃしんどかったが、がんばって噛み砕いで説明した。
実際この論文は本当によく書かれていて、多少前提知識がなくても気合いがあれば調べながら大筋は理解できるようになっている。
参考: - What is Agda? -- Agda docs
今回の趣旨
前回定義したSTLCに、 命令型言語にありがちな変更可能なデータの概念を導入する。
そのためにmutable dataを格納するためのストアを定義するが、 型安全性を保ちながらどのように実装するのかを紹介していく。
参照Syntax
OCamlに似た参照構文を導入する。
ポインタのようなものと考えればいいと思う。
重要な部分のみ抽出
data Ty where ref : Ty -> Ty -- Tyへの参照型 data Expr (Γ : List Ty) : Ty → Set where -- ref x : xへの参照 ref : ∀ {t} → Expr Γ t → Expr Γ (ref t) -- !(ref x) == x 参照先の値を取り出す !_ : ∀ {t} → Expr Γ (ref t) → Expr Γ t -- 参照先に値を代入 _≔_ : ∀ {t} → Expr Γ (ref t) → Expr Γ t → Expr Γ unit data Val : Ty → (Σ : StoreTy) → Set where loc : ∀ {Σ t} → t ∈ Σ → Val (ref t) Σ -- t型への参照
Val型は前回、Ty -> Set
(Tyでインデックスされた集合と呼ぶ) であったが、
今回参照型の値を導入するにあたり、加えてStoreTyでインデックスする必要がある。
StoreTyについてはこの後すぐに説明する。
well-typed store
前回の型環境と値環境の関係と同様
-- ストア型 StoreTy = List Ty -- well-typed store Store : (Σ : StoreTy) → Set Store Σ = All (λ t → Val t Σ) Σ -- ストアから値を取り出す lookup-store : ∀ {Σ t} → t ∈ Σ → Store Σ → Val t Σ lookup-store x μ = All.lookup μ x -- ストアの値を変更する。 update-store : ∀ {Σ t} → t ∈ Σ → Val t Σ → Store Σ → Store Σ update-store ptr v μ = μ All.[ ptr ]≔ v
これでストアの変更に対して型付けを保てるし、
ストアから抽出した値もしっかり型付けされていることが保証された(感動)。
実際の式のサンプル(イメージのため厳密なコードではない)
eval (ref (num 10)) [] [] === loc here -- ストアの最初の要素を示す eval (! (loc here)) [] [num 10] === num 10 eval (ref (num 10) ≔ num 11) [] [] === unit -- 評価後のストアは[num 11]となっている
Well-Typed Interpreterを目指して
前回、evalはこのように型付けされていた。
-- Section 2 -- モナド M : Ctx → Set → Set M Γ a = Env Γ → Maybe a eval : ℕ → ∀ {Γ t} → Expr Γ t → M Γ (Val t)
今回の目標として、evalをストアの変更に対して安全に型付けする必要がある。
第一の試み
regular indexed monad
結論からいうとこの方法はうまくいかない。
-- no good -- Σ : 評価時のストア型 -- Σ′ : 評価後のストア型 M : (Γ : Ctx) → (A : Set) → (Σ : StoreTy) → (Σ′: StoreTy) → Set -- M Γ a Σ Σ′ = Env Γ Σ → Store Σ → Maybe a たぶんこう -- evalは環境とストア eval : ℕ → ∀ {Σ Σ′ Γ t} → Expr Γ t → M Γ (Val t Σ′) Σ Σ′ -- M Γ (Val t Σ′) Σ Σ′ = Env Γ Σ → Store Σ → Maybe (Val t Σ′) たぶんこう
なぜうまくいかないのか、以下のような式の場合
let c = ref 42 in let d = if (x > 0) then c else ref 11 in !d
eval k (ref 42) : M [int] (Val (ref int)) Σ Σ′ : Maybe (Val (ref int) [int])
上の式はまだなんとか型付けできそうだが…
問題の式
eval k (if (x > 0) then c else ref 11) [x] [42] : Maybe (Val (ref int Σ')) (Σ'は任意)
評価後のストア型Σ′はxを評価するまでわからない (型検査の段階で決定不可能)
なのでこの後の!d
の型付けができない。これはまずい。
第二の試み
Monads over an Indexed Set
M : (Γ : Ctx) → (P : StoreTy → Set) → (Σ : StoreTy) → Set M Γ P Σ = (E : Env Γ Σ) → (μ : Store Σ) → Maybe (∃ λ Σ′ → Store Σ′ × P Σ′ × Σ ⊑ Σ′) -- Σ ⊑ Σ' <==> Σ is prefix of Σ' -- [1,3] ⊑ [1,3,5,7] eval : N → ∀ {Σ Γ t} → Expr Γ t → M Γ (Val t) Σ
∃ λ Σ′ → Store Σ′ × P Σ′ × Σ ⊑ Σ′
はAgda使いでなければ難しく考える必要はない、
「あるΣ′が存在して、Store Σ′ × P Σ′ × Σ ⊑ Σ′の値を返せる」くらいに思ってほしい。
evalの結果は、新しいストア と Val t Σ′、
それとΣ ⊑ Σ′型の値で Σ ⊑ Σ′ (Σ is prefix of Σ′)を保証する。
この定義で、さきほど問題になった式
let c = ref 42 in let d = if (x > 0) then c else ref 11 in !d
がうまく型付けできることを確認できる。
eval k (if (x > 0) then c else ref 11) : M [int, (ref int)] (Val (ref int)) [int] eval k (if (x > 0) then c else ref 11) [num x, loc here] [num 42] : Maybe (∃ λ Σ′ → Store Σ′ × P Σ′ × [num 42] ⊑ Σ′)
とりあえず型付けはできた。
bind
モナドにおいて大切なbindを定義する。
初めて登場した関数や演算子はすぐ後に説明する。
-- (_, Val t Σ′, _) >>= g _»=_ : ∀ {Σ Γ}{P Q : StoreTy → Set} → (f : M Γ P Σ) → (g : ∀{Σ′} → P Σ′ → M Γ Q Σ′) → M Γ Q Σ (f >>= c) E μ = case (f E μ) of λ{ nothing → nothing ; (just (_ , μ' , x , ext)) → case (c x (weaken-env ext E) μ') of λ{ nothing → nothing ; (just (_ , μ'' , y , ext')) → just (_ , μ'' , y , ext ⊚ ext') } }
f >>= g
fの新しいストア型をΣ′とする。
型検査の段階で、gに渡されるΣ′が具体的な値がわからないので、
gは任意のストア型に対し実装する。
ストア拡張に対する値・型環境の保存
-- x ∈ xs and xs ⊑ ys => x ∈ ys -- x ∈ xs -> x ∈ ys ∈-⊒ : ∀ {a}{A : Set a}{xs : List A}{x} → x ∈ xs → ∀ {ys} → ys ⊒ xs → x ∈ ys -- 値・環境が持つストアを拡張する mutual -- Val a Σ → Val a Σ' weaken-val : ∀ {a}{Σ Σ' : StoreTy} → Σ ⊑ Σ' → Val a Σ → Val a Σ' weaken-val ext unit = unit weaken-val ext (loc l) = loc (∈-⊒ l ext) weaken-val ext ⟨ e , E ⟩ = ⟨ e , weaken-env ext E ⟩ weaken-val ext (num z) = num z -- Env Γ Σ 内の各 Val t Σ を Val t Σ'にする。 weaken-env : ∀ {Γ}{Σ Σ' : StoreTy} → Σ ⊑ Σ' → Env Γ Σ → Env Γ Σ' weaken-env ext (v ∷ vs) = weaken-val ext v ∷ weaken-env ext vs weaken-env ext [] = [] -- 推移律 _⊚_ : ∀ {Σ Σ′ Σ′′ : StoreTy} → Σ ⊑ Σ′ →Σ′ ⊑ Σ′′ → Σ ⊑ Σ′′
個人的にここは言葉で説明するよりコードを眺めた方が理解しやすいと思っている。
ポイントは、 Σ ⊑ Σ' なる拡張を行っても、値や環境の、本質的な型や中身は変わらないこと。
weakenのような操作を弱化というらしい。
上記を踏まえてもう一度bindの定義を見てみよう。
-- bind _>>=_ : ∀ {Σ Γ}{p q : StoreTy → Set} → (f : M Γ p Σ) → (g : ∀ {Σ'} → p Σ' → M Γ q Σ') → M Γ q Σ (f >>= c) E μ = case (f E μ) of λ{ nothing → nothing ; (just (_ , μ' , x , ext)) → case (c x (weaken-env ext E) μ') of λ{ nothing → nothing ; (just (_ , μ'' , y , ext')) → just (_ , μ'' , y , ext ⊚ ext') } }
μ'' , y , ext' ∈ Store Σ′ × P Σ′ × Σ ⊑ Σ′
weaken-env ext E
環境E : Env Γ Σ の ストアμをμ'で拡張
ext ⊚ ext'
μ ⊑ μ''の証明
storeの操作
-- ストアに格納 append store : ∀ {Σ t Γ} → Val t Σ → M Γ (Val (ref t)) Σ store {Σ} {t} v _ μ = let ext = ∷ʳ-⊒ t Σ v' = loc (∈-∷ʳ Σ t) μ' = (All.map (weaken-val ext) μ) all-∷ʳ (weaken-val ext v) in just (_ , μ' , v' , ext) -- ストアから参照 deref : ∀ {Σ Γ t} → t ∈ Σ → M Γ (Val t) Σ deref x E μ = return (All.lookup μ x) E μ -- ストアの更新 update : ∀ {Σ Γ t} → t ∈ Σ → Val t Σ → M Γ (Val unit) Σ update x v E μ = return unit E (update-store x v μ)
今までの議論から、これらの操作が型安全性を保ったまま実行できることに感動してほしい。
updateについて、githubのコードにはλ _ → ⊤
などと書いているが上記に書き換えても型チェックは問題なく通った。こちらの方がわかりやすいだろう。
(storeの中身について解説する余裕はない)
問題
これでめでたしめでたしとはならなかった…
以下のケースが問題である。
eval (suc k) (e1 · e2) = eval k e1 »= λ{ ⟨e,E⟩ → eval k e2 »= λ v → usingEnv (v :: E) (eval k e) }
vとEのインデックスされているStoreTyが矛盾
-- 例 -- (λx. x) $ (&10) -- (ƛ var here) · (ref (num 10)) eval (suc k) (ƛ var here) [] [] ≡ ⟨(var here), []⟩ -- (E ≡ []: Env [] []) eval (suc k) (ref (num 10)) [] [] ≡ loc here -- (v ≡ loc here : Val (ref int) [int])
E is indexed by [], v is indexed by [int]
これに対し結合演算v :: E
を行うのはEnv定義に合わない。
原因
先ほど述べた通り、f >>= g
のgが任意のストア型に対し実装されているが、
そのgがΣ ⊑ Σ′の仮定を知らない(受け取っていない)。
v :: E
のEにweaken-env ext'を通したいので、gに渡されるストア型の仮定が必要となる。
第三の試み
f >>= g
のgに仮定を渡すようにする
_»=_ : ∀{Σ Γ}{P Q : StoreTy → Set} → (f : M Γ P Σ) → (g : ∀ {Σ′} → Σ ⊑ Σ′ → P Σ′ → M Γ Q Σ′) → M Γ Q Σ
-- before eval (suc k) (e1 · e2) = eval k e1 »= λ{ ⟨e,E⟩ → eval k e2 »= λ v → usingEnv (v :: E) (eval k e) } -- after eval (suc k) (e1 · e2) = eval k e1 »= λ{ ext ⟨ e , E ⟩ → eval k e2 »= λ{ ext′ v → usingEnv (v :: (weaken-env ext′ E)) (eval k e) }}
>>=
の左側に渡す情報が増える。- 言語が複雑になるほど書くのが大変になる。
- 要するに汚い
Dependent-Passing Style
できれば、extなんか渡さずにかければいい。
それを実現するため、Dependent-Passing Styleというものを紹介する。
課題
eval (suc k) (e1 · e2) = eval k e1 »= λ{ ext ⟨ e , E ⟩ → eval k e2 »= λ{ ext′ v → usingEnv (v :: (weaken-env ext′ E)) (eval k e) }}
最後の行で呼ばれるEは、2行目で渡されたE。
最後のλ関数にとっては自由変数である。
これを束縛すれば綺麗になりそうだ。
>>=
に渡す関数をStoreTy indexに関して閉じれば、weakenをカプセル化することができる。
目標のコード
eval (suc k) (e1 · e2) = eval k e1 »= λ{ ⟨ e , E ⟩ → (eval k e2 ^ E) »= λ{(v , E)→ usingEnv (v :: E) (eval k e) }}
(eval k e2 ^ E) »= λ{(v , E) →
の(v,E)について
vとEが同じストア型でインデックスされていることを保証するデータ型
-- 同じ StoreTy でインデックスされる述語のpair data _⊗_ (P Q : StoreTy → Set) : (Σ : StoreTy) → Set where _,_ : ∀ {Σ} → P Σ → Q Σ → (P ⊗ Q) Σ
f >>= g
のg : ∀ {Σ'} → p Σ' → M Γ q Σ'
はStoreTyでインデックスされる述語全般を受け取るので、
gとしてλ{(v , E)→ ...}
を与えることができる。(よくできている)
また、_^_
演算子
-- Q Σ を M Γ Q Σ にliftする(モナド用語) _^_ : ∀ {Σ Γ}{P Q : StoreTy → Set} → ⦃ w : WeakenableQ ⦄ → M Γ P Σ → Q Σ → M Γ (P ⊗ Q) Σ (f ^ x) E μ = case (f E μ) of λ { nothing → nothing ; (just (Σ , μ' , y , ext)) → just (Σ , μ' , (y , weaken ext x) , ext) }
⦃ w . Weakenable Q ⦄ は、Weakenable Q のインスタンスが存在することを保証する、すごい引数。 今からこれを詳しく見ていこう。
Weakenable は弱体化関数を定義するレコード型。
record Weakenable {i j}{A : Set i}(p : List A → Set j) : Set (i ⊔ j) where field wk : ∀ {w w'} → w ⊑ w' → p w → p w' instance any-weakenable : ∀ {x : A} → Weakenable (λ xs → x ∈ xs) all-weakenable : ∀ {j} {B : Set j} {xs : List B} → ∀ {k} {C : B → List A → Set k} {{wₐ : ∀ {x} → Weakenable (C x)}} → Weakenable (λ ys → All (λ x → C x ys) xs) list-weakenable : ∀ {b}{B : List A → Set b} → {{wb : Weakenable B}} → Weakenable (λ W → List (B W)) weaken : ∀ {i}{p : List Ty → Set i}⦃ w : Weakenable p ⦄ → ∀ {Σ Σ'} → Σ ⊑ Σ' → p Σ → p Σ' weaken ⦃ w ⦄ ext v = Weakenable.wk w ext v
(eval k e2 ^ E) »= λ{(v , E) →
の例では
Weaknable (Env Γ)
つまり
Weaknable (Σ : StoreTy) → All (λ t → Val t Σ) Γ
に対して検索が行われ、all-weakenableが対応する。
all-weakenableの中でまた
Val t
のインスタンス検索が入る。以下の宣言が対応する。
instance weaken-val' : ∀ {t} → Weakenable (Val t) weaken-val' = record { wk = weaken-val }
以上のプロセスで、環境が弱体化可能なのか、その証明を自動的に行ってくれる。すげえええええ。
ここまでの議論を踏まえて、
目標のコード
eval (suc k) (e1 · e2) = eval k e1 »= λ{ ⟨ e , E ⟩ → (eval k e2 ^ E) »= λ{(v , E)→ usingEnv (v :: E) (eval k e) }}
これが問題なく動くことを確認してほしい。bindの左側の関数にextを渡す必要もなくなり、かなりきれいになった。
Dependent-Passing Styleのこのインタプリタは、 非依存型のMonadicインタプリタと同じ構造をしている。
しかし、以下の点が違う。
- 型規則を破るようなCaseを考慮する必要がないので設計者は楽できる。
_^_
を使って>>=
をまたいで値を運ぶことができる。(先ほどの例ではEを運ぶことができた。)
ここからはおまけみたいなものである。
これから話すことで、実装上の進展はない、しかもちょっと難しいので、無理して読まなくても大丈夫だと思う。
ここまで読んでくれただけで十分ありがたい。
今まで弱体化を ⊑ 型の値を使って明示的に取り扱ってきたが、型クラスの自動証明検索によって暗黙の弱体化をできないだろうか。
_⊑_
の型クラス化
record IsIncluded (W W' : Carrier) : Set ℓ₂ where field is-included : W ⊑ W' record IsIncludedOnce (W W' : Carrier) : Set ℓ₂ where field is-included-once : W ⊑ W'
instance -- W ⊑ W is-included-refl : ∀ {W} → IsIncluded W W is-included-refl = record { is-included = refl } -- W ⊑ W' -> W' ⊑ W'' -> W ⊑ W'' is-included-step : ∀ {W W' W''} ⦃ p : IsIncludedOnce W W' ⦄ ⦃ q : IsIncluded W' W'' ⦄ → IsIncluded W W'' is-included-step {{p = record { is-included-once = p }}} {{record { is-included = q }}} = record { is-included = trans p q }
IsIncludedOnceは単一の拡張事実として、自分で与えることになる。
IsIncludedは、IsIncludedOnceの反射的・推移的閉包であるといえる。
次のように改めてWeaknableを定義してみる。
record Weakenable {i}(I : Carrier → Set i) : Set (i ⊔ ℓ₂ ⊔ c) where field weaken : ∀ {W W'} → W ⊑ W' → I W → I W' wk : ∀ {W W'} → I W → ⦃ p : IsIncluded W W' ⦄ → I W' wk x ⦃ record { is-included = p } ⦄ = weaken p x
しかし残念ながら今は、これはうまくいかない。
Agda (v2.5.3)は、証明検索中のインスタンスの重複をサポートしていない。
つまり、2通りの証明があると落ちる。 (included-reflとincluded-stepのどちらを選択するかなど)
ちなみに前に紹介したWeaknable Envは見た通り1本道の証明になっていたと思う。
それに、Agda, Idris, Coqでは証明検索の仕様が異なる。
よって他の依存型言語に移植することは難しい。
ここからは今まで定義した型や演算子の圏論的側面を説明する。ほんとに読まなくてもいいよここは。私もよくわかってない。
強モナドと強度
強度(strength)という関数が重要
-- 強モナド class StrongMonad m where return :: a -> m a (>>=) :: m a -> (a -> m b) -> m b strength :: (a, m b) -> m (a, b)
先ほどのモナドを一般化する。
indexed setのモナド
ISet = (Σ : StoreTy) → Set M : (Γ : Ctx) → (A : ISet) → ISet
Weakenableを導入
(P : StoreTy → Set)に対し Weakenable P のインスタンスが存在
-- equivalent to -- M : ∀ {i}(Γ : Ctx) → (p : StoreTy → Set i) → (Σ : StoreTy) → Set i -- M Γ p Σ = Env Γ Σ → Store Σ → -- Maybe (∃ λ Σ' → Store Σ' × p Σ' × Σ ⊑ Σ') -- Weakenableな(StoreTy → Set) WSet = (∃ λ (P : StoreTy → Set) → Weakenable P) M′ : (Γ : Ctx) → (A : WSet) → WSet M′ Γ A = (Σ : StoreTy) → Env Γ Σ → Store Σ → Maybe (∃ λ Σ' → Store Σ' × p Σ' × Σ ⊑ Σ')
indexed setの 直積と射が定義できる。
-- 直積 _⊗_ : WSet → WSet → WSet (P ⊗ Q) Σ = (P Σ × Q Σ) -- 射(要は写像です) _⇒_ : WSet → WSet → Set P ⇒ Q = ∀ {Σ} → P Σ → Q Σ
ここで筆者が言いたそうにしているのは、
_^_
演算子が、強度(strength)と同じ構造をしていることである。
おそらく、このインタプリタの設計には理論的裏付けがあることをアピールしたいのではないだろうか。
-- _^_ : ∀ {Σ Γ}{p q : StoreTy → Set} → ⦃ w : Weakenable q ⦄ → -- M Γ p Σ → q Σ → M Γ (p ⊗ q) Σ -- strengthと同じ構造 -- strength :: (a, m b) -> m (a, b) _^_: {Γ : Ctx} {P Q : WSet} → (P ⊗ M′ Γ Q) ⇒ M′ Γ (P ⊗ Q) (x ^ f) E μ = case (f E μ) of λ { nothing → nothing ; (just (Σ , μ' , y , ext)) → just (Σ , μ' , (y , weaken ext x) , ext) }
また、WSetがWeaknableを仮定しているので、_^_
演算子を証明検索を用いずに定義することができている。
後に、M'のより単純な形が強モナドを形成することを証明している。
しかし、そのスタイルのインタプリタを作るのは 実用的でない。
- Agda標準のサポートがない
今後の課題:
この論文が出てから2年が経過し、強モナドをサポートするライブラリがAgdaにあったので、何らかの進展があったかもしれないね。
以上、ここまで読んでくれた人、本当にありがとうございました。輪講は終わりましたが、続きが気になるのでまたまとめてアップするかもしれません。