Tapl勉強会 201908

23.5.md

23.5 基本的な性質

• 保存: Γ|-t:Tかつt->t'ならば Γ|-t':T

• 進行: tが閉じた、正しく型付けされた項ならば、tは値であるか、さもなくばあるt'が存在してt->t'となる

• 正規化: すべての正しく型付けされたプログラムの評価は停止する

23.6 型消去、型付け可能性、型再構築

• SystemFは型消去が適用できる

  • 型注釈をすべて取り払って型無しラムダ項にする

• 型付け可能

  • SystemFの正しく型付けされた項tが存在して、erase(t) = mであるとき、型無しラムダ計算の項mはSystemFで型付け可能であるという

• 形無し項mが与えられたとき、SystemFの正しく型付けされた項tでerase(t) = mとなるものがあるかは決定不能

• sが与えられたとき、SystemFの正しく型付けされた項tで、t ・> sとなるものがあるかは決定不能

23.7 型消去と評価順序

• SystemFの操作的意味論は型渡し意味論

  • 多相関数が型引数に出会ったとき、関数の本体に型が実際に代入される

• 値呼び評価戦略では型抽象が評価を止めるので、副作用のあるプリミティブの評価を遅延・抑制する

let f = (λX.error) in 0 # λX.error本体のerrorが評価されないので0が返る
let f = error in 0 # 例外

• 食い違いは型抽象を項抽象に変えると解決

erase(λX.t2) = λ_. erase_v(t2)
erase(t1 [T2]) = erase_v(t1) dummyv

23.8 制限された System F

• 型再構築を扱えるようにする提案
  • let多相(冠頭多相)
    • 型変数は量化子のない型(単型)の上だけを動き、量化された型が矢印の左側に現れることを許さない
  • ランク2多相: 型を木としてみたとき、その根から∀量子化へのパスで、二回以上矢印の左側を通るものがない
    • ランク2: (∀X.X->X)->Nat
    • ランク2ではない: ((∀X.X->X)->Nat)->Nat

23.9 パラメータ性

• パラメータ性
  • 多相的なプログラムの振る舞いの一様性を定式化したもの
  • 例：truとflsがCBoolのただ２つの要素という観察

23.10 非可述的

• 非可述的とは
  • SystemFの多相性が一例
  • 定義されているそのもの自身が定義域に含まれるような量化子を含む
  • 例： T = ∀X.X->X の型変数Xは任意の型の上を動き、T自身も含まれている
• 可述的とは
  • しばしばMLに見られる多相性
  • 型変数の値域が単型に制限されていて、量化子を含まない