\LaTeXはもう古い！令和の組版処理システムは\SATySFiで決まり！
Abstract
TeXのような組版処理システムは、ユーザーが書いたマークアップ言語を処理して、PDFを生成するシステムである。特にTeXは、理工系分野において論文、レポート、スライドなどの用途に広く用いられており、理系大学の新入生たちの一定数が、悪いお兄さん達にそそのかされてTeXを使い始めるケースが多い。しかしTeXにはユーザーにとって不親切な点がいくつか存在する。TeXを書くことはしばしば苦痛であり、ゆえに脱TeXの流れはもっと大きくなってもいいと考える。そこで、これからレポートを書くのにTeXを使おうと思っている人や、今までTeXばかりを使ってきて、他の選択肢を検討したこともない人のために、もっと悪いお姉さんであるところの私が、環境構築も簡単かつTeXの欠点を克服したシステムを持つSATySFiをここで紹介する。
SATiSFiは以下に1つでもあてはまる人におすすめである。
- TeX の わかりにくいエラーメッセージにうんざりしている
- プログラミングが好きな人 (特に関数型プログラミングに興味がある人)
- これから組版システムを使い始める人
- TeXを使っている人
SATySFiの特徴
SATySFiはTeXと同様、専用のマークアップ言語で書かれたファイルを読み込んでPDFを生成する。ではTeXとの違いは何なのだろうか。
SATySFiの最たる特徴は、マークアップ言語が関数型言語のような性質を持つことで、以下のような機能が実現されていることである。
- 独自の型システムにより、エラーの発生位置や原因が、より正確に報告される
- 自作コマンドの定義が、TeXより容易で、かつ読みやすい。
1つ目の機能だけで十分魅力的であるが、2つ目も強力である。自作コマンドは、文書に何度も出てくる何らかの装飾を施したフレーズをコマンド1発で呼び出すことができ、それゆえタイプ量も減るというわけだ。SATySFiのコマンド定義は、プログラミングに慣れ親しんだ人間にとっては簡単であり、型検査によって自分が犯したミスもちゃんと教えてくれる。
入門
SATySFiは入門のための資料が十分に揃っている。
インストール
opam を使ってインストールすると、外部ライブラリを使えるのでこっちがおすすめ。スライドも作れるようになる。
- satyrographos: github.com
標準ライブラリだけでも十分使用に耐えるだろう。上のが難しかったら、SATySFi wiki に リンクが貼ってあるので、Win/Mac/Linux どれでも問題なく簡単にできるはずだ。
- SATySFi wiki github.com
マニュアル
記事投稿時点で、BoothにてSATySFiの日本語公式マニュアルがなんと無料で配布されている。このマニュアルの3章まで読めば、普段のレポート作成に困ることはほとんどないだろう。
エディタ
VSCodeしか勝たん。SATySFiのための便利な拡張機能がある。
まとめ
私はスライド作りに使ってみたが、TeXに比べて「プログラミングをしている」という感覚が強かった。型システムによってエラーがわかりやすいのはとてもありがたい。satyrographosのようなパッケージ管理が標準で入ってくるともっと良いのだが。
興味が湧いたら是非とも1度試してみてほしい。実はこんな記事を書いたのはみんなが使ってSATySFi人口が増えれば、ライブラリとか環境とかの開発が盛んになると思ったから。(他力本願寺)
References
SATySFi wiki github.com
satyrographos github.com
SATySFi公式マニュアル PDF版 booth.pm
私が松屋よりウマいネギ塩豚丼を作れることの構成的証明 [Constructive proof that I can make a better "Pork Bowl with salt and green onions" than Matsuya.]
今月も真面目な記事を書く余力は残っていなかった。だって疲れるし…
3月はきっと少しくらい余裕ができるといいなあ。
さて今月はタイトルにもある通り「私が松屋よりうまいネギ塩豚丼を作れること」を構成的に証明します。別に松屋に恨みとかないですホント。
まず豚バラ肉を塩コショウで普通に焼きます。アブラがいっぱい出てくるのはエロくてドキドキしますね(高血圧)。
余ってる野菜確認したら、なんとネギがない(は？)、玉ねぎで代用します。
千切りキャベツと一緒にフライパンにぶち込みます。本当はキャベツは生が好きですが、我が家の衛生環境的に考えて危険と判断。
先行研究[1]に従い塩ダレに必要な調味料を投入し、しばらく加熱。
以上の2品を白米の上にのっけます。そうして得られた豚丼が以下です。
卓上のラー油やレモン汁によく合います。こりゃウマイ、勝ったな。Q.E.D 証明終了。
参考文献
チキンステーキ
最近は課題とかライザ２やったりとかで濃い記事を書く時間が年末年始くらいしかなかったので、今月はまだ投稿してないらしい。
ガチ記事を書く余力ないし、飯ブログとか書いてみたくなった。
そんなわけで今日の昼飯。
所詮自炊なので面倒なことはしない。
鶏肉2枚をバターで焼いていく。
両面焼けたらバター、ウスターソース、ケチャップ、ワイン、砂糖をまぜまぜでソースを作ってぶち込む。余ってた玉ねぎをぶち込んでみる。
このまましばらく煮詰める。この間にパスタ麺を茹でる。経験上ソースを余らかすので、パスタ麺に絡めてやるって寸法よ。
(盛り付け汚ねえな)
なんかナポリタンみたいになっちゃったなあ、そういえばパンチョのナポリタンを食いに行きたい。
鶏肉はいつも通りうまい。それにしてもパスタ麺がソースと絶妙にマッチしている、大成功だ。粉チーズを切らしていたのが非常に惜しい。
自炊だから手抜きするけど、おいしく出来上がるってのは大前提。家の中でも店の中でも、飯食ってるときって、「うまいうまい」ってことだけ考えながらニヤニヤしたいわけですよ。あ、ニヤニヤするのは家の中だけにしようね。
スコープとフレームを使った変数束縛
PoPLの論文(Intrinsically-Typed Definitional Interpreters for Imperative Languages)についてのまとめ
初めての人は最初の記事をまず読んで欲しい
ソースコードはこれ
github.com
参考: - 束縛変数 --筑波大学
スコープグラフ(scope graph)は静的束縛(lexical binding)と 動的束縛(non-lexical binding)の両方をサポートする静的名前解決の統一的アプローチ(uniform approach)です。
今回は、スコープグラフとヒープフレームをIntrinsically-Typed Definitional Interpreterに導入するためのライブラリを説明します。
lexical binding と non-lexical binding
参考 - lexical binding では スコープと変数の束縛関係が、プログラムを書いたときに決まる。ほとんどのプログラミング言語がこのスタイル。
- non-lexical binding では スコープと変数の束縛関係が、プログラムの実行順序で決まる。emacs-lispなど、ごく一部で使われている。身近な例だとJavaScriptのthisとか
具体例を見た方がわかりやすいです。 以下のようなコードを考えます。
let x = 1 in let f = fun _ -> print x in let x = 2 in f()
この実行によって得る出力を考えてみます。
lexical bindingでは1
(fが定義されているのがx = 1のスコープだから)
non-lexical bindingでは2
(fのprint xが実行されるのはx = 2のスコープだから)
を得ます。
スコープグラフ
スコープグラフは以下のnodeとedgeで構成される有向グラフです。
- 宣言edgeは、変数xがスコープkで宣言されていることを示します。
- スコープedgeは、スコープk'の宣言がスコープkから到達可能であることを示す。
- 参照edgeは、xがスコープkにて解決されることを示します。
これらを踏まえて例を見ます。
以下の図は(\x -> \y -> x $ y) $ (\z -> z)に対応するlexical bindingのスコープグラフです。
スコープ0はグローバルスコープです。ラムダ関数を宣言すると、新しくスコープができて、仮引数が宣言nodeになり、関数のbodyで呼ばれる変数が参照nodeとして現れています。ほとんどのプログラミング言語にあるスコープの概念と自然に結びつきます。
let x = 1 in let f = fun _ -> print x in let x = 2 in f()
名前解決
グラフ内の参照nodeから、同名の宣言nodeへのパスを構築することで解決されます。
図3の例では、xの参照nodeからスコープ2、スコープ1のnodeをたどって、宣言node xに到達します。
解決パスは 参照node --> スコープnode --> ... --> スコープnode --> 宣言node のような列で構成されます。
- de Bruijn indices
- 各スコープにつき1つの宣言
- lexical scopeに対応
- Scope Graph
- 1つのスコープに複数の宣言
- lexical, non-lexical両対応
前回のインタプリタを型環境の代わりにスコープグラフを使って書き直すことができます。
パラメータ付きのモジュールという面白い機能があります。モジュールをimportするときに自然数値と型の集合を与えることで、モジュール内のパラメータkとTyはその値を参照します。
module ScopesFrames.ScopesFrames (k : ℕ) (Ty : Set) where -- 型シノニム Scope = Fin k Graph = Scope → (List Ty × List Scope)
Scopeの識別子はkより小さい自然数とします。kはスコープnodeの数です。
Graphは、スコープ識別子と、そのスコープnodeから出る宣言edgeとスコープedgeの対応です。参照nodeはvar式によって作られるので必要ありません。
ここでは、解決パスの構造を定義します。
module UsesGraph (g : Graph) where -- declsOf s スコープsの宣言ノードの型のリスト declsOf : Scope → List Ty ; declsOf s = proj₁ (g s) -- edgesOf s スコープsから出るスコープedgeの行き先のリスト edgesOf : Scope → List Scope ; edgesOf s = proj₂ (g s) -- s ⟶ s' 型 スコープsからs'へのパス data _⟶_ : Scope → Scope → Set where [] : ∀ {s} → s ⟶ s _∷_ : ∀ {s s' s''} → s' ∈ edgesOf s → s' ⟶ s'' → s ⟶ s'' -- パスの結合 concat : ∀ {s s' s''} → s ⟶ s' → s' ⟶ s'' → s ⟶ s'' -- s ↦ t 型 スコープsからt型の宣言ノードへのパス(解決パス) data _↦_ (s : Scope) (t : Ty) : Set where path : ∀{s'} → s ⟶ s' → t ∈ declsOf s' → s ↦ t -- パスの結合 prepend : ∀ {s s' t} → s ⟶ s' → s' ↦ t → s ↦ t
Scopes and Frames
前回までの型環境Ctxと環境Envのように、スコープグラフを使って値をwell-typedに格納するには、スコープグラフに対応するメモリ構造が必要です。ここで、そのためのヒープとフレームを定義します。
フレームは基本的なメモリブロックであり、各フレームはスコープグラフのスコープによって型付けされます。実行時には、フレームはヒープ内に存在し、ヒープ内の各位置がフレームとなります。 ヒープ内の各位置（フレーム）が（スコープによって）型付けされている場合、ヒープは型付けされていると言います。
ヒープ型は、フレームに対応するスコープのリストです。
HeapTy = List Scope
Frame型
フレーム型は、ヒープ内の対応するスコープの位置で表現されます。
Frame : (s : Scope) → (Σ : HeapTy) → Set Frame s Σ = s ∈ Σ
Slots型
宣言ノードに対応する型付けされた値を格納する。
-- dsはスコープの宣言node Slots : (ds : List Ty) → (Σ : HeapTy) → Set Slots ds Σ = All (λ t → Val t Σ) ds
Links型
スコープedgeに対応する。
-- esはスコープから出るスコープedgeの行き先の列 Links : (es : List Scope) → (Σ : HeapTy) → Set Links es Σ = All (λ s → Frame s Σ) es
HeapFrame
HeapFrame型は、スコープsに対応するフレームが持つSlotsとLinksの組によって型付けされる。
HeapFrame : Scope → HeapTy → Set HeapFrame s Σ = Slots (declsOf s) Σ × Links (edgesOf s) Σ -- i.e. ([decls], [scopes])
Well-Typed Heap
Heap内のすべてのフレームがHeapFrameを型付けするとき、Well-Typedである。
各フレームがスコープによって型付けされているヒープのことです。
Heap : (Σ : HeapTy) → Set Heap Σ = All (λ s → HeapFrame s Σ) Σ -- i.e. [ ([decls0], [scopes0]), ([decls1], [scopes1])] -- scope0のフレーム scope1のフレーム -- List (List Ty × List Scope)
ヒープ型は、メモリ内の各フレームがスコープグラフのスコープによって記述されていることを保証します。
FrameのWell-Typed Functions
-- ヒープh内のフレームfから宣言dに対応するt型の値を取り出す。 getSlot : ∀ {s t Σ} → t ∈ declsOf s → Frame s Σ → Heap Σ → Val t Σ getSlot d f h with (All.lookup h f) ... | (slots , links) = All.lookup slots d -- ヒープh内のフレームfの宣言dのスロットにt型の値vをセットした新しいヒープを返す -- スロットの上書きが可能(mutable storeに応用できるので、後で拡張する) setSlot : ∀ {s t Σ} → t ∈ declsOf s → Val t Σ → Frame s Σ → Heap Σ → Heap Σ setSlot d v f h with (All.lookup h f) ... | (slots , links) = h All.[ f ]≔ (slots All.[ d ]≔ v , links) -- フレームfと繋がっているフレームを取得 getLink : ∀ {s s' Σ} → s' ∈ edgesOf s → Frame s Σ → Heap Σ → Frame s' Σ getLink e f h with (All.lookup h f) ... | (slots , links) = All.lookup links e -- フレームfからフレームf'へのLinkを作成(スコープグラフ上のスコープedgeの存在を仮定) setLink : ∀ {s s' Σ} → s' ∈ edgesOf s → Frame s' Σ → Frame s Σ → Heap Σ → Heap Σ setLink e f' f h with (All.lookup h f) ... | (slots , links) = h All.[ f ]≔ (slots , links All.[ e ]≔ f') -- フレームfからLinkを辿って、フレームf'を返す getFrame : ∀ {s s' Σ} → (s ⟶ s') → Frame s Σ → Heap Σ → Frame s' Σ getFrame [] f h = f getFrame (e ∷ p) f h with (All.lookup h f) ... | (slots , links) = getFrame p (All.lookup links e) h -- getSlotの略記関数(shorthand function) getVal : ∀ {s t} → (s ↦ t) → ∀ {Σ} → Frame s Σ → Heap Σ → Val t Σ getVal (path p d) f h = getSlot d (getFrame p f h) h -- setSlotの略記関数(shorthand function) setVal : ∀ {s t Σ} → (s ↦ t) → Val t Σ → Frame s Σ → Heap Σ → Heap Σ setVal (path p d) v f h = setSlot d v (getFrame p f h) h
initFrameは読むのが大変だった
-- initFrame: グラフ上のスコープsに対応するフレームをslotsとlinksで初期化する(新しく作る)。 -- 以下のコメントは演算の意味を説明するためのもので、厳密な式として正しくありません。雰囲気だけ感じ取ってください -- xs ∷ʳ x = [...xs, x] (append) -- ∷ʳ-⊒ xs x => (xs ∷ʳ x) ⊒ xs = xs ⊑ (xs ∷ʳ x) -- ∈-∷ʳ Σ s => s ∈ (Σ ∷ʳ s) -- Heap Σ all-∷ʳ HeapFrame s (Σ ∷ʳ s) => Heap (Σ ∷ʳ s) -- wkはrecord Weaknableの要素で、この場合、以下が対応する。 -- wk: bs ⊑ cs → All (λ x → C x bs) xs → All (λ x → C x cs) xs initFrame : (s : Scope) → ∀ {Σ ds es}⦃ shape : g s ≡ (ds , es) ⦄ → Slots ds Σ → Links es Σ → Heap Σ → Frame s (Σ ∷ʳ s) × Heap (Σ ∷ʳ s) initFrame s {Σ} ⦃ refl ⦄ slots links h = let ext = ∷ʳ-⊒ s Σ -- heap extension fact f' = ∈-∷ʳ Σ s -- updated frame pointer witness h' = (wk ext h) all-∷ʳ (wk ext slots , wk ext links) -- extended heap in (f' , h') -- 初期化するフレームfのslotsに、f自身に依存する値(例: fへのポインタ)を格納するケースに対応するため、 -- slotsの代わりに Frame s (Σ ∷ʳ s) → Slots ds (Σ ∷ʳ s) である関数slotsfを受け取る initFrameι : (s : Scope) → ∀ {Σ ds es}⦃ shape : g s ≡ (ds , es) ⦄ → (slotsf : Frame s (Σ ∷ʳ s) → Slots ds (Σ ∷ʳ s)) → Links es Σ → Heap Σ → Frame s (Σ ∷ʳ s) × Heap (Σ ∷ʳ s)
Definitional Interpreter for STLC using Scopes and Frames
式を型環境でなくスコープでインデックスします。
module Syntax (g : Graph) where open UsesGraph g data Expr (s : Scope) : Ty → Set where unit : Expr s unit var : ∀ {t} → (s ↦ t) → Expr s t ƛ : ∀ {s' a b} → ⦃ shape : g s' ≡ ( [ a ] , [ s ] ) ⦄ → Expr s' b → Expr s (a ⇒ b) _·_ : ∀ {a b} → Expr s (a ⇒ b) → Expr s a → Expr s b data Val : Ty → (Σ : HeapTy) → Set where unit : ∀ {Σ} → Val unit Σ ⟨_,_⟩ : ∀ {Σ s s' a b}⦃ shape : g s' ≡ ( [ a ] , [ s ] ) ⦄ → Expr s' b → Frame s Σ → Val (a ⇒ b) Σ num : ∀ {Σ} → ℤ → Val int Σ
var式は解決パスを受け取って変数を参照します(参照node)。
ƛ式は⦃ shape : g s' ≡ ( [ a ] , [ s ] ) ⦄で、ƛ式のスコープsの子スコープs'が存在することを保証して、その宣言ノードの型をaとしています。
モナド
型環境の代わりに、モナドは "現在のフレーム" に対応するスコープsによってインデックスされます。構造は前回と同じです。
M : (s : Scope) → (HeapTy → Set) → HeapTy → Set
M s p Σ = Frame s Σ → Heap Σ →
Maybe (∃ λ Σ' → (Heap Σ' × p Σ' × Σ ⊑ Σ'))
bindと_^_は前回と同じように定義されます。
getFrameやusingFrameは前回までのgetEnvやusingEnvと対応します。
_>>=_ : ∀ {s Σ}{p q : List Scope → Set} → M s p Σ → (∀ {Σ'} → p Σ' → M s q Σ') → M s q Σ _^_ : ∀ {Σ Γ}{p q : List Scope → Set} → ⦃ w : Weakenable q ⦄ → M Γ p Σ → q Σ → M Γ (p ⊗ q) Σ -- 現在のフレーム getFrame : ∀ {s Σ} → M s (Frame s) Σ getFrame f = return f f -- aにフレームfを渡す usingFrame : ∀ {s s' Σ}{p : List Scope → Set} → Frame s Σ → M s p Σ → M s' p Σ usingFrame f a _ = a f -- スコープsのフレームを、slotsとlinksで初期化する。 init : ∀ {Σ s' ds es}(s : Scope)⦃ shape : g s ≡ (ds , es) ⦄ → Slots ds Σ → Links es Σ → M s' (Frame s) Σ init {Σ} s slots links _ h with (initFrame s slots links h) ... | (f' , h') = just (_ , h' , f' , ∷ʳ-⊒ s Σ) -- 解決パスに対応するt型の値を返す getv : ∀ {s t Σ} → (s ↦ t) → M s (Val t) Σ getv p f h = return (getVal p f h) f h -- 式を受け取って、そのスコープを返す sₑ : ∀ {s t} → Expr s t → Scope sₑ {s} _ = s
eval
新しい評価規則は以下の通りです。前回と同じものは省略。今まで登場した関数を使って簡潔に書かれていてよいですね。
eval : ℕ → ∀ {s t Σ} → Expr s t → M s (Val t) Σ eval (suc k) (var x) = getv x eval (suc k) (ƛ e) = getFrame >>= λ f → return ⟨ e , f ⟩ eval (suc k) (l · r) = eval k l >>= λ{ ⟨ e , f ⟩ → (eval k r ^ f) >>= λ{ (v , f) → init (sₑ e) (v ∷ []) (f ∷ []) >>= λ f' → usingFrame f' (eval k e) }}
スコープとフレームを使うことで、定義的インタプリタはメモリの安全原則を自動的に継承し、オブジェクト言語は独自の型付きメモリや補助エンティティ（オブジェクトやスタックなど）の概念を定義する必要がありません。このセマンティクスをSTLC+Refに拡張することは、例えば、参照セルを表現するために切断された単一宣言スコープを使用することによって、簡単です。
Examples
スコープグラフは、型環境 Ctx = List Tyほど単純な構造ではないため、Agdaは式からグラフ構造を推論できない。そのため、グラフは手動で定義している(このままでは使いにくいことこの上ないが、グラフ自動構成は今後の課題となっている。)
-- スコープグラフ g : Graph g zero = [] , [] -- root scope g (suc (suc n)) = [ int ] , [ suc zero ] -- lexical scope for inner lambda g (suc n) = [ int ] , [ zero ] -- lexical scope for outer open Syntax g open UsesGraph g -- (+) curry+ : Expr zero (int ⇒ (int ⇒ int)) curry+ = ƛ {s' = suc zero} (ƛ {s' = suc (suc zero)} (iop _+_ (var (path [] (here refl))) (var (path ((here refl) ∷ []) (here refl))))) open UsesVal Val val-weaken -- Initial heap with an empty frame that is typed by the root scope: init-h : Heap [ zero ] init-h = ([] , []) ∷ [] -- 1 + 1 = 2 test-curry+ : eval 3 ((curry+ · (num (+ 1))) · (num (+ 1))) (here refl) init-h ≡ just (_ , _ , num (+ 2) , _) test-curry+ = refl
わかりやすい依存型入門その１
型について
HaskellやJavaような言語にある型システムは、以下のような役割があります。
- 実行前にエラーを検出する。
- コンパイラの最適化を可能にする。
- コードをわかりやすくする。
依存型は、プログラムが論理的に正しいかの検証をすることができます。(今度説明します)
依存型とは
依存型(dependent type)とは、値によってパラメタライズされた型です。
どういうことなのか、例を見ていきましょう。
依存型は、数学世界との親和性が高いです。
例えば、線形代数では、実数上のn次元ベクトルの集合をと書きますね。
これをプログラム世界で考えると、n次元ベクトルを表す型を
Vec n と書くことになりますが、このVecという型は、自然数(int型)の値であるnを受け取っています。
実際、Vec nはnの値次第で、Vec 0やVec 1になるわけです。これが依存型です。
標準のHaskellではMaybe Intのように型が型引数を受け取ることはあっても、値を受け取れることはありませんでした(Maybe 0なんて型はありませんね)。
(Just 0)は型ではなく値であることに注意してください。この先、型と値の違いを意識してください。
ベクトルを定義したので内積も定義しましょう。
数学世界では、ベクトルの内積は
の写像です。
これを型で考えると、
Vec n -> Vec n -> Numberのようになります。(Numberは適当な数値型と考えてください)
ここに依存型の強みの1つがあります。
もし標準のHaskellで内積をつくったなら、Vec -> Vec -> Doubleのようになるでしょう(依存型がないとベクトル型はVecと書くしかありません)。
その内積にVec型の値として(1,2)と(1,2,3)を渡すとどうなるでしょう。型検査は通過しますが、内積は次元の違うベクトルに対して定義されないので、実行時エラーになってしまいます。
しかし依存型で定義した型は、同じ次元のベクトルの組しか受け取りません(Vecの次元がnで固定されているので)、もしそんな引数を渡そうものなら型エラーを叩き返してくれるでしょう。
このような依存型を扱う言語には、Agda、Idris、Coqなどがあります。
上の例じゃなくても、長さnのList型List nとか
n×m行列型Mat n mとかでも同じ説明ができますね。
次回に続くかも
依存型を使った、型安全な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にあったので、何らかの進展があったかもしれないね。
以上、ここまで読んでくれた人、本当にありがとうございました。輪講は終わりましたが、続きが気になるのでまたまとめてアップするかもしれません。
