TaPL輪講/11章
かんたんな拡張
単純型付きラムダ計算は理論的性質が興味深いものになるのにじゅうぶんな構造を持っているけど、プログラミング言語にはまだ足りない
この章では、より身近な言語とのギャップを埋める
いろいろな型付けのレベルで単純明快な機能を導入することで
この章を通じて重要なテーマは「派生形式」の概念
11.1 基底型
理論的な目的から、個別の基底型やそれらに関する操作を抽象化しておくとやりやすいことが多い
11.2 unit型
もう1つの(とくにML族の言語で見られる)便利な基底型としてシングルトン型のUnitがある
図11-2
前節の基底型とは対照的に、この型は最も簡単な方法で扱われている
明示的に1つの要素(定数項unit)を導入する
型付け規則を導入する
unitはUnit型の式の唯一の評価結果
純粋な関数型言語においてもunit型はなお関心の対象になっている
しかし主要な応用は副作用のある言語
代入とか参照セルとか
13章で見る
そういった言語では、式の返す結果ではなく副作用に注意を払う
Unitはそういった式の結果の型として適切
11.2.1 演習
tnの大きさは高々O(n)だが、正規形に到着するのに少なくともO(2^n)のステップが必要となるような、Unit型のみを基底型として持つ単純型付きラムダ計算の項の列t1, t2, ...を構成できるか?
t1 = (λx:Unit. x) Unit
tn = (λf:Unit->Unit. f(f(unit))) (λx:Unit. tn-1)
11.3 派生形式: sequencingとワイルドカード
副作用のある言語では、しばしば2つ以上の式を順に評価できると便利
t1; t2
t1の評価をして(副作用を起こして)評価結果は無視してt2を評価する
sequencingを形式化する代わりの方法として t1; t2 を (λx:Unit. t2) t1 の略記であるとみなすというのがある
xはfresh
11.3.1 定理
sequencingは派生形式である
λE を単純型付きラムダ計算+Unit型+sequencingの規則
λI を単純型付きラムダ計算+Unit型 とする
e : λE -> λI をt1; t2 を (λx:Unit. t2) t1 (xはfresh) に置換する関数であるとする
λEの項tについて以下が成り立つ
$ t \rightarrow_E t' \iff e(t) \rightarrow_I e(t')
$ \Gamma \vdash^E t : T \iff \Gamma \vdash^I e(t) : T
定理11.3.1によって派生形式という語の使用が正当化された
sequencingの型つけや評価の振る舞いがabstractionとapplicationというより基本的な操作から派生できるので
新しい文法や評価規則を導入するごとに型安全性とかを証明しなおさなくてよいので便利
派生形式はしばしば糖衣構文とよばれる
派生形式を低レベル定義に置き換えることを脱糖という
もう1つののちの例で有用な派生形式として変数束縛の「ワイルドカード」規約がある
dummyのラムダ抽象を作りたいときがある
λ_:S.t を λx:S.tの略記とする (xはtに現れない変数)
11.3.2 演習
ワイルドカード抽象の型付けと評価規則を与えて、それが派生形式になることを示せ
型付け規則
(T-WildAbs)
Γ |- t : T => Γ |- λ_:S.t : S -> T
(E-AppWildAbs)
(λ_:S.t) v -> t
派生形式を取り除くような変換を定めて11.3.1と同じことを示すとよさそう
λx:Unit.tをλx:S.t (x is fresh) に変えるだけで同じ議論ができるのではないか
11.4 ascription
型のassertionみたいな感じ?
11.4.1 演習
(1) ascriptionを派生形式として形式化せよ
t as T = (λx:T.x) t
定理11.3.1が同様に示せる
(2) eager ruleを入れてもascriptionは派生形式とみなせるか?
t as T = (λx:Unit -> T.x unit) (λy:Unit. t) (yはfresh)
定理11.3.1はそのままの形では成り立たなくなる
なぜならdesugarされた側では簡約ステップが多くなる
$ t \rightarrow_E t' \iff e(t) \rightarrow_I^* e(t') なら示せる
11.5 let束縛
let束縛を派生形式にするのは面倒
評価に関してはすぐできるけど型付けがたいへん
22章でletを派生形式にしない理由が出る(HM多相性)
11.5.2 演習
let x = t1 in t2 を [x |-> t1]t2 の略記としてよいか?
→だめ
評価順が変わる
ill-typedな項に型がついてしまう
let x = unit unit in unit
11.6 ペア
11.7 タプル
ペアの一般化
11.8 レコード
n-タプルからラベル付きレコードへ
11.8.1 演習
規則 (E-ProjRcd) をより明示的に書き下せ
11.8.2 演習
パターンマッチング
11.9 和
ヴァリアント型に対応する
11.9.1 演習
if式やtrue,falseをUnitと直和の派生形式として形式化せよ
和型があると型の一意性が必ずしも成り立たなくなる
型のassertionを入れることで一意性が成り立つようにした (図11-10)
11.10 ヴァリアント
和を一般化
Option型
列挙型
1要素ヴァリアント
あまり便利そうには見えないが……
生のfloatを扱うことに起因するバグを防ぐ
ヴァリアントと(MLの)datatype
似てるけど違う
直和としてのヴァリアント
type dynamic
(動的型 とは異なる?)
静的型の言語であっても、しばしばコンパイル時に型を決定できないデータを扱う必要が出てくる
11.11 一般的な再帰
型なしラムダ計算では再帰を行うコンビネータが定義できる
型つきでは同じようにはできない
不動点コンビネータを導入 (図11-12)
letrec派生形式
11.11.1 演習
equal, plus, times, factorialをfixを用いて定義せよ
11.11.2 演習
演習11.11.1で定義した関数をfixの代わりにletrecを用いて書き直せ
11.12 リスト
11.12.1 演習
前進性と型保存が真偽値とリストの入った単純型付きラムダ計算について成り立つことを確かめよ
→真偽値についてはもう示したので、リスト関連の規則について示せば十分そう
11.12.2 演習
ここでのリストの表現には、本来は必要でない多くの型アノテーションが含まれている
*全ての* 型アノテーションを取り除くことができるか?
→nilの型が一意に定まならくなるのではないか