『ゼロから学ぶRust』を読む 第9章 線形型システム
線形型システム
線形型システム
値をちょうど1回しか利用できないような型システム
アフィン型システム
値を最大1回利用可能な型システム。
9.1 線形型システムの理論
線形型システムの理論について説明する。
9.1.1 数学的表記
本章では、以下の表9.1の表記を用いる。
https://gyazo.com/ab762837c617a1f10260dbd77ec0287a
https://gyazo.com/3489ccc30885657e8d4defaa73e92d83
EXPR = expression: 数式
記述と意味
<A> : 変数
<A>:= <B>: <A>は<B>である。
<A>:=<B>|<C> : <A>は<B>または<C>である。
9.1.3 LinZ言語
LinZ(リンゼット、もしくはリンズィー)
$ \Gamma はLinZの式ではなく、LinZの型付け規則を定義する際に用いられる記述で、これは型環境(type enviroment)と呼ばれる。 LinZの型付け規則は$ \Gamma := hogeで定義される。
https://gyazo.com/d6ae79707aa7698c2d5effb3215a4a4b
変数にはlin(線形、一度しか使用できない、一度は使用しなくてはならない)、またはun(使用回数に制限がない)のどちらかの修飾子がつく。
LinZは$ \lambda計算の拡張である。ラムダ計算 code:bnf
<Γ> ::= ø // 型環境(空集合)
| <Γ>, x : <T> // 型環境の拡張
Tips
Rustはアフィン型 + ライフタイムでメモリを管理している。
一度でも使えばfree
ライフタイムを越えればfree
9.1.4 型付け
$ \frac{A}{B}と書かれた場合、これは、「A が正しければ B も正しいと証明(推論)できる」
また、$ \frac{A_1 A_2}{B}と書かれた場合、これは、「A1 と A2 の両方が正しければ B も正しいと証明できる」という意味になり、条件の部分には2個以上の式を書くことができる。
code: LinZの型環境分割例
x: lin bool
lin <x, y>
3. Un述語とLin述語
https://gyazo.com/9d6e8858bfc4a3612a8990ac6108a9e8
3つ目逆の方が気持ちいいな。un がlinに包含されている?tkawauchiya.icon
Linの方が制約条件が強いからLin(un P)はできる(ture)けど、Un(Lin P)はできない(false)ってことではないか?SSS.Leopom.icon
型環境への適応が全然わからないSSS.Leopom.icon
$ Un(x:un <un bool, un bool>, y:lin bool)
$ = Un(un <un bool, un bool>) \land Un(un bool)
↑これ誤植じゃないのかな??y の修飾子が等式変形中に変わっちゃってるtkawauchiya.icon
誤植でしたSSS.Leopom.icon
正
Un(un bool) = true
Un(lin (lin bool * lin bool)) = false
Lin(un bool) = true
Lin(un (un bool * un bool)) = true
Lin(lin (un bool * lin bool)) = true
このように、Un 述語に lin 型を渡している2つ目の式のみ false となる。 Un 述語と Lin 述語は、型環境にも適用できる。型環境に適用する場合は、型環境中のすべての型が true の場合にのみ true となる。 たとえば、以下のようになる。ただし、∧は「かつ」という意味であり、つまり論理積の記号である。
高野祐輝. ゼロから学ぶRust システムプログラミングの基礎から線形型システムまで (KS情報科学専門書) (p.396). 講談社. Kindle 版.
この下の式も誤植
正
- Un(x:un (un bool * un bool), y:un bool)
= Un(un (un bool * un bool)) ∧ Un(un bool)
= true
- Un(x:un bool, y:lin bool)
= Un(un bool) ∧ Un(lin bool)
= false
式中に複数変数の引数を持つような形では(x, y)両方の成立している必要があるので、∧と置き換えて良い。SSS.Leopom.icon
4. 型付け規則
$ q: un|lin
修飾子qualifierの”q”なんやねtkawauchiya.icon
$ Q: Un|Lin
https://gyazo.com/f804e03187bf3bc0b27ed73c014291dc
T -Var
$ \Gamma_1と$ \Gamma_2両方にlin型変数がなければ、$ \Gamma_1と$ \Gamma_2に任意の型を追加した型環境において、その型を使える。
型を証明ってなんだろうtkawauchiya.icon
たぶん実用的には、型を特定できてコンパイル可能であるというようなことと紐づいているっぽいな。tkawauchiya.icon
逆に言えば、lin型変数があると適当に変数宣言すると参照が被ったり、使用回数の制限に引っかかってコンパイル通らんと言っているだけ?tkawauchiya.icon
T -Bool
lin bool がある型環境では適当に変数を使うと再利用性に引っかかる的なことかな。tkawauchiya.icon
T-If
$ \Gamma_1 \vdash e_1: q \;bool
$ \Gamma_2, x:T_1, y:T_2 \vdash e_2:T
[]
T-Pair
T-Split
$ \Gamma_1にペア型変数があって、$ \Gamma_2と$ T_1型のx、$ T_2型のyを組み合わせてT型を返すの式$ e_2を考えるとして、$ \Gamma_1と$ \Gamma_2の合成型空間でペア型変数を展開して、式$ e_2を構成できるよ、という意味。
T-Abs
$ Q(\Gamma)がtrue($ \Gammaにlin型変数がない、またはあるとしたら、q=lin)かつ、$ \Gammaと$ T_1型のxを使って$ T_2型の変数を返す式$ eを構成できるとしたとき、その式$ eを使って$ T_1型の変数を引数とし$ T_2型の変数を返すq 関数を構成できる、という意味。
T-App
$ \Gamma_1上で$ T_{11}を引数に$ T_{12}を返す処理$ e_1が構成できて、$ \Gamma_2上で$ T_{11}型を返す式$ e_2が構成できたら、$ e_1に$ e_2を適用して$ T_{12}型の値を得る式を得ることができる。
$ (e_1~e_2) ってなんだ。tkawauchiya.icon
関数適用だったわ。
T-Free
$ \Gamma_1上に$ lin P型変数があって、$ \Gamma_2上に適当な処理があれば、$ \Gamma_1と$ \Gamma_2の合成型空間で、xを解放して、処理を実行できる。
9.2.1 パーサコンビネータのきほん
Rustのパーサコンビネータ実装の一つであるnomをもちいてパーサコンビネータの説明を行う
https://gyazo.com/b2243c5ff2f6363b70409b4862ddbab3
9.3 LinZ言語の実装
B木ってなんだ〜?tkawauchiya.icon 9.4 課題 演習問題