Region based mini ml - translation

変換前言語・変換後定義、Regionの概要については前回の記事を読んでください。
この記事ではtranslationに必要な表現・変数の定義を先に説明し、参考論文の規則に則って詳細を説明していきます。
個人的な解釈が含まれているため、記事の内容が全て正しいとは限りません。何か問題点・不明点等があれば連絡してください。

Translation

結論から説明すると、SExpからTExpへのTranslationはRegion注釈付きの型推論と言い換えることができます。 ではまずそれぞれ変数・表現を元論文より抜粋して定義します。シンプルなものであるため、定義を列挙します。 例示・詳細については参考論文を参照してください(P21 5.1 Semantic object)。

Variable

  • {
\alpha \in TyVar
}

  • {
p \ or \ \rho \in RegVar
}

  • {
\epsilon \in EffectVar
}

それぞれ型変数・Region変数・Effect変数を示します。

Effect

  • {
\psi \in Effect  = Fin(AtomicEffect)
}

  • {
AtomicEffect = EffectVar \cup PutEffect \cup GetEffect
}

  • {
put(\rho) \in PutEffect = RegVar
}

  • {
get(\rho) \in GetEffect = RegVar
}

Effectは各Token(厳密には定義していないがExpressionの各項)について、その項を評価した際の副作用を示します。 また、EffectはRegionに対する操作・参照によるRegionへの副作用を示すものです。 PutEffectは 変数 {\rho}のRegionに対するWriteの操作を、GetEffectは変数 {\rho}のRegionに対するReadの操作を示します。これらの作用に関しては実行時に評価されるため、意味についての説明はこの程度にしておきます。

Type, TypeScheme

  • {
\tau \in Type = TyVar \cup ConsType \cup FunType
}

  • {
SimpleTypeScheme = Type
}

  • {
CompoundTypeScheme = \cup_{k \geq 0} RegVar^{k} \times \cup_{n \geq 0} TyVar^{n} \times \cup_{m \geq 0} EffectVar^{m}
}

  • {
\sigma \in TypeScheme = SimpleTypeScheme \cup CompoundTypeScheme
}

  • {
ConsType = { int }
}

  • {
\mu     \rightarrow^{\epsilon . \psi} \mu \in FunType = TypeWithPlace \times ArrowEffect \times TypeWithPlace
}

  • {
\epsilon . \psi \in ArrowEffect = EffectVar \times Effect
}

  • {
\mu \in TypeWithPlace = Type \times RegVar
}

前回の記事で後ほど紹介すると言っていたTExpに対するType schemeを含みます。これらを書き下すと

{
\sigma ::= \forall().\tau
}

{
\sigma ::= \forall \rho_1 \cdots \rho_k \alpha_1 \cdots \alpha_n \epsilon_1 \cdots \epsilon_m . \tau
}

となり、これらは任意のEffectVar, TypeVar, RegVarを含む多相を表現できると言えます。

他、特に説明しなければいけないのはFunTypeについてです。SExpでは純粋なArrowTypeであったに対し、 上記ではTypeWithPlaceからTypeWithPlaceへArrowEffectを伴う型と定義されており、 これはRegion {\rho_1}に紐づく型 {\tau_1}を持つ項を評価した際、 ArrowEffect  {\epsilon . \psi}を副作用とし、 Region {\rho_2}に紐づく型 {\tau_2}を持つ項を結果とすると言えます。

また、ArrowEffect  {\epsilon . \psi} にある  {\epsilon} はEffectVarであり、他のEffectから参照されるための識別子として使われ、  {\psi} はEffectの有限集合を示します。

Environment

  • {
TE \in TyEnv = Var \rightarrow^{fin} (TypeScheme \times RegVar)
}

評価を行う際の型環境TEの定義です。 プログラム中の変数を元として、型を示すTypeと紐付いているRegionを示すRegVarを対応させます。

Inference rule

推論は以下の形式で与えられます。

{
TE \vdash e \Rightarrow e' : \mu, \psi
}

これは 型環境TE上で、 {e}を評価した際、TypeWithPlace  {\mu}, Effect  {\psi} を持つ  {e'} へと変換される と読みます。 これに則り、P26 5.2 The inference system の各ruleを適用することでSExpからTExpへの変換を含めた型推論を行うことができます。 各ruleについての説明は、Variable, Effect, Type, TypeScheme, TEの定義、また多相型の推論をベースにした簡単なものであるため省略します。


ここまででRegion推論についての概要を説明しました。 まとめるとRegion推論(SExpからTExpへのtranslation)はRegion注釈付きの型推論であり、 多相型を拡張した型スキームに則り、型推論を行うことでRegionを推論することが可能であるという点です。 初期に考えていた記事のボリュームよりかなりやっつけになってしまいましたが、 とりあえずRegion推論に関する概要の説明はここまでとして、次回は推論の詳細の話と実装について書きます。