依存型による単純型付きλ計算(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 }
長くなりましたが、ここまで読んでくれた人、本当にありがとうございます。この先は難しいらしいですが、続きもやる予定なので、できる限り供養していきます。
左折ができる男
昨日の分もまとめて
前回の狂気に記した問題はほぼ解決した。が、そこに全神経をぶち込んでいるため次の行動のためのアクションが遅れ気味。
今日の技能は坂道と右折とバックとクランク。毎日毎日知らん人間にミスを指摘され続けるのは普通に苦行。指摘されること自体はいいんだが車動かしながら一瞬で理解できる解決策を示してもらえないのがしんどい、癖直そうとすれば別のところがおろそかになるし。
効果測定は余裕だった。運転もこれくらい楽ならいいのに。
マリカ買うかぁ…
そういえば
今日は時間があったのでCoPLを進めた、今4章の途中。これをやると精神が落ち着くので操作的意味論には抗うつ効果があるのかもしれない
うわああああああああああああ
昨日朝から技能とか言ってたけどスケジュール読み間違えてたぜ
学科だらけの日曜日、もう顔中知識まみれや
もう車乗るの?マジ?ぶつけちゃうよ?
カーブができん!!!!!!愛想笑いがつらい!!!!!!やだ!やだ!もう無理
- タイヤがどこにあるのかわからん
- ハンドル切るタイミングがわからん
- ハンドルの切る具合がわからん
- ブレーキの踏み込み具合がわからん
- 走行中に考えることが多すぎる
- 話しかけてくるな
- 頼む1人で試行錯誤させてくれ
くそが
日記9/5
今日から車校です、嫌だねえ
昼頃からオリエンテーション・適性検査、そのあと学科が2つ。
適性検査の悪意ある抜粋
(いいえって答える奴の方がヤバイと思いませんか?)・消えたいと思うことがある……はい
— opfer.negative (@opfer_10155) September 5, 2020
・ときどき憂鬱になって死にたくなる……はい
・世の中が嫌になることがある……はい
- 学科1
1を取らないと他の学科は受けられないらしい。内容は学科の注意事項とか免許取得までの流れとか、オリエンテーションの補足っぽい感じだった。
講習はちゃんとマジメに"50分"受けないと講習受けた扱いにならないらしい(単位が来ない的な)。
「ちゃんとマジメに50分受けた」の判断基準が厳しい、途中入退室は(トイレだろうが)再履、居眠り・内職・スマホは即退出させられて再履。大学のスタイルになれているとオーバーに感じるかもしれないが人を轢き殺せるモノの免許だしまあ納得はできる。pcでノートをとるのも無理そうだが、教本に書き込めばいい程度の内容ぽいし大丈夫だろ
授業中にtwitterを見られないのはちょっと寂しい(そんな余裕はマジでないんだが)
- 学科10
免許の種類とか更新とか大型特殊自動車とかの定義。みんなこんなん覚えてんの?
帰りはひでえ雨だったし結構疲れた。はよ終わって欲しい
明日は朝から技能です
日記 ~9/4
やってしまいました。実に一週間半も日記をサボってしまいました。
もう細かいことは覚えてないのでざっくりになります。
- Reactでグラフ書いたり色々
- CopL あんまり進んでなくて今3章の途中です
- 車校の入校手続き
- MGS5 たのしー
- 高校同期とZoom飲み
- 久々に顔を見ることができてよかったんだが、なぜ全員服を脱いでいたのか…
- opferちゃんの中に入りました。相変わらずかわいいね
- 先輩and同期とカラオケand麻雀
- 昨日のことだから覚えてる
- 先輩とカラオケする経験はほとんどなかった(はずだ)が全然歌えた。選曲に困らないのが東工大のいいところである。私が成長したということもあるけどな。
- 同期くん、麻雀では降りることを知らないツッパリ野郎だからメチャクチャにカモられて半荘5回で-140点とかえらいことになってた
- 今回は私が1位よ。
これしか思い出せん、なんと空虚な人生。
opferちゃん「さてopferさん、サボったペナルティは受けてもらいますよ」 \そ、そんな…
車校出るまで毎日日記書くことになりました。
日記 ~8/26
8/24(月)
8/25(火)
- 昼起床
- カルビとウィンナーを焼いて焼肉のタレをかけるとうまいぞ
- CoPL 2章の半分くらい
- 某書類に不備があり返送されていた、クソ、訂正して郵便局へ。
- ある居酒屋の感動メニューのパクリ
これをこうしてこう! pic.twitter.com/oqcxJwZWII
— opfer.negative (@opfer_10155) August 25, 2020 - MGS5
8/26(水)
- 昼起床
- CoPL 2章
- 今日は薬を飲まずに元気でいよう
- 今日の夜から二日間雨が降るらしい(信頼度低)ため、買い物
- 友人とバッタリ、久しぶりに話せてよかった。また飲みに行きたい(反省0)
- 社会人に数学を教えた