Skip to content

Instantly share code, notes, and snippets.

@uehaj

uehaj/hindleyMilnerTypeInference.groovy

Last active August 2, 2018 06:56
Show Gist options
  • Save uehaj/8743580 to your computer and use it in GitHub Desktop.
Save uehaj/8743580 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
hindleyMilnerTypeInference.groovy
/**
* Hindley-Milner type inference
* Ported to Groovy from Scala by Example Chapter 16 code.
* (http://www.scala-lang.org/docu/files/ScalaByExample.pdf)
* refered also
* https://github.com/namin/spots/blob/master/hindleyMilner/typeInference.scala
* Japanese page of 'Scala by Example':
* http://www29.atwiki.jp/tmiya/pages/78.html
*/
import groovy.transform.*
import static TypeInfer.typeInfer
@InheritConstructors
class TypeError extends Exception {}
/**
* 構文木や式木をnewキーワード無しでオブジェクトを生成するために、
* @Newify AST変換を適用するアノテーション@ApplyNewifyを定義する。
* @AnnotationCollectorは、Groovyの合成アノテーション作成機能。
* [annocations]* @AnnocationCollector @interface 新規アノテーション {}
* で、[annocations]*を指定したのと等価な新規アノテーションを作成する。
*/
@Newify([Var,Lam,App,Let,LetRec,Tyvar,Arrow,Tycon])
@AnnotationCollector @interface ApplyNewify {}
/**
* Termおよびそのサブクラスによって構文木を構成する項を定義する。
* 項とは以下のいずれか。
* - 変数(Var)
* - λ抽象(Lambda)
* - 関数適用(App)
* - let式(Let)
* - letrec式(LetRec)
* @Immutable AST変換を適用するとTupleConstructorと同様に、
* メンバーを引数で初期化するコンストラクタが生成される。
*/
interface Term {}
@Immutable class Var implements Term { String x
@Override String toString(){ x } }
@Immutable class Lam implements Term { String x; Term e
@Override String toString(){ "λ $x . $e" } }
@Immutable class App implements Term { Term f; Term e
@Override String toString(){ "($f $e)" } }
@Immutable class Let implements Term { String x; Term e; Term f
@Override String toString(){ "let $x = $e in $f" } }
@Immutable class LetRec implements Term { String x; Term e; Term f
@Override String toString(){ "letrec $x = $e in $f" } }
/**
* Typeおよびそのサブクラスによって式木の構成要素を定義する。
* 型とは以下のいずれか。
* - 型変数(Tyvar)
* - 関数型(Arrow)
* - 型コンストラクタ呼び出し(Tycon)(具体型)
* 型変数を含む型を多相型と呼ぶ。
*/
interface Type {}
@Immutable class Tyvar implements Type { String a
@Override String toString(){ a } }
@Immutable class Arrow implements Type { Type t1; Type t2
@Override String toString(){ "($t1 -> $t2)" } }
@Immutable class Tycon implements Type { String k; List<Type> ts = []
@Override String toString(){ k + "[${ts.join(',')}]" } }
/**
* Substは「型に含まれる型変数の置換処理」を表わす。
* Subst represent a step of substitution of type variables of polymorphic type.
*
* Substはcallメソッドが定義されているので、Subst(のサブクラス)のイ
* ンスタンスに対して関数のように呼び出すことができる(Groovyの機能)。
* 例えばx = new Subst(); x(..)と呼べるということ。
* 2種類の引数の型に対してcallが定義されている。
*
* - call(Type)
* 型中に含まれる型変数を置換する。
* - call(Env)
* Envに含まれるすべての型スキーマに含まれる型変数を置換したEnvを返す。
*
* 実装機構としては、Substのサブクラスのインスタンス1つは、「Innerクラ
* ス→内部クラスを含むOuterクラスのインスタンス」、それをまた含む
* Outerクラス…というチェインを構成する。そのチェインは複数の置換処理
* を連鎖である。callはOuterクラスのcallを呼び、という再帰処理が行なわ
* れるので、複数の置換が適用できる。Innerクラスのインスタンスを作成す
* るには、extendを呼ぶ。
*/
@ApplyNewify
abstract class Subst {
/**
* 指定した型変数の置換結果を返す。
* SubstのOuter/Innerクラス関係から構成されるチェインを辿って探す。
*/
protected abstract Type lookup(Tyvar x)
abstract String toString()
/**
* 型Type t中に含まれる型変数を置換した結果の型を返す。
* 型に含まれる型変数(つまり多相型の型変数)の変数を、変化しなく
* なるまでひたすら置換する。置換の結果がさらに置換可能であれば、
* 置換がなされなくなるまで置換を繰り返す。(循環参照の対処はさ
* れてないので現実装は置換がループしてないことが前提)。
*/
Type call(Type t) {
switch (t) {
case Tyvar: def u = lookup(t); return (t == u) ? t : call(u)
// TODO: this code could throw stack overflow in the case of cyclick substitution.
case Arrow: return Arrow(call(t.t1), call(t.t2))
case Tycon: return Tycon(t.k, t.ts.collect{owner.call(it)})
}
}
/**
* 環境Env eに含まれるすべての型スキーマに含まれる型変数を置換した
* Envを返す。
*/
Env call(Env env) {
env.collectEntries { String x, TypeScheme ts ->
// assumes tyvars don't occur in this substitution
def tmp = new TypeScheme(ts.tyvars, owner.call(ts.tpe))
[x, tmp]
}
}
/**
* Innerクラスのインスタンスを生成する操作がextend()であり、「1つの
* 型変数を一つの型へ置換」に対応するインスタンス1つを返す。ただし
* extendで生成されたインスタンスは、extendを呼び出した元のオブジェ
* クト(extendにとってのthisオブジェクト) =Outerクラスのインスタン
* スとチェインしており、さらにcallにおいて、Outerクラスを呼び出し
* て実行した置換の結果に対して追加的に置換を行うので、元の置換に対
* して「拡張された置換」になる。
*/
Subst extend(Tyvar x, Type t) {
new Subst() {
Type lookup(Tyvar y) {
if (x == y) t else Subst.this.lookup(y)
}
String toString() {
Subst.this.toString() + "\n$x = $t"
}
}
}
/**
* 初期値としての空の置換を返す。
* 任意のSubstインスタンスについて、OuterクラスのOuterクラスの…
* という連鎖の最終端となる。
*/
static final Subst emptySubst = new Subst() {
Type lookup(Tyvar t) { t }
String toString() { "(empty)" }
}
}
/**
* TypeSchemeは、型抽象(∀X.T)を表わす。
* 型抽象とは、「型引数」を引数に取り、型変数を含むテンプレートのよう
* なものを本体とするような、λ式のようなもの。
*
* TypeSchemeはTypeを継承していない。その結果、Typeの構造の途中に
* TypeSchemeが表われることもない。
*
* Haskellの「forall.」は型スキーマ(型抽象)に対応しているが、このHMアル
* ゴリズムでは型スキーマ(抽象)はトップレベルの環境における識別子に直接
* 結びつく形でしか存在しない。つまりランクN多相を許していない。
*
* もしTypeSchemeが型の一種であり、型構造の任意の部分に表われ得るなら
* (つまりmgu()やtp()の型推定の解決対象の型コンストラクタなら)、ランク
* N多相が実現されることになる。
*/
@Canonical
class TypeScheme {
/**
* tyvarsは型抽象において全称量化された型変数の集合を表す。
* tyvars are set of universally quantified types in the type scheme.
*
* tyvarsは「その外側に対して名前が衝突しないことの保証」を持った型
* 変数である。なぜなら型スキーマの使用に際してnewInstance()するこ
* とでtpe中でのtyvars変数の使用がリネームされるからである。
*
* 具体的には、プログラム中にVar(x)の形で識別子xが使用されるとき、
* 識別子xの型を得るために、環境に登録された「xに対応する型スキーマ」
* を取得した上で、Type型に変換する処理(TypeScheme.newInstance())が
* 行なわれる。newInstance()は、tpe中のtyvarsと同じ名前を持った変数
* を、すべて重ならない新規の名前にリネーム置換したバージョンのtpe
* を返す。
*/
List<Tyvar> tyvars
/**
* 型のテンプレートを表わす。全称量化されている型変数と同じ型変数を
* 含んでいれば、その型変数は、型スキーマがインスタンス化されるとき
* に重ならない別名に置換される。
*/
Type tpe
/**
* 型スキーマ(型抽象)を型に具体化する操作。
*
* newInstance: TypeSchema → Type
*
* ちなみにgen()は反対に型から型スキーマを生み出す操作である。
*
* gen: Type → TypeSchema
*
* newInstance()は、全称限量指定された変数およびそれに束縛された変
* 数(つまりフリー型変数を除いた全ての型変数)の使用を、新規の変数名
* にリネームする。この操作の結果は、環境には左右されず、
* TypeSchemeインスタンスのみの情報によって確定される。(変数名のシー
* ドとなるtypeInfer.nの値には依存するが)
*
* newInstance()の結果として得られる型には全称限量で指定されていた
* 型変数は含まれない。たとえば、型スキーマ
*
* TypeSchema s = ∀ a,b . (a,b型を含む型)
*
* に対して、newInstanceした結果は、
*
* s.newInstance() = (a',b'型を含む型)
*
* であり、a,bは、a'b'に置換されるので、結果の型には決して現われな
* い。
*/
Type newInstance() {
tyvars.inject(Subst.emptySubst){ s, tv -> s.extend(tv, TypeInfer.instance.newTyvar())} (tpe)
}
String toString() { "∀ (${tyvars.join(',')}) . ($tpe)" }
}
/**
* 環境Envは、プログラムのある位置における、識別子と型情報(型スキー
* マ)の対応表である。
* Env is map of identifier to type schema.
* 環境Envは、意味的には型変数を含む制約の集合と見做すことができる。
* Env can be regarded as set of constraints of relationships concerning
* types include type variables. So HM type checker is constraints solver for it.
* 環境は、tp()が解くべき、型方程式の制約条件を表現している。
* Env: 「プログラム中の識別子→型スキーマ」の対応の集合
*
* ちなみに、Substもある種の対応表であるが、型変数の書き換えルールの
* 集合。
*
* Subst: 「型変数→型(型変数|Arrow|Tycon)」という書き換え規則の集合
*
* なお、明かにこの実装は空間効率が悪い。Scalaではタプルのリスト(連想リ
* スト)で実現されていたところをGroovy化する際に、安易にMapにしてコピー
* して受け渡すようにしたが、実用的には連想リストにすべき。
*/
@InheritConstructors
@ApplyNewify
class Env extends LinkedHashMap<String, TypeScheme> {
}
/**
* TypeInferはHM型推論の全体を含む。Scalaではオブジェクトだったので、
* @SIngletonとして定義してある。サービスメソッドを呼び出すための静的
* import可能な変数として、static typeInferを容易してある。
* 型チェックの全体の流れは、
*
* showType -> predefinedEnv
* -> typeOf -> tp -> mgu
*
* である。
*/
@ApplyNewify
@Singleton
class TypeInfer {
int n = 0
def reset() {
n = 0
}
/**
* 名前が重ならない新規の型変数を作成する。
*/
Type newTyvar() { Tyvar("a${n++}") }
/**
* 環境中にで定義された識別子xに対応する型スキーマを取得する。
*/
TypeScheme lookup(Env e, String x) {
return e.get(x)
}
/**
* 型tに含まれているすべての型変数の集合(A)から、この環境に登録され
* ているすべての型スキーマの「全称量化に関するフリー型変数の集合
* (※1)」=(B)を除外したもの((A)-(B))を全称量化することで型スキーマ
* を生成する。
*
* (※1)λx.yのとき変数xに束縛されていることを「λ束縛」と呼び、
* 「λ束縛されていない変数」をフリー変数と呼ぶが、それと同様に、
* 型変数に関する∀y...のとき型変数yに束縛されていることを「全
* 称量化束縛」と呼び、「全称量化束縛」されていない型変数を「全
* 称量化に関するフリー型変数」とする(ここで作った言葉)。
*
* 環境において「全称量化に関するフリー型変数」が発生するケースとい
* うのは、具体的にはラムダ式
*
* λ x . y
*
* において、識別子xに対応する型は、新規の型変数として環境に登録さ
* れ、そのもとでyが型推論されるが、y解析中でのxの登場はスキーマ内
* で全称量化されていない、という状態である。
*/
TypeScheme gen(Env env, Type t) {
new TypeScheme(tyvars(t) - tyvars(env), t)
}
/**
* 型に対するtyvars()は、指定した型Type t中に含まれる型変数のリスト
* を返す。
*/
List<Tyvar> tyvars(Type t) {
switch (t) {
case Tyvar: return [t]
case Arrow: return tyvars(t.t1) + tyvars(t.t2)
// 型コンストラクタ T[a,b]のとき、Tは型変数ではない。
case Tycon: return t.ts.inject([]) { List<Tyvar> tvs, Type elem -> tvs + tyvars(elem) }
}
}
/**
* 型スキーマに対するtyvars()は、指定した型スキーマTypeSchema tsの
* 型テンプレート(ts.tpe)が使用している型変数から、全称量化された変
* 数(ts.tyvars)を除外したものを返す。これは、何かというと、型スキー
* マの型テンプレート(TypeSchema.tpe)が含む「全称量化に関するフリー
* 型変数)の集合」である。
*/
List<Tyvar> tyvars(TypeScheme ts) {
tyvars(ts.tpe) - ts.tyvars
}
/**
* 環境Envに対するtyvarsは、その環境に登録されているすべての型スキー
* マに対するtvarsの値全体を返す。
* つまり、環境全体が含む「全称量化に関するフリー変数の集合」を返す。
*/
List<Tyvar> tyvars(Env env) {
env.values().inject([]){ acc, it -> acc+tyvars(it)}
}
/**
* 型tと型uのユニフィケーション。
* 型tと型uに対してs'(t) s'(u)が一致するような、sを拡張した置換s'
* を返す。
*/
Subst mgu(Type t, Type u, Subst s) {
def (st, su) = [s(t), s(u)]
if (st instanceof Tyvar && su instanceof Tyvar && st.a == su.a) { return s } // 等しい型変数
else if (st instanceof Tyvar) { return s.extend(st, su) } // 左辺が型変数
else if (su instanceof Tyvar) { return mgu(u, t, s) } // 右辺が型変数
else if (st instanceof Arrow && su instanceof Arrow) { // Arrow同士
return mgu(su.t1, st.t1, mgu(su.t2, st.t2, s))
}
else if (st instanceof Tycon && su instanceof Tycon && st.k == su.k) {
return zip(st.ts, su.ts).inject(s) { acc, it -> mgu(it[0], it[1], acc) }
}
throw new TypeError("cannot unify $st with $su")
}
/**
* 二つのリストxs=[x1,x2,x3..], ys=[y1,y2,y3]のとき、
* [[x1,y1],[x2,y2],[x3,y3]..]を返す。
*/
static zip(xs, ys) {
if (xs.size() != ys.size()) {
throw new TypeError("cannot unify $xs with $ys, number of type arguments are different")
}
Iterator itor = ys.iterator()
xs.collect { [it, itor.next()] }
}
/**
* エラーメッセージに含めるための、処理中の項への参照。
*/
Term current = null
/**
* envのもとで、eの型がt型に一致するためのsを拡張した置換s'を返す。
* 数式で書くと以下のとおり。
*
* s'(env) ├ ∈ e:s'(t)
*
* つまり、型の間の関係制約式(型変数を含む)の集合envのもとで、「eの型はtで
* ある」を満たすような、sを拡張した置換s'を値を返す。
*/
Subst tp(Env env, Term e, Type t, Subst s) {
current = e
switch (e) {
case Var:
// 変数参照eの型は、eの識別子e.xとして登録された型スキーマを実体化(全称量
// 化された変数のリネーム)をした型である。
TypeScheme u = lookup(env, e.x)
if (u == null) throw new TypeError("undefined: "+e.x)
return mgu(u.newInstance(), t, s)
case Lam:
// λで束縛される変数とletで束縛される変数の扱いの違いにつ
// いて。
// 変数(識別子)は、HMの多相型の解決において、キーとなる存在
// である。型スキーマは変数(識別子)にのみ結びつく。変数を介
// 在して得た型スキーマを基軸に、インスタンス化=全称量化=型
// 変数置換が実行される。
//
// 識別子x,yに束縛される式が多相型であるとき、型変数の解決
// の扱いに関して両者には違いがある。
//
// λx.eの場合、xに対応して環境に登録されるのは、xの型を表
// わす新規の型変数(a = newTyvar())を型テンプレートとする型
// スキーマ(型抽象)であり、かつaについては全称限量されない。
// つまり「全称量化に関するフリー型変数を含む型スキーマ」に
// なっている。
//
// let y=e1 in e2の場合、yに対応して環境に登録されるのは、
// e1の型を元にして、e1中の型変数群
//
// 「e1.tyvars-tyvars(e1.e)」…(*)
//
// を全称限量した型スキーマ(型抽象)。例えば「new
// TypeScheme(tyvars(e1), e1)」が登録される。(*)における、
// tyvars(e1.e)は、e1中のフリー型変数だが、これが生じるのは、
// λ束縛の本体の型検査の場合である。つまり
//
// \ x -> let y=e1 in e2
//
// のように、λ本体の中にlet式が出現するときに、let束縛され
// る識別子yのために登録される型スキーマでは、xに対応する型
// スキーマで使用されている型変数がフリーなので全称限量対象
// から除外される。
//
// [ここでのλとletの違いがどのような動作の違いとして現われるか?]
//
// Haskellで確認する。
//
// ghci> let x=length in x [1,2,3]+x "abc"
// 6
// ghci> (\ x -> x [1,2,3]+x "abc") length
// <interactive>:5:12:
// No instance for (Num Char)
// arising from the literal `1'
// Possible fix: add an instance declaration for (Num Char)
// In the expression: 1
// In the first argument of `x', namely `[1, 2, 3]'
// In the first argument of `(+)', namely `x [1, 2, 3]'
//
// letでのxに束縛された多相関数lengthの型(a->a)における型変
// 数aは全称限量されるので、「x [1,2,3]」と「x "abc"」それ
// ぞれにおけるxの出現それぞれでaがリネームされ(1回目はa',
// 二回目はa''など)、別の型変数扱いになる。そのため、a'と
// a''がそれぞれのIntとCharに実体化されても、型エラーになら
// ない。
//
// λの場合、xの型は全称限量されない(a->a)なので、a=Intと
// a=Charの型制約が解決できず型エラーとなる。この動作はテス
// トケースtestTpLamP2()、testTpLetP1() で確認する。
def (Tyvar a, Tyvar b) = [newTyvar(), newTyvar()]
Subst s1 = mgu(t, Arrow(a, b), s)
return tp(new Env(env)+[(e.x):new TypeScheme([], a)], e.e, b, s1)
case App:
Tyvar a = newTyvar()
Subst s1 = tp(env, e.f, Arrow(a, t), s)
return tp(env, e.e, a, s1)
case Let:
// λ x ...で束縛される変数とlet x= ..in..で束縛され
// る変数の違いについては前述の通り。
Tyvar a = newTyvar()
Subst s1 = tp(env, e.e, a, s)
return tp(new Env(env) + [(e.x):gen(s1(env), s1(a))], e.f, t, s1)
case LetRec:
def (Tyvar a, Tyvar b) = [newTyvar(), newTyvar()]
def s1 = tp(new Env(env) + [(e.x):new TypeScheme([], a)], e.e, b, s)
def s2 = mgu(a, b, s1)
return tp(new Env(env) + [(e.x):gen(s2(env), s2(a))], e.f, t, s2)
}
}
/**
* 環境envにおいてTerm eの型として推定される型を返す。
*/
Type typeOf(Env env, Term e) {
def a = newTyvar()
tp(env, e, a, Subst.emptySubst)(a)
}
/**
* 既定義の識別子(処理系の組み込み関数もしくはライブラリ関数を想定)を
* いくつか定義した型環境を返す。型のみの情報でありそれらに対する構
* 文木の情報はない。
*/
Env predefinedEnv() {
Type booleanType = Tycon("Boolean", [])
Type intType = Tycon("Int", [])
Closure<Type> listType = { Type t -> Tycon("List", [t]) }
Closure<TypeScheme> gen = { Type t -> gen(new Env(), t) }
def a = newTyvar()
return new Env(['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))])
}
/**
* 項の型を返す。
*/
String showType(Term e) {
try {
typeOf(predefinedEnv(), e).toString()
} catch (TypeError ex) {
"\n cannot type: $current"+
"\n reason: ${ex.message}"
}
}
/**
* @Singleton宣言したクラスのシングルトンはTypeInfer.instanceで保持
* されており、クラス外からも取得できる。しかし、
* 「TypeInfer.instance」が少し冗長なのと、Scala版に合せるため、シ
* ングルトンを以下で定義する静的変数TypeInfer.typeInferで取得でき
* るようにする。ただしSingletonの初期化タイミングの都合上か、遅延
* 設定のAST変換@Lazyを指定しないとうまくいかないようである。
*/
@Lazy static typeInfer = TypeInfer.instance
}
/**
* テスト
*/
@ApplyNewify([Var,Lam,App,Let,LetRec,Tyvar,Arrow,Tycon])
class TypeInferenceTest extends GroovyTestCase {
void testTerms() {
// 構文木の試験。
assert Var('a').toString() == "a"
assert Lam('a', Var('b')).toString() == "λ a . b"
assert App(Var('a'), Var('b')).toString() == "(a b)"
assert Let('a', Var('b'), Var('c')).toString() == "let a = b in c"
assert LetRec('a', Var('b'), Var('c')).toString() == "letrec a = b in c"
}
void testTermsEquals() {
// 構文木に対する@Immutableが生成した自明なequalsの動作を確認(一致する場合)。
assert Var('a') == Var('a')
assert Lam('a', Var('b')) == Lam('a', Var('b'))
assert App(Var('a'), Var('b')) == App(Var('a'), Var('b'))
assert Let('a', Var('b'), Var('c')) == Let('a', Var('b'), Var('c'))
assert LetRec('a', Var('b'), Var('c')) == LetRec('a', Var('b'), Var('c'))
}
void testTermsNotEquals() {
// 構文木に対する@Immutableが生成した自明なequalsの動作を確認(一致しない場合)。
assert Var('a') != Var('a0')
assert Lam('a', Var('b')) != Lam('a', Var('b0'))
assert App(Var('a'), Var('b')) != App(Var('a'), Var('b0'))
assert Let('a', Var('b'), Var('c')) != Let('a', Var('b'), Var('c0'))
assert LetRec('a', Var('b'), Var('c')) != LetRec('a', Var('b'), Var('c0'))
}
void testTypes1() {
// 型の構成要素に対する@Immutableが生成した自明なtoStringの動作を確認。
assert Tyvar('a').toString() == "a"
assert Arrow(Tyvar('a'), Tyvar('b')).toString() == "(a -> b)"
assert Tycon('A', []).toString() == "A[]"
assert Tycon('A', []).toString() == "A[]"
assert Tycon('A', [Tyvar('b')]).toString() == "A[b]"
}
void testTypes2() {
// 型の構成要素に対する@Immutableが生成した自明なequalsの動作を確認。
assert Tyvar('a') == Tyvar('a')
assert Arrow(Tyvar('a'), Tyvar('b')) == Arrow(Tyvar('a'), Tyvar('b'))
assert Tycon('A', []) == Tycon('A', [])
assert Tycon('A', []) == Tycon('A', [])
assert Tycon('A', [Tyvar('b')]) == Tycon('A', [Tyvar('b')])
}
void testSubstLookup1() {
// substの羃等性をチェック。置換対象ではない型変数はそのものが返る。
def subst0 = Subst.emptySubst
assert subst0.lookup(Tyvar('a')) == Tyvar('a')
}
void testSubstLookup2() {
// substの羃等性をチェック。置換対象ではない型変数はそのものが返る。
def subst0 = Subst.emptySubst
def subst1 = subst0.extend(Tyvar('a'), Tyvar('b')) // a→b
assert subst0.lookup(Tyvar('a')) == Tyvar('a') // subst0は変化していない
assert subst0 != subst1
assert subst1.lookup(Tyvar('a')) == Tyvar('b') // a == b
assert subst1.lookup(Tyvar('b')) == Tyvar('b') // b == b
}
void testSubstCallTyvar1() {
// substによる2段置換のテスト。
def subst = Subst.emptySubst
.extend(Tyvar('b'), Tyvar('c')) // b → c
.extend(Tyvar('a'), Tyvar('b')) // a → b
assert subst(Tyvar('a')) == Tyvar('c') // a (→b) == c
assert subst(Tyvar('b')) == Tyvar('c') // b == c
assert subst(Tyvar('c')) == Tyvar('c') // c == c
}
void testSubstCallTyvar2() {
// substによる2段置換のテスト。extendの順序を変更しても同じ結果 。
def subst = Subst.emptySubst
.extend(Tyvar('a'), Tyvar('b')) // a → b
.extend(Tyvar('b'), Tyvar('c')) // b → c
assert subst(Tyvar('a')) == Tyvar('c') // a (→ b) == c
assert subst(Tyvar('b')) == Tyvar('c') // b == c
assert subst(Tyvar('c')) == Tyvar('c') // c == c
}
void testSubstCallTyvar3() {
// substによる2段置換のテスト。同じ変数に対する置換は、後勝ち。
def subst0 = Subst.emptySubst
.extend(Tyvar('a'), Tyvar('x')) // a → b
def subst1 = subst0
.extend(Tyvar('a'), Tyvar('y')) // b → c
assert subst0(Tyvar('a')) == Tyvar('x') // a==x
assert subst1(Tyvar('a')) == Tyvar('y') // a==y
}
void testSubstCallTyvar4() { // Ignore me
// 循環参照のテスト。
def subst = Subst.emptySubst
.extend(Tyvar('a'), Tyvar('b')) // a = b
.extend(Tyvar('b'), Tyvar('c')) // b = c
.extend(Tyvar('c'), Tyvar('a')) // c = a
// 循環参照に対応していない(以下をコメントアウトすると無限ループする)。
// TODO: should avoid infinite loop
// assert subst(Tyvar('a')) == Tyvar('c')
// assert subst(Tyvar('b')) == Tyvar('c')
// assert subst(Tyvar('c')) == Tyvar('c')
}
void testSubstCallArrow1() {
// Arrowへの置換
def subst = Subst.emptySubst
.extend(Tyvar('a'), Arrow(Tyvar('b'), Tyvar('c'))) // a → (b->c)
assert subst.lookup(Tyvar('a')) == Arrow(Tyvar('b'), Tyvar('c')) // a == (b->c)
assert subst(Tyvar('a')) == Arrow(Tyvar('b'), Tyvar('c')) // a == (b->c)
}
void testSubstCallArrow2() {
// Arrowとtyvarへの両方を含み、置換対象のtyvarをArrowが含む。
def subst = Subst.emptySubst
.extend(Tyvar('b'), Tyvar('c')) // b→c
.extend(Tyvar('a'), Arrow(Tyvar('b'), Tyvar('c'))) // a→(b->c)
assert subst(Tyvar('a')) == Arrow(Tyvar('c'), Tyvar('c')) // a==(c->c)
def subst2 = subst.extend(Tyvar('d'), Tyvar('a')) // d→a
assert subst2(Tyvar('d')) == Arrow(Tyvar('c'), Tyvar('c')) // a==(c->c)
def subst3 = subst.extend(Tyvar('c'), Tyvar('d')) // c→d
assert subst3(Tyvar('a')) == Arrow(Tyvar('d'), Tyvar('d')) // a==(d->d)
}
void testSubstCallTycon1() { // a→B
// 単相型への置換
def subst = Subst.emptySubst
.extend(Tyvar('a'), Tycon('B', []))
assert subst(Tyvar('a')) == Tycon('B', [])
}
void testSubstCallTycon2() { // a→B[c,d]
// 多相型への置換
def subst = Subst.emptySubst
.extend(Tyvar('a'), Tycon('B', [Tyvar('c'), Tyvar('d')]))
assert subst(Tyvar('a')) == Tycon('B', [Tyvar('c'), Tyvar('d')])
}
void testSubstCallTycon3() { // a→B[c,d], b → x, c → y, d → z
// 置換の連鎖
def subst = Subst.emptySubst
.extend(Tyvar('a'), Tycon('B', [Tyvar('c'), Tyvar('d')])) // a → B[c, d]
.extend(Tyvar('b'), Tyvar('x')) // b → x
.extend(Tyvar('c'), Tyvar('y')) // c → y
.extend(Tyvar('d'), Tyvar('z')) // d → z
assert subst(Tyvar('a')) == Tycon('B', [Tyvar('y'), Tyvar('z')])
// type constructor name 'b' is not substituted.
}
void testSubstCallEnv1() {
// Envに対する置換。環境に登録されている型スキーマの型変数が(フリーか否かにかかわらず)置換される。
def subst = Subst.emptySubst
Env env = new Env()
assert subst(env).size() == 0
env['x'] = new TypeScheme([Tyvar('a'), Tyvar('b')], Arrow(Tyvar('a'),Tyvar('c')))
subst = subst.extend(Tyvar('a'), Tyvar('b'))
assert env.size() == 1
assert subst(env)['x'].toString() == "∀ (a,b) . ((b -> c))"
}
void testTypeSchemeNewInstance1() {
// 型スキーマをnewInstance()するときに型変数が置換されることの確認
typeInfer.reset()
def ts = new TypeScheme([Tyvar('a'), Tyvar('b')], Tyvar('a'))
// where 'a' is bounded
assert ts.tyvars == [Tyvar('a'), Tyvar('b')]
assert ts.tpe == Tyvar('a')
assert ts.toString() == "∀ (a,b) . (a)"
Type t1 = ts.newInstance() // 'a' of ts1.tpe is replaced to 'a0'
assert t1.toString() == 'a0'
}
void testTypeSchemeNewInstance2() {
// 型スキーマをnewInstance()するときにフリー型変数が置換されないことの確認
typeInfer.reset()
def ts = new TypeScheme([Tyvar('a'), Tyvar('b')], Tyvar('c')) // where 'c' is a free variable
assert ts.tyvars == [Tyvar('a'), Tyvar('b')]
assert ts.tpe == Tyvar('c')
assert ts.toString() == "∀ (a,b) . (c)"
Type t1 = ts.newInstance() // a,b is replaced but 'c' of ts.tpe is not changed
assert t1.toString() == 'c'
}
void testEnvLookup1() {
Env e = new Env()
// 識別子に結びつけた型スキーマが環境からlookupできること。
e['a'] = new TypeScheme([Tyvar('a'), Tyvar('b')], Tyvar('c'))
e['b'] = new TypeScheme([Tyvar('a'), Tyvar('b')], Arrow(Tyvar('c'),Tyvar('a')))
assert typeInfer.lookup(e, 'a') == new TypeScheme([Tyvar('a'), Tyvar('b')], Tyvar('c'))
assert typeInfer.lookup(e, 'b') == new TypeScheme([Tyvar('a'), Tyvar('b')], Arrow(Tyvar('c'),Tyvar('a')))
assert typeInfer.lookup(e, 'c') == null
}
void testGenType1() {
Env e = new Env()
// 型に含まれる型変数は全称量化される。
assert typeInfer.gen(e, Tyvar('a')) == new TypeScheme([Tyvar('a')], Tyvar('a'))
assert typeInfer.gen(e, Arrow(Tyvar('a'),Tyvar('b'))) == new TypeScheme([Tyvar('a'),Tyvar('b')], Arrow(Tyvar('a'),Tyvar('b')))
}
void testGenType2() {
Env e = new Env()
e['a'] = new TypeScheme([Tyvar('b'), Tyvar('c')], Tyvar('a')) // a is free
// 型に含まれる型変数は全称量化されるが、
// この環境に登録されている型スキーマでフリーな変数aは全称量化の対象外となる。
assert typeInfer.gen(e, Tyvar('a')) == new TypeScheme([], Tyvar('a'))
assert typeInfer.gen(e, Arrow(Tyvar('a'),Tyvar('b'))) == new TypeScheme([Tyvar('b')], Arrow(Tyvar('a'),Tyvar('b')))
}
void testNewTyvar1() {
// 重複しない名前の新しい型変数を作成して返す。
typeInfer.reset()
assert typeInfer.newTyvar() == Tyvar('a0')
assert typeInfer.newTyvar() == Tyvar('a1')
assert typeInfer.newTyvar() == Tyvar('a2')
assert typeInfer.newTyvar() == Tyvar('a3')
typeInfer.reset()
assert typeInfer.newTyvar() == Tyvar('a0')
assert typeInfer.newTyvar() == Tyvar('a1')
assert typeInfer.newTyvar() == Tyvar('a2')
assert typeInfer.newTyvar() == Tyvar('a3')
}
void testTyvarsType1() {
// 型に対するtyvars()は指定した型Type t中に含まれる型変数のリストが取得できること。
assert typeInfer.tyvars(Tyvar('a')) == [Tyvar('a')]
assert typeInfer.tyvars(Arrow(Tyvar('a'),Tyvar('b'))) == [Tyvar('a'),Tyvar('b')]
assert typeInfer.tyvars(Tycon('B', [Tyvar('c'), Tyvar('d')])) == [Tyvar('c'),Tyvar('d')]
assert typeInfer.tyvars(Arrow(Tycon('C',[Tyvar('a'),Tyvar('b')]),
Tycon('C',[Tyvar('c'),Tyvar('b')]))) == [Tyvar('a'),Tyvar('b'),Tyvar('c'),Tyvar('b')]
// リストなので特に重複を回避していない(元のScala版もそうなっている)
assert typeInfer.tyvars(Tycon('C',[Arrow(Tyvar('a'),Tyvar('b')),
Arrow(Tyvar('b'),Tyvar('c'))])) == [Tyvar('a'),Tyvar('b'),Tyvar('b'),Tyvar('c')]
}
void testTyvarsTypeScheume1() {
// 型スキーマに対するtyvarsは、型本体が使用している型変数から、全
// 称量化された変数を除外したものを返す。
assert typeInfer.tyvars(new TypeScheme([], Tyvar('a'))) == [Tyvar('a')]
assert typeInfer.tyvars(new TypeScheme([Tyvar('a')], Tyvar('a'))) == []
assert typeInfer.tyvars(new TypeScheme([Tyvar('a')], Tyvar('c'))) == [Tyvar('c')]
assert typeInfer.tyvars(new TypeScheme([Tyvar('a')], Arrow(Tyvar('a'),Tyvar('b')))) == [Tyvar('b')]
assert typeInfer.tyvars(new TypeScheme([Tyvar('a')], Arrow(Tyvar('a'),Tyvar('a')))) == []
}
void testTyvarsEnv1() {
// 環境Envに対するtyvarsは、その環境に登録されているすべての型スキー
// マに対するtvarsの値全体を返す。
// つまり、環境全体が含む全称量化に関するフリー変数の集合を返す。
Env e = new Env()
e['a'] = new TypeScheme([Tyvar('b'), Tyvar('c')], Tyvar('a')) // a is free
assert typeInfer.tyvars(e) == [Tyvar('a')]
e['b'] = new TypeScheme([Tyvar('f'), Tyvar('e')], Tyvar('d')) // d is free
assert typeInfer.tyvars(e) == [Tyvar('a'), Tyvar('d')]
}
void testMguTyvar1() { // a <=> a
// 同じ型変数同士のユニフィケーション(一致する)
def (Type left0, Type right0) = [Tyvar('a'), Tyvar('a')]
Subst subst = typeInfer.mgu(left0, right0, Subst.emptySubst)
def (Type left1, Type right1) = [subst(left0), subst(right0)]
assert left1 == right1
}
void testMguTyvar2() { // a<=>b
// 異る型変数同士のユニフィケーション。
// 片一方をもう一方の型変数に一致させることで一致。
def (Type left0, Type right0) = [Tyvar('a'), Tyvar('b')]
Subst subst = typeInfer.mgu(left0, right0, Subst.emptySubst) // a→b
def (Type left1, Type right1) = [subst(left0), subst(right0)] // (a→)b, b
assert left1 == right1 // b==b
}
void testMguArrow1() { // A->B <=> A->B
// 同じ単相Arrow同士のユニフィケーション。成功する。
Type left0 = Arrow(Tycon('A',[]), Tycon('B',[]))
Type right0 = Arrow(Tycon('A',[]), Tycon('B',[]))
Subst subst = typeInfer.mgu(left0, right0, Subst.emptySubst)
def (Type left1, Type right1) = [subst(left0), subst(right0)]
assert left1 == right1
}
void testMguArrow2() { // A->B <=> A->C
// 異る型の単相Arrow同士のユニフィケーション。失敗する。
Type left0 = Arrow(Tycon('A',[]), Tycon('B',[]))
Type right0 = Arrow(Tycon('A',[]), Tycon('C',[]))
def msg = shouldFail (TypeError) {
Subst subst = typeInfer.mgu(left0, right0, Subst.emptySubst)
}
assert msg == 'cannot unify C[] with B[]'
}
void testMguArrowP1() { // a->b <=> c->d
// 多相Arrow同士のユニフィケーション。成功する。
Type left0 = Arrow(Tyvar('a'), Tyvar('b'))
Type right0 = Arrow(Tyvar('c'), Tyvar('d'))
Subst subst = typeInfer.mgu(left0, right0, Subst.emptySubst)
def (Type left1, Type right1) = [subst(left0), subst(right0)]
assert left1 == right1
}
void testMguArrowP2() { // A->B <=> A->c
// 単相Arrowと多相Arrowのユニフィケーション。成功する。
Type left0 = Arrow(Tycon('A',[]), Tycon('B', []))
Type right0 = Arrow(Tycon('A',[]), Tyvar('c'))
Subst subst = typeInfer.mgu(left0, right0, Subst.emptySubst)
def (Type left1, Type right1) = [subst(left0), subst(right0)]
assert left1 == right1
assert right1 == Arrow(Tycon('A',[]), Tycon('B',[]))
}
void testMguArrowP3() { // a->B <=> C->d
// 単相Arrowと多相Arrowのユニフィケーション。成功する。
Type left0 = Arrow(Tyvar('a'), Tycon('B', []))
Type right0 = Arrow(Tycon('C',[]), Tyvar('d'))
Subst subst = typeInfer.mgu(left0, right0, Subst.emptySubst)
def (Type left1, Type right1) = [subst(left0), subst(right0)]
assert left1 == right1
assert left1 == Arrow(Tycon('C',[]), Tycon('B',[]))
assert right1 == Arrow(Tycon('C',[]), Tycon('B',[]))
}
void testMguTycon1() { // A[] <=> A[]
// 同じ単相型コンストラクタ同士のユニフィケーション(一致する)
def (Type left0, Type right0) = [Tycon('A',[]), Tycon('A',[])]
Subst subst = typeInfer.mgu(left0, right0, Subst.emptySubst)
def (Type left1, Type right1) = [subst(left0), subst(right0)]
assert left1 == right1
}
void testMguTycon2() { // A[] <=> B[]
// 異なる単相型コンストラクタ同士のユニフィケーション。
// 一致する置換はないので型エラー。
def (Type left0, Type right0) = [Tycon('A',[]), Tycon('B',[])]
def msg = shouldFail (TypeError) {
Subst subst = typeInfer.mgu(left0, right0, Subst.emptySubst)
}
assert msg == 'cannot unify A[] with B[]'
}
void testMguTycon3() { // A[AA] <=> A[]
// 異なる単相型コンストラクタ同士(引数の個数が異なる)のユニフィケーション。
// 一致する置換はないので型エラー。
// unify A[AA] and A[]. it fails because there is no valid substitution.
def (Type left0, Type right0) = [Tycon('A',[Tycon('AA',[])]), Tycon('A',[])]
def msg = shouldFail (TypeError) {
Subst subst = typeInfer.mgu(left0, right0, Subst.emptySubst)
}
assert msg == 'cannot unify [AA[]] with [], number of type arguments are different'
}
void testMguTycon4() { // A[AA] <=> A[AB]
// 異なる単相型コンストラクタ同士(引数の値が異なる)のユニフィケーション。
// 一致する置換はないので型エラー。
// unify A[AA] and A[AB]. it fails because there is no valid substitution.
def (Type left0, Type right0) = [Tycon('A',[Tycon('AA',[])]), Tycon('A',[Tycon('AB',[])])]
def msg = shouldFail (TypeError) {
Subst subst = typeInfer.mgu(left0, right0, Subst.emptySubst)
}
assert msg == 'cannot unify AA[] with AB[]'
}
void testMguTyconP1() { // A[a] <=> A[a]
// 同じ多相型コンストラクタ同士のユニフィケーション(一致する)
// unify A[a] and A[a]. success (trivial).
def (Type left0, Type right0) = [Tycon('A',[Tyvar('a')]), Tycon('A',[Tyvar('a')])]
Subst subst = typeInfer.mgu(left0, right0, Subst.emptySubst)
def (Type left1, Type right1) = [subst(left0), subst(right0)]
assert left1 == right1
}
void testMguTyconP2() { // A[a] <=> A[b]
// 引数が異なる型変数の多相型コンストラクタ同士のユニフィケーション。
// 型変数同士のmguによって一致する。(b=a)
// unify A[a] and A[b]. success with substitiution of b->a (or a->b)
def (Type left0, Type right0) = [Tycon('A',[Tyvar('a')]), Tycon('A',[Tyvar('b')])]
Subst subst = typeInfer.mgu(left0, right0, Subst.emptySubst)
def (Type left1, Type right1) = [subst(left0), subst(right0)]
assert left1 == right1
}
void testMguTyconP3() { // A[a] <=> A[] (TypeError!)
// 異なる多相型コンストラクタ同士(引数の個数が異なる)のユニフィケーション。
// 一致する置換はないので型エラー。
// unify A[a] and A[]. it fails because there is no valid substitution.
def (Type left0, Type right0) = [Tycon('A',[Tyvar('a')]), Tycon('A',[])]
def msg = shouldFail (TypeError) {
Subst subst = typeInfer.mgu(left0, right0, Subst.emptySubst)
}
assert msg == 'cannot unify [a] with [], number of type arguments are different'
}
void testMguTyconP4() { // A[a] <=> B[a] (TypeError!)
// 異なる多相型コンストラクタ同士(引数の値が異なる)のユニフィケーション。
// 一致する置換はないので型エラー。
// unify A[a] and B[a]. it fails because there is no valid substitution.
def (Type left0, Type right0) = [Tycon('A',[Tyvar('a',)]), Tycon('B',[Tyvar('a')])]
def msg = shouldFail (TypeError) {
Subst subst = typeInfer.mgu(left0, right0, Subst.emptySubst)
}
assert msg == 'cannot unify A[a] with B[a]'
}
void testMguTyvarArrow1() { // a <=> B->C
// 型変数aと関数型B->Cのユニフィケーション。成功する(a=B->C)
// unify type variable a and functional type B->C. succeed with a=B->C
def (Type left0, Type right0) = [Tyvar('a'), Arrow(Tycon('B',[]), Tycon('C',[]))]
Subst subst = typeInfer.mgu(left0, right0, Subst.emptySubst)
def (Type left1, Type right1) = [subst(left0), subst(right0)]
assert left1 == right1
assert left1 == Arrow(Tycon('B',[]), Tycon('C',[]))
}
void testMguTyvarArrow2() { // B->C <=> a
// 関数型B->Cと型変数aのユニフィケーション。成功する(a=B->C)。
// unify functional type B->C and type variable a. succeed with a=B->C
def (Type left0, Type right0) = [Arrow(Tycon('B',[]), Tycon('C',[])), Tyvar('a')]
Subst subst = typeInfer.mgu(left0, right0, Subst.emptySubst)
def (Type left1, Type right1) = [subst(left0), subst(right0)]
assert left1 == right1
assert right1 == Arrow(Tycon('B',[]), Tycon('C',[]))
}
void testMguTyvarTycon1() { // a <=> B
// 型変数aと型コンストラクタB[]のユニフィケーション。成功する(a=B[])
// unify type variable a and type constructor B[]. succeed with a=B[]
def (Type left0, Type right0) = [Tyvar('a'), Tycon('B',[])]
Subst subst = typeInfer.mgu(left0, right0, Subst.emptySubst)
def (Type left1, Type right1) = [subst(left0), subst(right0)]
assert left1 == right1
assert left1 == Tycon('B',[])
}
void testMguTyvarTycon2() { // B <=> a
// 型コンストラクタB[]と型変数aのユニフィケーション。成功する(a=B[])。
// unify type constructor B[] and type variable a. succeed with a=B[]
def (Type left0, Type right0) = [Tycon('B',[]), Tyvar('a')]
Subst subst = typeInfer.mgu(left0, right0, Subst.emptySubst)
def (Type left1, Type right1) = [subst(left0), subst(right0)]
assert left1 == right1
assert right1 == Tycon('B',[])
}
void testMguTyconArrow1() { // A <=> a->b (TypeError!)
// 型コンストラクタとArrowのユニフィケーション。失敗する。
// unify type constructor and arrow. it fails.
def (Type left0, Type right0) = [Tycon('A',[]), Arrow(Tyvar('a'), Tyvar('b'))]
def msg = shouldFail (TypeError) {
Subst subst = typeInfer.mgu(left0, right0, Subst.emptySubst)
}
assert msg == 'cannot unify A[] with (a -> b)'
}
void testZip() {
assert TypeInfer.zip([1,2,3],["a","b","c"]) == [[1,"a"],[2,"b"],[3,"c"]]
assert TypeInfer.zip([],[]) == []
shouldFail (TypeError) { TypeInfer.zip([1,2],["a","b","c"]) == [[1,"a"],[2,"b"],[3,"c"]] }
}
void testTpVar1() { // [a:A] |- a : A
Env env = new Env()
env['a'] = new TypeScheme([], Tycon('A',[]))
Type type = Tyvar('a')
Subst subst = typeInfer.tp(env, Var('a'), type, Subst.emptySubst)
assert subst(type) == Tycon('A', [])
}
void testTpVar2() { // [] |- a : TypeError!
Env env = new Env()
Type type = Tyvar('a')
def msg = shouldFail (TypeError) {
Subst subst = typeInfer.tp(env, Var('a'), type, Subst.emptySubst)
}
assert msg =='undefined: a'
}
void testTpLam1() { // [1:Int] |- (\a -> a) 1 : Int
Env env = new Env()
env['1'] = new TypeScheme([], Tycon('Int',[]))
Type type = Tyvar('a')
Subst subst = typeInfer.tp(env, App(Lam('a', Var('a')),Var('1')), type, Subst.emptySubst)
assert subst(type) == Tycon('Int',[])
}
void testTpLam2() { // [true:Bool, 1:Int] |- (\a -> true) 1 : Bool
Env env = new Env()
env['true'] = new TypeScheme([], Tycon('Boolean',[]))
env['1'] = new TypeScheme([], Tycon('Int',[]))
Type type = Tyvar('a')
Subst subst = typeInfer.tp(env, App(Lam('a', Var('true')),Var('1')), type, Subst.emptySubst)
assert subst(type) == Tycon('Boolean',[])
}
void testTpLam3() { // [1:Int, a:Bool] |- (\a -> a) 1 : Int
Env env = new Env()
env['1'] = new TypeScheme([], Tycon('Int',[]))
env['a'] = new TypeScheme([], Tycon('Boolean',[]))
Type type = Tyvar('a')
Subst subst = typeInfer.tp(env, App(Lam('a', Var('a')),Var('1')), type, Subst.emptySubst)
assert subst(type) == Tycon('Int',[])
}
void testTpLam4() { // [add:Int->(Int->Int),1:Int] |- add(1)1) : Int
Env env = new Env()
env['add'] = new TypeScheme([], Arrow(Tycon('Int',[]), Arrow(Tycon('Int',[]),Tycon('Int',[]))))
env['1'] = new TypeScheme([], Tycon('Int',[]))
Type type = Tyvar('a')
Subst subst = typeInfer.tp(env, App(App(Var('add'), Var('1')),Var('1')), type, Subst.emptySubst)
assert subst(type) == Tycon('Int',[])
}
void testTpLet1() { // [1:Int] |- let a = 1 in a : Int
Env env = new Env()
env['1'] = new TypeScheme([], Tycon('Int',[]))
Type type = Tyvar('a')
Subst subst = typeInfer.tp(env, Let('a', Var('1'), Var('a')), type, Subst.emptySubst)
assert subst(type) == Tycon('Int',[])
}
void testTpLet2() { // [true:Bool, 1:Int] |- let a = 1 in true : Bool
Env env = new Env()
env['true'] = new TypeScheme([], Tycon('Boolean',[]))
env['1'] = new TypeScheme([], Tycon('Int',[]))
Type type = Tyvar('a')
Subst subst = typeInfer.tp(env, Let('a', Var('1'), Var('true')), type, Subst.emptySubst)
assert subst(type) == Tycon('Boolean',[])
}
void testTpLet3() { // [1:Int, a:Bool] |- let a = 1 in a : Int
Env env = new Env()
env['1'] = new TypeScheme([], Tycon('Int',[]))
env['a'] = new TypeScheme([], Tycon('Boolean',[]))
Type type = Tyvar('a')
Subst subst = typeInfer.tp(env, Let('a', Var('1'), Var('a')), type, Subst.emptySubst)
assert subst(type) == Tycon('Int',[])
}
void testTpLet4() { // [1:Int] |- let a = a in 1 : (TypeError!)
Env env = new Env()
env['1'] = new TypeScheme([], Tycon('Int',[]))
Type type = Tyvar('a')
def msg = shouldFail (TypeError) {
Subst subst = typeInfer.tp(env, Let('a', Var('a'), Var('1')), type, Subst.emptySubst)
}
assert msg == 'undefined: a'
}
void testTpLamLet1() {
// [e1:Bool, 1:Int] |- (\ x -> let y=e1 in x) 1 : Int
//
// 「 \ x -> let y=e1 in x」のように、λ本体の中にlet式が出現す
// るときに、let束縛される識別子yのために登録される型スキーマで
// は、xに対応する型スキーマで使用されている型変数が全称限量対
// 象から除外される。
//
Env env = new Env()
env['e1'] = new TypeScheme([], Tycon('Boolean',[]))
env['1'] = new TypeScheme([], Tycon('Int',[]))
Type type = Tyvar('a')
Subst subst = typeInfer.tp(env,
App(
Lam('x',
Let('y', Var('e1'), Var('x'))),
Var('1')
),
type, Subst.emptySubst)
assert subst(type) == Tycon('Int',[])
}
void testTpLamP1() {
// [s:String, 7:Int] |- (\ x -> x s) (\x->7) : Int
// λ変数xに多相関数を束縛し、x->Intでインスタンス化する。
// bind lambda variable x to polymorphic function and instantiate with x->Int type.
Env env = new Env()
env['s'] = new TypeScheme([], Tycon('String',[]))
env['7'] = new TypeScheme([], Tycon('Int',[]))
Type type = Tyvar('a')
Subst subst = typeInfer.tp(env,
App(
Lam('x',
App(Var('x'), Var('s'))),
Lam('x', Var('7'))
),
type, Subst.emptySubst)
assert subst(type) == Tycon('Int',[])
}
void testTpLamP2() {
// [s:String, c:Char, 7:Int, add:Int->(Int->Int)] |- (\ x -> (add(x s))(x c)) (\x->7) : TypeError!
// λ変数xが多相関数(a->Int)のとき、異なる型での複数回のインスタンス化でエラーになることの確認。
/// if the lambda variable x is polymorphic function(a->Int), it should be error
// every type instantiation for each different type occurence of x.
Env env = new Env()
env['add'] = new TypeScheme([], Arrow(Tycon('Int',[]), Arrow(Tycon('Int',[]),Tycon('Int',[]))))
env['c'] = new TypeScheme([], Tycon('Char',[]))
env['s'] = new TypeScheme([], Tycon('String',[]))
env['7'] = new TypeScheme([], Tycon('Int',[]))
Type type = Tyvar('a')
def msg = shouldFail(TypeError) {
Subst subst = typeInfer.tp(env,
App(
Lam('x',
App(
App(Var('add'),
App(Var('x'), Var('s'))),
App(Var('x'), Var('c')))
),
Lam('x', Var('7'))
),
type, Subst.emptySubst)
}
assert msg == 'cannot unify Char[] with String[]'
}
void testTpLetP1() {
// [s:String, c:Char, 7:Int, add:Int->(Int->Int)] |- (let x=(\x->7) in (add(x s))(x c)) : Int
// let変数xが多相関数(a->Int)のとき、異なる型での複数回のインスタンス化でエラーにならないことの確認。
/// if the let variable x is polymorphic function(a->Int), it should not be error
// every type instantiation for each different type occurence of x.
Env env = new Env()
env['add'] = new TypeScheme([], Arrow(Tycon('Int',[]), Arrow(Tycon('Int',[]),Tycon('Int',[]))))
env['c'] = new TypeScheme([], Tycon('Char',[]))
env['s'] = new TypeScheme([], Tycon('String',[]))
env['7'] = new TypeScheme([], Tycon('Int',[]))
Type type = Tyvar('a')
Subst subst = typeInfer.tp(env,
Let('x',
Lam('x', Var('7')),
App(
App(Var('add'),
App(Var('x'), Var('s'))),
App(Var('x'), Var('c')))
),
type, Subst.emptySubst)
assert subst(type) == Tycon('Int',[])
}
void testTpLetRec1() { // [1:Int] |- letrec a = 1 in a : Int
Env env = new Env()
env['1'] = new TypeScheme([], Tycon('Int',[]))
Type type = Tyvar('a')
Subst subst = typeInfer.tp(env, LetRec('a', Var('1'), Var('a')), type, Subst.emptySubst)
assert subst(type) == Tycon('Int',[])
}
void testTpLetRec2() { // [true:Bool, 1:Int] |- letrec a = 1 in true : Bool
Env env = new Env()
env['true'] = new TypeScheme([], Tycon('Boolean',[]))
env['1'] = new TypeScheme([], Tycon('Int',[]))
Type type = Tyvar('a')
Subst subst = typeInfer.tp(env, LetRec('a', Var('1'), Var('true')), type, Subst.emptySubst)
assert subst(type) == Tycon('Boolean',[])
}
void testTpLetRec3() { // [1:Int, a:Bool] |- letrec a = 1 in a : Int
Env env = new Env()
env['1'] = new TypeScheme([], Tycon('Int',[]))
env['a'] = new TypeScheme([], Tycon('Boolean',[]))
Type type = Tyvar('a')
Subst subst = typeInfer.tp(env, LetRec('a', Var('1'), Var('a')), type, Subst.emptySubst)
assert subst(type) == Tycon('Int',[])
}
void testTpLetRecP1() {
// [s:String, c:Char, 7:Int, add:Int->(Int->Int)] |- (letrec x=(\x->7) in (add(x s))(x c)) : Int
// letrec変数xが多相関数(a->Int)のとき、異なる型での複数回のインスタンス化でエラー
// にならないことの確認。
/// if the letrec variable x is polymorphic function(a->Int), it should not be error
// every type instantiation for each different type occurence of x.
Env env = new Env()
env['add'] = new TypeScheme([], Arrow(Tycon('Int',[]), Arrow(Tycon('Int',[]),Tycon('Int',[]))))
env['c'] = new TypeScheme([], Tycon('Char',[]))
env['s'] = new TypeScheme([], Tycon('String',[]))
env['7'] = new TypeScheme([], Tycon('Int',[]))
Type type = Tyvar('a')
Subst subst = typeInfer.tp(env,
LetRec('x',
Lam('x', Var('7')),
App(
App(Var('add'),
App(Var('x'), Var('s'))),
App(Var('x'), Var('c')))
),
type, Subst.emptySubst)
assert subst(type) == Tycon('Int',[])
}
void testTpLetRec4() { // [1:Int] |- letrec a = a in 1 : Int
Env env = new Env()
env['1'] = new TypeScheme([], Tycon('Int',[]))
Type type = Tyvar('a')
Subst subst = typeInfer.tp(env, LetRec('a', Var('a'), Var('1')), type, Subst.emptySubst)
assert subst(type) == Tycon('Int',[])
}
void testTypeOf() { // [] |- (\a->a) : a->a
Env env = new Env()
def type = typeInfer.typeOf(env, Lam('a', Var('a'))) // a->a
assert type instanceof Arrow
assert type.t1 == type.t2
}
void testPredefinedEnv() {
Env env = typeInfer.predefinedEnv()
assert typeInfer.typeOf(env, Var('true')) == Tycon('Boolean',[])
}
void testShowType() {
// 最終的な型判定のテスト群。
assert typeInfer.showType(Var('true')) == 'Boolean[]'
assert typeInfer.showType(Var('xtrue')) == "\n cannot type: xtrue\n reason: undefined: xtrue"
assert typeInfer.showType(Var('zero')) == 'Int[]'
def intList = App(App(Var('cons'),
Var('zero')),
Var('nil'))
def zero = Var('zero')
def one = App(Var('succ'), Var('zero'))
assert typeInfer.showType(intList) == 'List[Int[]]'
assert typeInfer.showType(App(Var('isEmpty'), intList)) == 'Boolean[]'
assert typeInfer.showType(App(Var('head'), intList)) == 'Int[]'
assert typeInfer.showType(App(Var('tail'), App(Var('head'), intList))).startsWith("\n cannot type: zero\n reason: cannot unify Int[] with List[")
assert typeInfer.showType(App(Var('tail'), App(Var('tail'), intList))) == 'List[Int[]]' // runtime erro but type check is OK
assert typeInfer.showType(App(App(App(Var('if'), Var('true')), zero), one)) == 'Int[]'
assert typeInfer.showType(App(App(App(Var('if'), Var('true')), intList), one)) == "\n cannot type: succ\n reason: cannot unify List[Int[]] with Int[]"
def listLenTest = LetRec('len',
Lam('xs',
App(App(App(Var('if'),
App(Var('isEmpty'), Var('xs'))),
Var('zero')),
App(Var('succ'),
App(Var('len'),
App(Var('tail'),
Var('xs'))))
)),
App(Var('len'),
App(
App(Var('cons'),
Var('zero')),
Var('nil'))
)
);
assert listLenTest.toString() == 'letrec len = λ xs . (((if (isEmpty xs)) zero) (succ (len (tail xs)))) in (len ((cons zero) nil))'
assert typeInfer.showType(listLenTest) == "Int[]"
}
}
junit.textui.TestRunner.run(TypeInferenceTest)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment