線形型システム
ATTaPL 1.2より
(Linear-): weakeningとcontractionができない型システム
すべての変数をちょうど1回使う
構文
STLCの拡張
qualifier q: intro-termにくっつくアノテーション
lin: ちょうど1回使われる
un: 普通のSTLCと同じように何回でも使ってOK(ガベコレなどでの回収が想定される)
term t: 大体普通のSTLCだが、全てのintro-termにqualifierがつく
pairのprojectionだけは「片方だけ取り出す」ことを防ぐため、split t as x,y in tという形
pretype P: STLCでの型
type T: この体系で扱う型
q P: qualified pretype
型付け
次のようなことを達成したい
線形な変数はどのパスにおいてもちょうど一回使われる
xがlinearだとして、(λz.λy.<free z, free y>) x x みたいなことをされると困る
Unrestrictedなデータの中にはlinearなデータが入っていない
xがlinearだとして、un <x,3>を複製してアンパックされると↑が起こる
線形性の担保 → 型環境の分割を導入
unの場合は双方にコピーできる
linの場合はどちらか片方だけ
構造の健全性の担保 → containmentq(T), q(Γ)を導入
q(T) iff. $ \mathtt{T} = \mathtt{q}' and $ \mathtt{q} \sqsubseteq \mathtt{q}'
q(Γ) iff. $ x:T \in \Gamma implies $ \mathtt{q}(T)
lin ⊑ unです
型付けのbase caseが線形性などの担保に重要
code:T-Var
un(Γ_1,Γ_2)
------------------ T-Var
Γ_1,x:T,Γ_2 ⊢ x:T
un(Γ_1,Γ_2)で全ての変数が必ず使われることを担保している
Bool値の導入にも同じようなことをしないといけない