「Chapter 16 Hindley/Milner Type Inference」の編集履歴（バックアップ）一覧に戻る
*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 calledMini-ML. Abstract syntax trees for theMini-ML are represented by the following data type of Terms.
この章では、Hindly/Milnerスタイルの型推論システムの開発を通して、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
}
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.
四つの木のコンストラクタがあります：変数を表す'Var'、関数抽象を表す'Lam'、関数適用を表す'App'、そしてlet式を表す'Let'。それぞれのケースクラスは、AnyのメソッドtoStringをオーバーライドしており、項は判読可能なように表示できます。
We next define the types that are computed by the inference system.
次に、推論システムによって計算される型を定義します。
We next define the types that are computed by the inference system.
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("[", ",", "]"))
}
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メソッドを実装しています。
Note that Type is a sealed class. Thismeans 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 typewith exactly three alternatives.
By contrast, type Term is an open algebraic type for which further alternatives can be defined.
'Type'が'sealed'なクラスである事に注意してください。これは、'Type'を拡張するサブクラスやデータコンストラクタ'Type'が、定義されている定義の列の外部では作成できない事を意味します。これにより、'Type'は閉じた代数データ型で、代替物が確実に3つである事が保証されます。逆に、型'Term'は開いた代数型であり、さらなる代替物が定義可能です。
The main parts of the type inferencer are contained in object typeInfer. We start with a utility function which creates fresh type variables:
型推論器の主な部品は'typeInfer'オブジェクトに含まれます。新しい型変数を生成するユーティリティー関数から始めましょう：
object typeInfer {
private var n: Int = 0
def newTyvar(): Type = { n += 1; Tyvar("a" + n) }
We next define a class for substitutions. A substitution is an idempotent function fromtype variables to types. Itmaps 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 amapping from types to types.
次に、代入を表すクラスを定義します。代入は型変数から型への冪等な関数です。有限な数の型変数を何らかの型にマップし、ほかのすべての型変数には変更を加えません。代入の意味は、型から型へのマッピングへの拡張された点指向(？point-wise)です。
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 }
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](*). 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).
(* 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'を1変数の関数型 'Function1[Type, Type]'を継承させる事で実現できます。この型のインスタンスであるために、代入's'は、'Type'を引数にとって結果として他の'Type'を戻す'apply'メソッドを実装する必要があります※。これにより、関数適用's(t)'は's.apply(t)'と解釈されます。
※このクラスは、関数型を直接のスーパークラスではなくmixinとして継承しています。これは、Scalaの現在の実装ではFunction1型が、他のクラスの直接のスーパークラスとして使用できないJavaのinterfaceであるためです。
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'メソッドによって定義されているものです。
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:
次のデータ型は、型のスキームを記述するもので、その型スキームにおいてあまねく量化(？quantified)されて表れる型変数名のリストと、型からなります。たとえば、型スキーム'∀a∀b.a→b'は、型チェッカーにおいて次のように表現されます。
TypeScheme(List(Tyvar("a"), Tyvar("b")), Arrow(Tyvar("a"), Tyvar("b"))) .
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)
}
}
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'を新しい型変数に変名します。結果の代入は、型スキームのすべての型変数が新しい名前に変名されます。この代入は、型スキームの型部分に適用されます。
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'によって表されます。
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)
}
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)
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))
}
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
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))
A central operation ofHindley/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 s0 which extends s, and which makes '''s’(t) and s’(u)''' equal types.
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))
}
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.
case class TypeError(s: String) extends Exception(s) {}
(尻切れ)
