Arantium Maestum

プログラミング、囲碁、読書の話題

Algorithm W実装のためにPrincipal Type Schemes for Functional Programsを読む(前編)

型推論のためのAlgorithm Wを実装するため、DamasとMilnerのPrincipal Type Schemes for Functional Programsを読んでいる。

重要そうな概念としては

  • expression
  • type/type-scheme
  • substitution
  • instance/generic instance
  • assumption
  • assertion
  • closure
  • type inference
  • Robinson's unification algorithm
  • algorithm W

あたり。それらの定義や周辺のポイントを整理するためにメモっていく。長かったので今回はexpressionからclosureまで。

Expression

型付けをする言語の式:

e::= x | e e′ | λx.e | let x = e in e′

ラムダ計算にletが加えられている。Hindley-Milner-Damasだとletを使ってのみ多相を扱えるので、STLCのように「letは関数適用の糖衣構文」というスタンスを取れない。

Vが値だとして

Env = Id → V be the domain of environments η
semantic function ε : Exp → Env → V

という関数も重要。Envは変数環境、εは式の評価関数。

以下のように使う:

η[x] : 変数xに対応する値を環境ηからとる
ε[e]η : 変数環境ηで式eを評価した結果の値を得る

Type and Type Scheme

Type τとType Scheme σが分けられている。

定義は:

τ ::= α | ι | τ → τ 
σ ::= τ | ∀α σ

typeは型変数α、何らかのbase type ι(intとかunitとか)、そして二つのtypeをとるbinary type constructor →で作る関数型で再帰的に定義。

type schemeはただのtypeか、何らかのtype schemeの前に何らかの型変数の全称量化∀αがついたもの。

この定義だとtypeには全称量化子がでて来ないので、typeに含まれる型変数は必ずfree variableで、さらに関数型の中のどちら側にも全称量化子はでてくることができない。例えば多相的な型を引数にとるような関数の型は定義できない。

全称量化はtype schemeの先頭にズラーっと並んで、そのあとに必ずtypeがくる、という形になる。

いくつか関連用語:

A type-scheme ∀α_1 . . . ∀α_n τ (which we may write ∀α_1 . . . α_n τ) has generic type variables α_1 . . . α_n .

A monotype μ is a type containing no type variables.

Substitution

S is a substitution of types for type variables, often written [τ_1/α_1,...,τ_n/α_n] or [τ_i/α_i]

Substitutionとは型変数をtypeにマップするもの。注意点としては、任意の型ではなく型変数から、type schemeではなくtypeへのマッピングだということ。

Instantiation

If S is a substitution ... and σ is a type-scheme, then Sσ is the type-scheme obtained by replacing each free occurrence of α_i in σ by τ_i , renaming the generic variables of σ if necessary. Then Sσ is called an instance of σ; the notions of substitution and instance extend naturally to larger syntactic constructs containing type-schemes.

Substitution同士を組み合わせることもできる。後述のunificationの部分で:

If S unifies τ and τ′ then U(τ,τ′) returns some (substitution) V and there is another substitution R such that S = RV

と出てくる。この組み合わせ方がよくわからない。RVというのはVに出てくる型変数をRマッピングで変換したものなのか、それともRVに含まれるマッピングをすべて合わせた新しいマッピングなのか(その場合、同じ型変数が出てくる場合どうするのか)

さらに後ほどalgorithm Wの説明でS = V S_2 S_1のようにSubstitutionを3つ組み合わせるものも出てくるのだが、これは右結合でいいのだろうか?

Generic instantiation

By contrast a type-scheme σ = ∀α_1 ...α_m τ has a generic instance σ′ = ∀β_1 ...β_n τ′ if τ′ = [τ_i/α_i]τ for some types τ_1,...,τ_m and the β_j are not free in σ. In this case we shall write σ > σ′.

generic instanceというのは「よりgenericになったinstance」ではなく「generic variableをinstantiateしたもの」で、結果としては元のtype schemeよりnon-genericになっている。元のtype schemeの全称量化を一つ以上外して型変数をtypeで入れ替えたもの。全称量化をすべて外す必要はない。

(ちなみに型変数もtypeなのでα_1∀α_1 α_1のgeneric instanceなんだな・・・)

Assumption

A is a set of assumptions of the form x :σ

Assumptionというのは式における変数(型変数ではなく)とtype schemeマッピング

... we shall assume that A contains at most one assumption about each identifier x.

A_x stands for removing any assumption about x from A.

というのも注意点。

AssumptionsはSubstitutionを適用できる。基本的には単体のassumptionではなく、set of assumptionsにsubstitutionを適用して自由型変数をtypeに入れ替えるようだ。

Assertion

Assertionというのは「あるset of assumptions(式変数からtype schemeへのマッピング)Aを前提とすると、式eの型はtype scheme σ」という意味を持つ文で、以下のように表される:

A |= e:σ

(ちなみに「式eの型はtype scheme σ」でいいのだろうか?それとも「式eの型はtype scheme σの何らかのgeneric instance」とした方が正しい?)

「Assertionが成立する」という意味:

(An) assertion is closed ... if A and σ contain no free type variables

(T)he sentence is said to hold iff, for every environment η, whenever η[x] :σ′ for each member x :σ′ of A, it follows that ε[e]η:σ

Closed assertionが成り立つには、Assumptionsと合致するいかなる変数環境においても式を評価した結果の値が正しいtype schemeである必要がある。

(A)n assertion holds iff all its closed instances hold

all its closed instancesと書いていることからも、assertionにもsubstitutionが適用できることがわかる。Assertionを構成するAssumptionsとType Schemeをcloseさせるような(自由変数をすべて束縛するような)いかなるsubstitutionを適用しても、その結果得られるclosed assertionが成り立つ必要がある。すでにclosedなassertionは自身を唯一のclosed instanceとして持つ、という認識でいいのだろうか。

Closure

We also need to define the closure of a type τ with respect to assumptions A;

A(τ)=∀α_1,...,α_n τ

where α_1,...,α_n are the type variables occurring free in τ but not in A.

Type τに出てきてAssumptionsに出てこない自由型変数を全称量化する。type schemeではなくtypeなのは何か理由があるのだろうか。

実例で考えるとAがx:α_1; y:∀α_2 (α_2 -> α_1)でτがα_1 -> α_2 -> α_3だった場合、A(τ)は∀α_2 ∀α_3 (α_1 -> α_2 -> α_3)になる。

次回

今回の用語の整理を踏まえて、次は以下の三点を見ていく:

  • type inference
  • Robinson's unification algorithm
  • algorithm W

これらの詳細を読んでいくことでsubstitutionについての不明点なども解決されることを期待・・・