#co(){ Chapter 16 Hindley/Milner Type Inference This chapter demonstrates Scala's data types and patternmatching by developing a type inference system in the Hindley/Milner style [Mil78]. The source language for the type inferencer is lambda calculus with a let construct called Mini-ML. Abstract syntax trees for the Mini-ML are represented by the following data type of Terms. } #setmenu2(ex-r-menu) * 第 16 章 Hindley/Milner 型推論 (Hindley/Milner Type Inference) この章では、Hindely/Milner スタイル[Mil78] の型推論システムの開発を通して、Scala のデータ型とパターンマッチングを見てみます。型推論器の対象言語は、mini-ML と呼ばれる let 構成子を持つ λ計算です。mini-ML の抽象構文木は、次のデータ型 Term によって表現されます。 abstract class Term {} case class Var(x: String) extends Term { override def toString = x } case class Lam(x: String, e: Term) extends Term { override def toString = "(\\" + x + "." + e + ")" } case class App(f: Term, e: Term) extends Term { override def toString = "(" + f + " " + e + ")" } case class Let(x: String, e: Term, f: Term) extends Term { override def toString = "let " + x + " = " + e + " in " + f } #co(){ There are four tree constructors: Var for variables, Lam for function abstractions, App for function applications, and Let for let expressions. Each case class overrides the toString method of class Any, so that terms can be printed in legible form. We next define the types that are computed by the inference system. } 木のコンストラクタが４つあります。変数を表す Var、関数抽象を表す Lam、関数適用を表す App、そして let 式を表す Let などです。それぞれのケースクラスでは、Any クラスのメソッド toString をオーバーライドして、項をわかりやすく表示しています。 次に、推論システムによって計算される型を定義します。 sealed abstract class Type {} case class Tyvar(a: String) extends Type { override def toString = a } case class Arrow(t1: Type, t2: Type) extends Type { override def toString = "(" + t1 + ">" + t2 + ")" } case class Tycon(k: String, ts: List[Type]) extends Type { override def toString = k + (if (ts.isEmpty) "" else ts.mkString("[", ",", "]")) } #co(){ There are three type constructors: Tyvar for type variables, Arrow for function types and Tycon for type constructors such as Boolean or List. Type constructors have as component a list of their type parameters. This list is empty for type constants such as Boolean. Again, the type constructors implement the toString method in order to display types legibly. } 型コンストラクタが３つあります。型変数を表す Tyvar、関数の型を表す Arrow、そして Boolean や List などのような型コンストラクタを表す Tycon などです。型コンストラクタは構成要素として型パラメータのリストを持ちます。このリストは Boolean のような型定数については空になります。型コンストラクタもまた、型をわかりやすく表示するために toString メソッドを実装しています。 #co(){ Note that Type is a sealed class. This means that no subclasses or data constructors that extend Type can be formed outside the sequence of definitions in which Type is defined. This makes Type a closed algebraic data type with exactly three alternatives. By contrast, type Term is an open algebraic type for which further alternatives can be defined. } Type が sealed(封印された)クラスである事に注意してください。これは、Type を拡張するサブクラスやデータコンストラクタを、Type が定義されている定義列の外部では作れない事を意味します。これにより、Type は&bold(){クローズ}な代数データ型で、代替物が確実に3つである事が保証されます。逆に、型 Term は&bold(){オープン}な代数型であり、さらなる代替物を定義できます。 #co(){ The main parts of the type inferencer are contained in object typeInfer. We start with a utility function which creates fresh type variables: } 型推論器の主な部品は object typeInfer に含まれます。新しい型変数を生成するユーティリティ関数から始めましょう。 object typeInfer { private var n: Int = 0 def newTyvar(): Type = { n += 1; Tyvar("a" + n) } #co(){ We next define a class for substitutions. A substitution is an idempotent function from type variables to types. It maps a finite number of type variables to some types, and leaves all other type variables unchanged. The meaning of a substitution is extended point-wise to a mapping from types to types. } 次に、代入を表すクラスを定義します。代入は、型変数から型への冪等な (何度同じ操作をしても同じ結果となる) 関数です。有限な数の型変数を何らかの型にマップし、ほかのすべての型変数はそのまま変えません。代入の意味は、各点でのマッピングから、複数の型から複数の型へのマッピングへと拡張されます。 abstract class Subst extends Function1[Type,Type] { def lookup(x: Tyvar): Type def apply(t: Type): Type = t match { case tv @ Tyvar(a) => val u = lookup(tv); if (t == u) t else apply(u) case Arrow(t1, t2) => Arrow(apply(t1), apply(t2)) case Tycon(k, ts) => Tycon(k, ts map apply) } def extend(x: Tyvar, t: Type) = new Subst { def lookup(y: Tyvar): Type = if (x == y) t else Subst.this.lookup(y) } } val emptySubst = new Subst { def lookup(t: Tyvar): Type = t } #co(){ We represent substitutions as functions, of type Type => Type. This is achieved by making class Subst inherit from the unary function type Function1[Type, Type](*1). To be an instance of this type, a substitution s has to implement an apply method that takes a Type as argument and yields another Type as result. A function application s(t) is then interpreted as s.apply(t). (*1) The class inherits the function type as a mixin rather than as a direct superclass. This is because in the current Scala implementation, the Function1 type is a Java interface, which cannot be used as a direct superclass of some other class. } 代入は、Type => Type 型の関数で表します。クラス Subst を１変数の関数型 Function1[Type, Type](*1) を継承させる事で実現できます。この型のインスタンスであるためには、代入 s は、引数として Type をとり結果として他の Type を戻す apply メソッドを実装する必要があります。これにより、関数適用 s(t) は s.apply(t) と解釈されます。 (*1) このクラスは、関数型を直接のスーパークラスではなくミックスインとして継承しています。これは、Scala の現在の実装では Function1 型が、他のクラスの直接のスーパークラスとして使用できない、Java の interface であるためです。 #co(){ The lookup method is abstract in class Subst. There are two concrete forms of substitutions which differ in how they implement this method. One form is defined by the emptySubst value, the other is defined by the extend method in class Subst. } lookup は Subst クラスの抽象メソッドです。代入には２つの具体的な形態があり、このメソッドの実装方法が異なります。一つは、emptySubst 値によって定義されているもの、もう一つはクラス Subst の extend メソッドによって定義されているものです。 #co(){ The next data type describes type schemes, which consist of a type and a list of names of type variables which appear universally quantified in the type scheme. For instance, the type scheme ∀a∀b.a→b would be represented in the type checker as: } 次のデータ型は、型のスキームを記述するもので、型と型の変数名リストからなり、型変数は型スキームにおいて普遍量化されて登場します。たとえば、型スキーム ∀a∀b.a→b は、型チェッカーにおいて次のように表現されます。 TypeScheme(List(Tyvar("a"), Tyvar("b")), Arrow(Tyvar("a"), Tyvar("b")))、 #co(){ The class definition of type schemes does not carry an extends clause; this means that type schemes extend directly class AnyRef. Even though there is only one possible way to construct a type scheme, a case class representation was chosen since it offers convenient ways to decompose an instance of this type into its parts. } 型スキームのクラス定義には、extends 節がありません。これは、型スキームはクラス AnyRef を直接拡張しているということです。型スキームを構築できる方法がひとつしかなくても、ケースクラス表現を選びました。この型のインスタンスを部分に分解する便利な方法が必要だったからです。 case class TypeScheme(tyvars: List[Tyvar], tpe: Type) { def newInstance: Type = { (emptySubst /: tyvars) ((s, tv) => s.extend(tv, newTyvar())) (tpe) } } #co(){ Type scheme objects come with a method newInstance, which returns the type contained in the scheme after all universally type variables have been renamed to fresh variables. The implementation of this method folds (with /:) the type scheme's type variables with an operation which extends a given substitution s by renaming a given type variable tv to a fresh type variable. The resulting substitution renames all type variables of the scheme to fresh ones. This substitution is then applied to the type part of the type scheme. } 型スキームオブジェクトには、newInstance メソッドがあります。これは、普遍量化された型変数を新しい変数に変名した後、そのスキームに含まれる型を返します。このメソッドの実装では、拡張オペレーションによって型スキームの型変数を ( /: で) 畳み込みます。拡張オペレーションは、与えられた代入 s について、与えられた型変数 tv を新しい型変数に変名することで、s を拡張します。得られた代入は、型スキームのすべての型変数を新しい名前に変名します。次にこの代入は、型スキームの型部分に適用されます。 #co(){ The last type we need in the type inferencer is Env, a type for environments, which associate variable names with type schemes. They are represented by a type alias Env in module typeInfer: } 型推論器に必要な最後の型は、環境を表す Env です。変数名と型スキームを関連づけます。これは、typeInfer モジュール内の型エイリアス Env によって表されます。 type Env = List[(String, TypeScheme)] #co(){ There are two operations on environments. The lookup function returns the type scheme associated with a given name, or null if the name is not recorded in the environment. } 「環境」には２つのオペレーションがあります。 lookup 関数は、与えられた名前に関連づけられた型スキームを返します。名前がその環境に記録されていない場合は null を返します。 def lookup(env: Env, x: String): TypeScheme = env match { case List() => null case (y, t) :: env1 => if (x == y) t else lookup(env1, x) } #co(){ The gen function turns a given type into a type scheme, quantifying over all type variables that are free in the type, but not in the environment. } gen 関数は与えられた型を、その環境になく、かつ、型で自由であるすべての型変数を量化することで、型スキームに変えます。 def gen(env: Env, t: Type): TypeScheme = TypeScheme(tyvars(t) diff tyvars(env), t) #co(){ The set of free type variables of a type is simply the set of all type variables which occur in the type. It is represented here as a list of type variables, which is constructed as follows. } ある型の自由な型変数の集合は、単に、その型に現れているすべての型変数です。ここでは、次のように構築される型変数のリストとして表現されます。 def tyvars(t: Type): List[Tyvar] = t match { case tv @ Tyvar(a) => List(tv) case Arrow(t1, t2) => tyvars(t1) union tyvars(t2) case Tycon(k, ts) => (List[Tyvar]() /: ts) ((tvs, t) => tvs union tyvars(t)) } #co(){ Note that the syntax tv @ ... in the first pattern introduces a variable which is bound to the pattern that follows. Note also that the explicit type parameter [Tyvar] in the expression of the third clause is needed to make local type inference work. The set of free type variables of a type scheme is the set of free type variables of its type component, excluding any quantified type variables: } 最初のパターンにある文法 tv @ ... は、それに続くパターンに束縛された、変数を導入します。また、三つ目の節の式にある、明示的な型パラメータ [Tyvar] は、ローカルな型推論を働かせるために必要です。型スキームの自由な型変数の集合は、量化された型変数を除いた、その型コンポーネントの自由な型変数の集合です。 def tyvars(ts: TypeScheme): List[Tyvar] = tyvars(ts.tpe) diff ts.tyvars #co(){ Finally, the set of free type variables of an environment is the union of the free type variables of all type schemes recorded in it. } 結局、環境の自由な型変数の集合は、その環境に記録されたすべての型スキームの自由な型変数の集合です。 def tyvars(env: Env): List[Tyvar] = (List[Tyvar]() /: env) ((tvs, nt) => tvs union tyvars(nt._2)) #co(){ A central operation of Hindley/Milner type checking is unification, which computes a substitution to make two given types equal (such a substitution is called a unifier). Function mgu computes the most general unifier of two given types t and u under a pre-existing substitution s. That is, it returns the most general substitution s' which extends s, and which makes s'(t) and s'(u) equal types. } Hindley/Milner型チェックの中心的な操作は単一化であり、それは２つの与えられた型を等しくする代入計算です (そのような代入は&bold(){単一化代入}と呼ばれます)。関数 mgu は、事前の代入 s 下の２つの与えられた型 ｔ と u の最も大きな単一化代入を計算します。それは、s を拡張する最も大きな代入 s' を返し、s'(t) と s'(u) を同じ型にします。 def mgu(t: Type, u: Type, s: Subst): Subst = (s(t), s(u)) match { case (Tyvar(a), Tyvar(b)) if (a == b) => case (Tyvar(a), _) if !(tyvars(u) contains a) => s.extend(Tyvar(a), u) case (_, Tyvar(a)) => mgu(u, t, s) case (Arrow(t1, t2), Arrow(u1, u2)) => mgu(t1, u1, mgu(t2, u2, s)) case (Tycon(k1, ts), Tycon(k2, us)) if (k1 == k2) => (s /: (ts zip us)) ((s, tu) => mgu(tu._1, tu._2, s)) case _ => throw new TypeError("cannot unify " + s(t) + " with " + s(u)) } #co(){ The mgu function throws a TypeError exception if no unifier substitution exists. This can happen because the two types have different type constructors at corresponding places, or because a type variable is unified with a type that contains the type variable itself. Such exceptions are modeled here as instances of case classes that inherit from the predefined Exception class. } もし単一化代入がなければ mgu 関数は TypeError 例外を送出します。このことは、２つの型が対応する場所で異なる型コンストラクタを持つとき、あるいは型変数が型変数自身からなる型と単一化されるときに起こり得ます。そのような例外を、あらかじめ定義された Exception クラスから継承する、ケースクラスのインスタンスとしてモデル化してみます。 case class TypeError(s: String) extends Exception(s) {} #co(){ The main task of the type checker is implemented by function tp. This function takes as parameters an environment env, a term e, a proto-type t , and a pre-existing substitution s. The function yields a substitution s' that extends s and that turns s'(env) ├ e:s'(t) into a derivable type judgment according to the derivation rules of the Hindley/Milner type system [Mil78]. A TypeError exception is thrown if no such substitution exists. } 型チェックの主な仕事は関数 tp によって実装されます。この関数はパラメータとして環境 env、項 e、プロトタイプ t、事前の代入 s をとります。関数 tp は s を拡張して代入 s' をもたらし、s'(env) ├ e:s'(t) を Hindler/Milner 型システム[Mil178] の推論規則に従って推論可能な型判定に変えます。もしそのような代入が存在しなければ TypeError 例外が送出されます。 def tp(env: Env, e: Term, t: Type, s: Subst): Subst = { current = e e match { case Var(x) => val u = lookup(env, x) if (u == null) throw new TypeError("undefined: " + x) else mgu(u.newInstance, t, s) case Lam(x, e1) => val a, b = newTyvar() val s1 = mgu(t, Arrow(a, b), s) val env1 = {x, TypeScheme(List(), a)} :: env tp(env1, e1, b, s1) case App(e1, e2) => val a = newTyvar() val s1 = tp(env, e1, Arrow(a, t), s) tp(env, e2, a, s1) case Let(x, e1, e2) => val a = newTyvar() val s1 = tp(env, e1, a, s) tp({x, gen(env, s1(a))} :: env, e2, t, s1) } } var current: Term = null #co(){ To aid error diagnostics, the tp function stores the currently analyzed sub-term in variable current. Thus, if type checking is aborted with a TypeError exception, this variable will contain the subterm that caused the problem. } エラー診断を支援するため、tp 関数は直近に解析されたサブ項を現変数に保存します。したがって、もし型チェックが TypeError 例外でアボートされれば、この変数が問題を引き起こしたサブ項を含みます。 #co(){ The last function of the type inference module, typeOf, is a simplified facade for tp. It computes the type of a given term e in a given environment env. It does so by creating a fresh type variable a, computing a typing substitution that makes env ├ e:a into a derivable type judgment, and returning the result of applying the substitution to a. } 型推論モジュールの最後の関数 typeOf は、tp の簡略化版です。与えられた環境 env 内の与えられた項 e の型を計算します。新しい型変数 a を生成し、型付け代入を計算して env ├ e:a を推論可能な型判定にし、代入を a に適用した結果を返します。 def typeOf(env: Env, e: Term): Type = { val a = newTyvar() tp(env, e, a, emptySubst)(a) } }// end typeInfer #co(){ To apply the type inferencer, it is convenient to have a predefined environment that contains bindings for commonly used constants. The module predefined defines an environment env that contains bindings for the types of booleans, numbers and lists together with some primitive operations over them. It also defines a fixed point operator fix, which can be used to represent recursion. } 型推論を適用するにあたり、よく使われる定数まわりの環境を事前に定義しておくと便利です。事前定義されたモジュールでは、boolean、数字、リスト等の型について、それらのプリミティブな操作とともに、関係するものを含む環境 env を定義しています。 不動点操作 fix も定義しており、再帰を表現するのに使えます。 object predefined { val booleanType = Tycon("Boolean", List()) val intType = Tycon("Int", List()) def listType(t: Type) = Tycon("List", List(t)) private def gen(t: Type): typeInfer.TypeScheme = typeInfer.gen(List(), t) private val a = typeInfer.newTyvar() val env = List( {"true", gen(booleanType)}, {"false", gen(booleanType)}, {"if", gen(Arrow(booleanType, Arrow(a, Arrow(a, a))))}, {"zero", gen(intType)}, {"succ", gen(Arrow(intType, intType))}, {"nil", gen(listType(a))}, {"cons", gen(Arrow(a, Arrow(listType(a), listType(a))))}, {"isEmpty", gen(Arrow(listType(a), booleanType))}, {"head", gen(Arrow(listType(a), a))}, {"tail", gen(Arrow(listType(a), listType(a)))}, {"fix", gen(Arrow(Arrow(a, a), a))} ) } #co(){ Here's an example how the type inferencer can be used. Let's define a function showType which returns the type of a given term computed in the predefined environment Predefined.env: } 型推論の使い方の例を見てみましょう。あらかじめ定義された環境 Predefined.env 内で計算される、与えられた項の型を返す関数 showType を定義しましょう。 object testInfer { def showType(e: Term): String = try { typeInfer.typeOf(predefined.env, e).toString } catch { case typeInfer.TypeError(msg) => "\n cannot type: " + typeInfer.current + "\n reason: " + msg } #co(){ Then the application } アプリケーションを起動すると > testInfer.showType(Lam("x", App(App(Var("cons"), Var("x")), Var("nil")))) #co(){ would give the response } 次のように応答するでしょう。 > (a6->List[a6]) #co(){ Exercise 16.0.1 Extend the Mini-ML type inferencer with a letrec construct which allows the definition of recursive functions. Syntax: } &b(){演習 16.0.1　} Mini-ML 型推論器を、letrec 構成子で再帰関数を許容するように拡張しなさい。構文 : letrec ident "=" term in term . #co(){ The typing of letrec is as for let, except that the defined identifier is visible in the defining expression. Using letrec, the length function for lists can now be defined as follows. } letrec の形は、定義された識別子が定義している式中に見えていることを除き、let と同じです。letrec を使えば、リスト用の length 関数を次のように定義できます。 letrec length = \xs. if (isEmpty xs) zero (succ (length (tail xs))) in ... #center(){[[前ページ>Chapter 15 Implicit Parameters and Conversions]]　[[ 16 章>Chapter 16 Hindley/Milner Type Inference]]　[[目次>ScalaByExample和訳]]　[[次ページ>Chapter 17 Abstractions for Concurrency]]} ---- #comment

» タグ（このWIKIのタグ一覧）: