Last active
June 27, 2023 18:25
-
-
Save pocarist/d276210532940f51b353 to your computer and use it in GitHub Desktop.
Hindley-Milner型推論アルゴリズムをF#で書いてみた - http://d.hatena.ne.jp/pocarist/20141220/1419087653
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (* 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 | |
| */ *) | |
| (* F#: | |
| * Hindley-Milner type inference | |
| * Ported to F# from Groovy. | |
| * http://uehaj.hatenablog.com/entry/2014/02/01/183039 | |
| *) | |
| module HindleyMilnerTypeInference | |
| exception TypeError of string | |
| //F#: Listの引き算を定義 | |
| let inline (--) a b = | |
| let s = Set.ofList b | |
| a | |
| |> List.filter (not << s.Contains) | |
| (* /** | |
| * Termおよびそのサブクラスによって構文木を構成する項を定義する。 | |
| * 項とは以下のいずれか。 | |
| * - 変数(Var) | |
| * - λ抽象(Lambda) | |
| * - 関数適用(App) | |
| * - let式(Let) | |
| * - letrec式(LetRec) | |
| * @Immutable AST変換を適用するとTupleConstructorと同様に、 | |
| * メンバーを引数で初期化するコンストラクタが生成される。 | |
| */ *) | |
| type Term = | |
| | Var of string | |
| | Lam of string * Term | |
| | App of Term * Term | |
| | Let of string * Term * Term | |
| | LetRec of string * Term * Term | |
| with | |
| override this.ToString() = | |
| match this with | |
| | Var x -> x | |
| | Lam(x, e) -> sprintf "λ %s . %s" x <| e.ToString() | |
| | App(f, e) -> sprintf "(%s %s)" <| f.ToString() <| e.ToString() | |
| | Let(x, e, f) -> sprintf "let %s = %s in %s" x <| e.ToString() <| f.ToString() | |
| | LetRec(x, e, f) -> sprintf "letrec %s = %s in %s" x <| e.ToString() <| f.ToString() | |
| (* /** | |
| * Typeおよびそのサブクラスによって式木の構成要素を定義する。 | |
| * 型とは以下のいずれか。 | |
| * - 型変数(Tyvar) | |
| * - 関数型(Arrow) | |
| * - 型コンストラクタ呼び出し(Tycon)(具体型) | |
| * 型変数を含む型を多相型と呼ぶ。 | |
| */ *) | |
| type Type = | |
| | Tyvar of tyvar | |
| | Arrow of Type * Type | |
| | Tycon of string * Type list | |
| with | |
| override this.ToString() = | |
| match this with | |
| | Tyvar x -> x | |
| | Arrow(t1, t2) -> sprintf "(%s -> %s)" <| t1.ToString() <| t2.ToString() | |
| | Tycon(k, ts) -> k + "[" + (ts |> List.map string |> String.concat ",") + "]" | |
| //F#: 本当はTypeを継承したTyvar型を定義したかったけど、 | |
| // うまいやり方が分からないのでstringの別名としてtyvarを作ってお茶を濁す | |
| and tyvar = string | |
| let tyvar_of_Type = function | |
| | Tyvar(x) -> x | |
| | _ -> raise <| new System.InvalidCastException() | |
| let tyvars_of_Types = List.map tyvar_of_Type | |
| (* /** | |
| * 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を呼ぶ。 | |
| */ *) | |
| //F#: F#には上記のようなcallメソッドはないので普通に、let x = new Subst(); x.call(..)とする | |
| [<AbstractClass>] | |
| type Subst() = | |
| (* /** | |
| * 指定した型変数の置換結果を返す。 | |
| * SubstのOuter/Innerクラス関係から構成されるチェインを辿って探す。 | |
| */ *) | |
| abstract member lookup : tyvar -> Type | |
| //F#: 本当はtyvarにキャストしたい | |
| member this.lookup (t : Type) : Type = | |
| match t with | |
| | Tyvar(a) -> | |
| this.lookup a | |
| | _ -> raise <| new System.InvalidCastException() | |
| (* /** | |
| * 型Type t中に含まれる型変数を置換した結果の型を返す。 | |
| * 型に含まれる型変数(つまり多相型の型変数)の変数を、変化しなく | |
| * なるまでひたすら置換する。置換の結果がさらに置換可能であれば、 | |
| * 置換がなされなくなるまで置換を繰り返す。(循環参照の対処はさ | |
| * れてないので現実装は置換がループしてないことが前提)。 | |
| */ *) | |
| member this.call (t : Type) : Type = | |
| match t with | |
| | Tyvar(a) -> | |
| let u = this.lookup a | |
| if t = u then t else this.call u | |
| | Arrow(t1, t2) -> | |
| Arrow(this.call t1, this.call t2) | |
| | Tycon(k, ts) -> | |
| Tycon(k, List.map (fun (i : Type) -> this.call i) ts) | |
| (* /** | |
| * 環境Env eに含まれるすべての型スキーマに含まれる型変数を置換した | |
| * Envを返す。 | |
| */ *) | |
| member this.call (env : Env) : Env = | |
| env | |
| |> Map.map (fun x (ts : TypeScheme) -> | |
| new TypeScheme(ts.tyvars, this.call ts.tpe)) | |
| (* /** | |
| * Innerクラスのインスタンスを生成する操作がextend()であり、「1つの | |
| * 型変数を一つの型へ置換」に対応するインスタンス1つを返す。ただし | |
| * extendで生成されたインスタンスは、extendを呼び出した元のオブジェ | |
| * クト(extendにとってのthisオブジェクト) =Outerクラスのインスタン | |
| * スとチェインしており、さらにcallにおいて、Outerクラスを呼び出し | |
| * て実行した置換の結果に対して追加的に置換を行うので、元の置換に対 | |
| * して「拡張された置換」になる。 | |
| */ *) | |
| member this.extend (x : tyvar, t : Type) = | |
| { new Subst() with | |
| override this2.lookup y = if x = y then t else this.lookup y | |
| override this2.ToString() = this.ToString() + (sprintf "\n%s = %s" x <| t.ToString()) | |
| } | |
| //F#: 本当はtyvarにキャストしたい | |
| member this.extend (x : Type, t : Type) = | |
| match x with | |
| | Tyvar(a) -> | |
| this.extend(a, t) | |
| | _ -> raise <| new System.InvalidCastException() | |
| (* /** | |
| * 初期値としての空の置換を返す。 | |
| * 任意のSubstインスタンスについて、OuterクラスのOuterクラスの… | |
| * という連鎖の最終端となる。 | |
| */ *) | |
| static member emptySubst = | |
| { new Subst() with | |
| override this.lookup t = Tyvar(t) | |
| override this.ToString() = "(empty)" | |
| } | |
| (* /** | |
| * TypeSchemeは、型抽象(∀X.T)を表わす。 | |
| * 型抽象とは、「型引数」を引数に取り、型変数を含むテンプレートのよう | |
| * なものを本体とするような、λ式のようなもの。 | |
| * | |
| * TypeSchemeはTypeを継承していない。その結果、Typeの構造の途中に | |
| * TypeSchemeが表われることもない。 | |
| * | |
| * Haskellの「forall.」は型スキーマ(型抽象)に対応しているが、このHMアル | |
| * ゴリズムでは型スキーマ(抽象)はトップレベルの環境における識別子に直接 | |
| * 結びつく形でしか存在しない。つまりランクN多相を許していない。 | |
| * | |
| * もしTypeSchemeが型の一種であり、型構造の任意の部分に表われ得るなら | |
| * (つまりmgu()やtp()の型推定の解決対象の型コンストラクタなら)、ランク | |
| * N多相が実現されることになる。 | |
| */ *) | |
| and TypeScheme (tyvars : tyvar list, tpe : Type) = | |
| (* /** | |
| * 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 | |
| * を返す。 | |
| */ *) | |
| member this.tyvars = tyvars | |
| (* /** | |
| * 型のテンプレートを表わす。全称量化されている型変数と同じ型変数を | |
| * 含んでいれば、その型変数は、型スキーマがインスタンス化されるとき | |
| * に重ならない別名に置換される。 | |
| */ *) | |
| member this.tpe : 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'に置換されるので、結果の型には決して現われな | |
| * い。 | |
| */ *) | |
| member this.newInstance () = | |
| tyvars | |
| |> List.fold (fun (s:Subst) tv -> | |
| s.extend(tv, TypeInfer.typeInfer.newTyvar()) ) Subst.emptySubst | |
| |> fun x -> x.call tpe | |
| override this.ToString() = sprintf "∀ (%s) . (%s)" (String.concat "," tyvars) <| tpe.ToString() | |
| (* /** | |
| * 環境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にしてコピー | |
| * して受け渡すようにしたが、実用的には連想リストにすべき。 | |
| */ *) | |
| //F#: F#も素直にmapで実装 | |
| and Env = Map<string, TypeScheme> | |
| (* /** | |
| * TypeInferはHM型推論の全体を含む。Scalaではオブジェクトだったので、 | |
| * @SIngletonとして定義してある。サービスメソッドを呼び出すための静的 | |
| * import可能な変数として、static typeInferを容易してある。 | |
| * 型チェックの全体の流れは、 | |
| * | |
| * showType -> predefinedEnv | |
| * -> typeOf -> tp -> mgu | |
| * | |
| * である。 | |
| */ *) | |
| and TypeInfer private () = | |
| (* /** | |
| * エラーメッセージに含めるための、処理中の項への参照。 | |
| */ *) | |
| let current = ref None | |
| let n = ref 0 | |
| //F#: Singletonとして実装したい | |
| static let instance = lazy new TypeInfer() | |
| static member typeInfer : TypeInfer = instance.Value | |
| member this.reset () = | |
| n := 0 | |
| (* /** | |
| * 名前が重ならない新規の型変数を作成する。 | |
| */ *) | |
| member this.newTyvar () = | |
| let ret = Tyvar("a"+string !n) | |
| incr n | |
| ret | |
| (* /** | |
| * 環境中にで定義された識別子xに対応する型スキーマを取得する。 | |
| */ *) | |
| member this.lookup (e : Env, x) = | |
| e.TryFind x | |
| (* /** | |
| * 型tに含まれているすべての型変数の集合(A)から、この環境に登録され | |
| * ているすべての型スキーマの「全称量化に関するフリー型変数の集合 | |
| * (※1)」=(B)を除外したもの((A)-(B))を全称量化することで型スキーマ | |
| * を生成する。 | |
| * | |
| * (※1)λx.yのとき変数xに束縛されていることを「λ束縛」と呼び、 | |
| * 「λ束縛されていない変数」をフリー変数と呼ぶが、それと同様に、 | |
| * 型変数に関する∀y...のとき型変数yに束縛されていることを「全 | |
| * 称量化束縛」と呼び、「全称量化束縛」されていない型変数を「全 | |
| * 称量化に関するフリー型変数」とする(ここで作った言葉)。 | |
| * | |
| * 環境において「全称量化に関するフリー型変数」が発生するケースとい | |
| * うのは、具体的にはラムダ式 | |
| * | |
| * λ x . y | |
| * | |
| * において、識別子xに対応する型は、新規の型変数として環境に登録さ | |
| * れ、そのもとでyが型推論されるが、y解析中でのxの登場はスキーマ内 | |
| * で全称量化されていない、という状態である。 | |
| */ *) | |
| member this.gen (env : Env, t : Type) = | |
| new TypeScheme(this.tyvars(t) -- this.tyvars(env), t) | |
| (* /** | |
| * 型に対するtyvars()は、指定した型Type t中に含まれる型変数のリスト | |
| * を返す。 | |
| */ *) | |
| member this.tyvars (t : Type) = | |
| match t with | |
| | Tyvar a -> | |
| [a] | |
| | Arrow(t1, t2) -> | |
| this.tyvars(t1) @ this.tyvars(t2) | |
| | Tycon(k, ts) -> | |
| List.fold (fun tvs (elem : Type) -> tvs @ this.tyvars elem) [] ts | |
| (* /** | |
| * 型スキーマに対するtyvars()は、指定した型スキーマTypeSchema tsの | |
| * 型テンプレート(ts.tpe)が使用している型変数から、全称量化された変 | |
| * 数(ts.tyvars)を除外したものを返す。これは、何かというと、型スキー | |
| * マの型テンプレート(TypeSchema.tpe)が含む「全称量化に関するフリー | |
| * 型変数)の集合」である。 | |
| */ *) | |
| member this.tyvars (ts : TypeScheme) = | |
| this.tyvars(ts.tpe) -- ts.tyvars | |
| (* /** | |
| * 環境Envに対するtyvarsは、その環境に登録されているすべての型スキー | |
| * マに対するtvarsの値全体を返す。 | |
| * つまり、環境全体が含む「全称量化に関するフリー変数の集合」を返す。 | |
| */ *) | |
| member this.tyvars (env : Env) = | |
| env | |
| |> Map.fold (fun acc _ it -> acc @ this.tyvars it) [] | |
| (* /** | |
| * 型tと型uのユニフィケーション。 | |
| * 型tと型uに対してs'(t) s'(u)が一致するような、sを拡張した置換s' | |
| * を返す。 | |
| */ *) | |
| member this.mgu (t : Type, u : Type, s : Subst) = | |
| let st, su = s.call(t), s.call(u) | |
| match st, su with | |
| | Tyvar(stv), Tyvar(suv) when stv = suv -> s | |
| | Tyvar(stv), _ -> s.extend(stv, su) | |
| | _, Tyvar(suv) -> this.mgu(u, t, s) | |
| | Arrow(st1, st2), Arrow(su1, su2) -> | |
| this.mgu(su1, st1, this.mgu(su2, st2, s)) | |
| | Tycon(kt, tst), Tycon(ku, tsu) when kt = ku -> | |
| TypeInfer.zip (tst, tsu) | |
| |> List.fold (fun acc (it0, it1) -> this.mgu(it0, it1, acc)) s | |
| | _ -> | |
| raise <| TypeError(sprintf "cannot unify %s with %s" <| st.ToString() <| su.ToString()) | |
| (* /** | |
| * 二つのリストxs=[x1,x2,x3..], ys=[y1,y2,y3]のとき、 | |
| * [[x1,y1],[x2,y2],[x3,y3]..]を返す。 | |
| */ *) | |
| static member zip (xs, ys) = | |
| if List.length xs <> List.length ys then | |
| raise <| TypeError(sprintf "cannot unify %s with %s, number of type arguments are different" <| xs.ToString() <| ys.ToString()) | |
| List.zip xs ys | |
| (* /** | |
| * envのもとで、eの型がt型に一致するためのsを拡張した置換s'を返す。 | |
| * 数式で書くと以下のとおり。 | |
| * | |
| * s'(env) ├ ∈ e:s'(t) | |
| * | |
| * つまり、型の間の関係制約式(型変数を含む)の集合envのもとで、「eの型はtで | |
| * ある」を満たすような、sを拡張した置換s'を値を返す。 | |
| */ *) | |
| member this.tp (env : Env, e : Term, t, s) = | |
| current := Some e | |
| match e with | |
| | Var(x) -> | |
| // 変数参照eの型は、eの識別子e.xとして登録された型スキーマを実体化(全称量 | |
| // 化された変数のリネーム)をした型である。 | |
| let uopt = this.lookup(env, x) | |
| match uopt with | |
| | None -> raise <| TypeError("undefined: "+x) | |
| | Some u -> this.mgu (u.newInstance(), t, s) | |
| | Lam(x, ee) -> | |
| // λで束縛される変数と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() で確認する。 | |
| let a, b = this.newTyvar(), this.newTyvar() | |
| let s1 = this.mgu(t, Arrow(a, b), s) | |
| let env1 = env.Add(x, (new TypeScheme([], a))) | |
| this.tp (env1, ee, b, s1) | |
| | App(f, ee) -> | |
| let a = this.newTyvar() | |
| let s1 = this.tp (env, f, Arrow(a, t), s) | |
| this.tp (env, ee, a, s1) | |
| | Let(x, ee, f) -> | |
| // λ x ...で束縛される変数とlet x= ..in..で束縛され | |
| // る変数の違いについては前述の通り。 | |
| let a = this.newTyvar() | |
| let s1 = this.tp (env, ee, a, s) | |
| let env1 = env.Add(x, this.gen (s1.call env, s1.call(a))) | |
| this.tp (env1, f, t, s1) | |
| | LetRec(x, ee, f) -> | |
| let a, b = this.newTyvar(), this.newTyvar() | |
| let env1 = env.Add(x, (new TypeScheme([], a))) | |
| let s1 = this.tp (env1, ee, b, s) | |
| let s2 = this.mgu(a, b, s1) | |
| let env2 = env.Add(x, this.gen (s2.call env, s2.call(a))) | |
| this.tp (env2, f, t, s2) | |
| (* /** | |
| * 環境envにおいてTerm eの型として推定される型を返す。 | |
| */ *) | |
| member this.typeOf (env, e) = | |
| let a = this.newTyvar() | |
| this.tp(env, e, a, Subst.emptySubst).call(a) | |
| (* /** | |
| * 既定義の識別子(処理系の組み込み関数もしくはライブラリ関数を想定)を | |
| * いくつか定義した型環境を返す。型のみの情報でありそれらに対する構 | |
| * 文木の情報はない。 | |
| */ *) | |
| member this.predefinedEnv () : Env = | |
| let booleanType = Tycon("Boolean", []) | |
| let intType = Tycon("Int", []) | |
| let listType = fun t -> Tycon("List", [t]) | |
| let gen = fun t -> this.gen (Map.empty, t) | |
| let a = this.newTyvar() | |
| ["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))] | |
| |> Map.ofList | |
| (* /** | |
| * 項の型を返す。 | |
| */ *) | |
| member this.showType (e :Term) = | |
| try | |
| this.typeOf(this.predefinedEnv(), e).ToString() | |
| with TypeError ex -> | |
| "\n cannot type: "+ current.Value.Value.ToString() + | |
| "\n reason: " + ex | |
| (* /** | |
| * テスト | |
| */ *) | |
| module TypeInferenceTest = | |
| let typeInfer = TypeInfer.typeInfer | |
| let shouldFail_TypeError f = | |
| try | |
| f () | |
| "should not come here ???" | |
| with | |
| | TypeError(msg) -> msg | |
| | e -> e.Message | |
| let 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") | |
| let 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"))) | |
| let 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"))) | |
| let 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]") | |
| let 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")])) | |
| let testSubstLookup1() = | |
| // substの羃等性をチェック。置換対象ではない型変数はそのものが返る。 | |
| let subst0 = Subst.emptySubst | |
| assert (subst0.lookup(Tyvar("a")) = Tyvar("a")) | |
| let testSubstLookup2() = | |
| // substの羃等性をチェック。置換対象ではない型変数はそのものが返る。 | |
| let subst0 = Subst.emptySubst | |
| let 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 | |
| let testSubstCallTyvar1() = | |
| // substによる2段置換のテスト。 | |
| let subst = Subst.emptySubst | |
| let subst = subst.extend(Tyvar("b"), Tyvar("c")) // b → c | |
| let subst = subst.extend(Tyvar("a"), Tyvar("b")) // a → b | |
| assert (subst.call(Tyvar("a")) = Tyvar("c")) // a (→b) = c | |
| assert (subst.call(Tyvar("b")) = Tyvar("c")) // b = c | |
| assert (subst.call(Tyvar("c")) = Tyvar("c")) // c = c | |
| let testSubstCallTyvar2() = | |
| // substによる2段置換のテスト。extendの順序を変更しても同じ結果 。 | |
| let subst = Subst.emptySubst | |
| let subst = subst.extend(Tyvar("a"), Tyvar("b")) // a → b | |
| let subst = subst.extend(Tyvar("b"), Tyvar("c")) // b → c | |
| assert (subst.call(Tyvar("a")) = Tyvar("c")) // a (→ b) = c | |
| assert (subst.call(Tyvar("b")) = Tyvar("c")) // b = c | |
| assert (subst.call(Tyvar("c")) = Tyvar("c")) // c = c | |
| let testSubstCallTyvar3() = | |
| // substによる2段置換のテスト。同じ変数に対する置換は、後勝ち。 | |
| let subst0 = Subst.emptySubst | |
| let subst0 = subst0.extend(Tyvar("a"), Tyvar("x")) // a → b | |
| let subst1 = subst0 | |
| let subst1 = subst1.extend(Tyvar("a"), Tyvar("y")) // b → c | |
| assert (subst0.call(Tyvar("a")) = Tyvar("x")) // a=x | |
| assert (subst1.call(Tyvar("a")) = Tyvar("y")) // a=y | |
| let testSubstCallTyvar4() = // Ignore me | |
| // 循環参照のテスト。 | |
| let subst = Subst.emptySubst | |
| let subst = subst.extend(Tyvar("a"), Tyvar("b")) // a = b | |
| let subst = subst.extend(Tyvar("b"), Tyvar("c")) // b = c | |
| let subst = subst.extend(Tyvar("c"), Tyvar("a")) // c = a | |
| () | |
| // 循環参照に対応していない(以下をコメントアウトすると無限ループする)。 | |
| // TODO: should alet infinite loop | |
| // assert (subst(Tyvar("a")) = Tyvar("c")) | |
| // assert (subst(Tyvar("b")) = Tyvar("c")) | |
| // assert (subst(Tyvar("c")) = Tyvar("c")) | |
| let testSubstCallArrow1() = | |
| // Arrowへの置換 | |
| let subst = Subst.emptySubst | |
| let subst = subst.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.call(Tyvar("a")) = Arrow(Tyvar("b"), Tyvar("c"))) // a = (b->c) | |
| let testSubstCallArrow2() = | |
| // Arrowとtyvarへの両方を含み、置換対象のtyvarをArrowが含む。 | |
| let subst = Subst.emptySubst | |
| let subst = subst.extend(Tyvar("b"), Tyvar("c")) // b→c | |
| let subst = subst.extend(Tyvar("a"), Arrow(Tyvar("b"), Tyvar("c"))) // a→(b->c) | |
| assert (subst.call(Tyvar("a")) = Arrow(Tyvar("c"), Tyvar("c"))) // a=(c->c) | |
| let subst2 = subst.extend(Tyvar("d"), Tyvar("a")) // d→a | |
| assert (subst2.call(Tyvar("d")) = Arrow(Tyvar("c"), Tyvar("c"))) // a=(c->c) | |
| let subst3 = subst.extend(Tyvar("c"), Tyvar("d")) // c→d | |
| assert (subst3.call(Tyvar("a")) = Arrow(Tyvar("d"), Tyvar("d"))) // a=(d->d) | |
| let testSubstCallTycon1() = // a→B | |
| // 単相型への置換 | |
| let subst = Subst.emptySubst | |
| let subst = subst.extend(Tyvar("a"), Tycon("B", [])) | |
| assert (subst.call(Tyvar("a")) = Tycon("B", [])) | |
| let testSubstCallTycon2() = // a→B[c,d] | |
| // 多相型への置換 | |
| let subst = Subst.emptySubst | |
| let subst = subst.extend(Tyvar("a"), Tycon("B", [Tyvar("c"); Tyvar("d")])) | |
| assert (subst.call(Tyvar("a")) = Tycon("B", [Tyvar("c"); Tyvar("d")])) | |
| let testSubstCallTycon3() = // a→B[c,d], b → x, c → y, d → z | |
| // 置換の連鎖 | |
| let subst = Subst.emptySubst | |
| let subst = subst.extend(Tyvar("a"), Tycon("B", [Tyvar("c"); Tyvar("d")])) // a → B[c, d] | |
| let subst = subst.extend(Tyvar("b"), Tyvar("x")) // b → x | |
| let subst = subst.extend(Tyvar("c"), Tyvar("y")) // c → y | |
| let subst = subst.extend(Tyvar("d"), Tyvar("z")) // d → z | |
| assert (subst.call(Tyvar("a")) = Tycon("B", [Tyvar("y"); Tyvar("z")])) | |
| // type constructor name "b" is not substituted. | |
| let testSubstCallEnv1() = | |
| // Envに対する置換。環境に登録されている型スキーマの型変数が(フリーか否かにかかわらず)置換される。 | |
| let subst = Subst.emptySubst | |
| let env = Map.empty | |
| assert (subst.call(env).Count = 0) | |
| let env = env.Add("x", new TypeScheme(["a"; "b"], Arrow(Tyvar("a"),Tyvar("c")))) | |
| let subst = subst.extend(Tyvar("a"), Tyvar("b")) | |
| assert (env.Count = 1) | |
| assert (subst.call(env).["x"].ToString() = "∀ (a,b) . ((b -> c))") | |
| let testTypeSchemeNewInstance1() = | |
| // 型スキーマをnewInstance()するときに型変数が置換されることの確認 | |
| typeInfer.reset() | |
| let ts = new TypeScheme(["a"; "b"], Tyvar("a")) | |
| // where "a" is bounded | |
| assert (ts.tyvars = ["a"; "b"]) | |
| assert (ts.tpe = Tyvar("a")) | |
| assert (ts.ToString() = "∀ (a,b) . (a)") | |
| let t1 = ts.newInstance() // "a" of ts1.tpe is replaced to "a0" | |
| assert (t1.ToString() = "a0") | |
| let testTypeSchemeNewInstance2() = | |
| // 型スキーマをnewInstance()するときにフリー型変数が置換されないことの確認 | |
| typeInfer.reset() | |
| let ts = new TypeScheme(["a"; "b"], Tyvar("c")) // where "c" is a free variable | |
| assert (ts.tyvars = ["a"; "b"]) | |
| assert (ts.tpe = Tyvar("c")) | |
| assert (ts.ToString() = "∀ (a,b) . (c)") | |
| let t1 = ts.newInstance() // a,b is replaced but "c" of ts.tpe is not changed | |
| assert (t1.ToString() = "c") | |
| let testEnvLookup1() = | |
| let e : Env = Map.empty | |
| // 識別子に結びつけた型スキーマが環境からlookupできること。 | |
| let e = e.Add("a", new TypeScheme(["a"; "b"], Tyvar("c"))) | |
| let e = e.Add("b", new TypeScheme(["a"; "b"], Arrow(Tyvar("c"),Tyvar("a")))) | |
| assert (typeInfer.lookup(e, "a").Value.ToString() = (new TypeScheme(["a"; "b"], Tyvar("c"))).ToString()) | |
| assert (typeInfer.lookup(e, "b").Value.ToString() = (new TypeScheme(["a"; "b"], Arrow(Tyvar("c"),Tyvar("a")))).ToString()) | |
| assert (typeInfer.lookup(e, "c") = None) | |
| let testGenType1() = | |
| let e : Env = Map.empty | |
| // 型に含まれる型変数は全称量化される。 | |
| assert (typeInfer.gen(e, Tyvar("a")).ToString() = (new TypeScheme(["a"], Tyvar("a"))).ToString()) | |
| assert (typeInfer.gen(e, Arrow(Tyvar("a"),Tyvar("b"))).ToString() = (new TypeScheme(["a"; "b"], Arrow(Tyvar("a"),Tyvar("b")))).ToString()) | |
| let testGenType2() = | |
| let e : Env = Map.empty | |
| let e = e.Add("a", new TypeScheme(["b"; "c"], Tyvar("a"))) // a is free | |
| // 型に含まれる型変数は全称量化されるが、 | |
| // この環境に登録されている型スキーマでフリーな変数aは全称量化の対象外となる。 | |
| assert (typeInfer.gen(e, Tyvar("a")).ToString() = (new TypeScheme([], Tyvar("a"))).ToString()) | |
| assert (typeInfer.gen(e, Arrow(Tyvar("a"),Tyvar("b"))).ToString() = (new TypeScheme(["b"], Arrow(Tyvar("a"),Tyvar("b")))).ToString()) | |
| let 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")) | |
| let testTyvarsType1() = | |
| // 型に対するtyvars()は指定した型Type t中に含まれる型変数のリストが取得できること。 | |
| assert (typeInfer.tyvars(Tyvar("a")) = tyvars_of_Types [Tyvar("a")]) | |
| assert (typeInfer.tyvars(Arrow(Tyvar("a"),Tyvar("b"))) = tyvars_of_Types [Tyvar("a"); Tyvar("b")]) | |
| assert (typeInfer.tyvars(Tycon("B", [Tyvar("c"); Tyvar("d")])) = tyvars_of_Types [Tyvar("c");Tyvar("d")]) | |
| assert (typeInfer.tyvars(Arrow(Tycon("C",[Tyvar("a");Tyvar("b")]), | |
| Tycon("C",[Tyvar("c");Tyvar("b")]))) = tyvars_of_Types [Tyvar("a");Tyvar("b");Tyvar("c");Tyvar("b")]) | |
| // リストなので特に重複を回避していない(元のScala版もそうなっている) | |
| assert (typeInfer.tyvars(Tycon("C",[Arrow(Tyvar("a"),Tyvar("b")); | |
| Arrow(Tyvar("b"),Tyvar("c"))])) = tyvars_of_Types [Tyvar("a");Tyvar("b");Tyvar("b");Tyvar("c")]) | |
| let testTyvarsTypeScheume1() = | |
| // 型スキーマに対するtyvarsは、型本体が使用している型変数から、全 | |
| // 称量化された変数を除外したものを返す。 | |
| assert (typeInfer.tyvars(new TypeScheme([], Tyvar("a"))) = tyvars_of_Types [Tyvar("a")]) | |
| assert (typeInfer.tyvars(new TypeScheme(tyvars_of_Types [Tyvar("a")], Tyvar("a"))) = []) | |
| assert (typeInfer.tyvars(new TypeScheme(tyvars_of_Types [Tyvar("a")], Tyvar("c"))) = tyvars_of_Types [Tyvar("c")]) | |
| assert (typeInfer.tyvars(new TypeScheme(tyvars_of_Types [Tyvar("a")], Arrow(Tyvar("a"),Tyvar("b")))) = tyvars_of_Types [Tyvar("b")]) | |
| assert (typeInfer.tyvars(new TypeScheme(tyvars_of_Types [Tyvar("a")], Arrow(Tyvar("a"),Tyvar("a")))) = []) | |
| let testTyvarsEnv1() = | |
| // 環境Envに対するtyvarsは、その環境に登録されているすべての型スキー | |
| // マに対するtvarsの値全体を返す。 | |
| // つまり、環境全体が含む全称量化に関するフリー変数の集合を返す。 | |
| let e : Env = Map.empty | |
| let e = e.Add("a", new TypeScheme(["b"; "c"], Tyvar("a"))) // a is free | |
| assert (typeInfer.tyvars(e) = tyvars_of_Types [Tyvar("a")]) | |
| let e = e.Add("b", new TypeScheme(["f"; "e"], Tyvar("d"))) // d is free | |
| assert (typeInfer.tyvars(e) = tyvars_of_Types [Tyvar("a"); Tyvar("d")]) | |
| let testMguTyvar1() = // a <=> a | |
| // 同じ型変数同士のユニフィケーション(一致する) | |
| let left0, right0 = Tyvar("a"), Tyvar("a") | |
| let subst = typeInfer.mgu(left0, right0, Subst.emptySubst) | |
| let left1, right1 = subst.call(left0), subst.call(right0) | |
| assert (left1 = right1) | |
| let testMguTyvar2() = // a<=>b | |
| // 異る型変数同士のユニフィケーション。 | |
| // 片一方をもう一方の型変数に一致させることで一致。 | |
| let left0, right0 = Tyvar("a"), Tyvar("b") | |
| let subst = typeInfer.mgu(left0, right0, Subst.emptySubst) | |
| let left1, right1 = subst.call(left0), subst.call(right0) | |
| assert (left1 = right1) // b=b | |
| let testMguArrow1() = // A->B <=> A->B | |
| // 同じ単相Arrow同士のユニフィケーション。成功する。 | |
| let left0 = Arrow(Tycon("A",[]), Tycon("B",[])) | |
| let right0 = Arrow(Tycon("A",[]), Tycon("B",[])) | |
| let subst = typeInfer.mgu(left0, right0, Subst.emptySubst) | |
| let left1, right1 = subst.call(left0), subst.call(right0) | |
| assert (left1 = right1) | |
| let testMguArrow2() = // A->B <=> A->C | |
| // 異る型の単相Arrow同士のユニフィケーション。失敗する。 | |
| let left0 = Arrow(Tycon("A",[]), Tycon("B",[])) | |
| let right0 = Arrow(Tycon("A",[]), Tycon("C",[])) | |
| let msg = shouldFail_TypeError (fun () -> | |
| typeInfer.mgu(left0, right0, Subst.emptySubst) |> ignore) | |
| assert (msg = "cannot unify C[] with B[]") | |
| let testMguArrowP1() = // a->b <=> c->d | |
| // 多相Arrow同士のユニフィケーション。成功する。 | |
| let left0 = Arrow(Tyvar("a"), Tyvar("b")) | |
| let right0 = Arrow(Tyvar("c"), Tyvar("d")) | |
| let subst = typeInfer.mgu(left0, right0, Subst.emptySubst) | |
| let (left1, right1) = subst.call(left0), subst.call(right0) | |
| assert (left1 = right1) | |
| let testMguArrowP2() = // A->B <=> A->c | |
| // 単相Arrowと多相Arrowのユニフィケーション。成功する。 | |
| let left0 = Arrow(Tycon("A",[]), Tycon("B", [])) | |
| let right0 = Arrow(Tycon("A",[]), Tyvar("c")) | |
| let subst = typeInfer.mgu(left0, right0, Subst.emptySubst) | |
| let (left1, right1) = subst.call(left0), subst.call(right0) | |
| assert (left1 = right1) | |
| assert (right1 = Arrow(Tycon("A",[]), Tycon("B",[]))) | |
| let testMguArrowP3() = // a->B <=> C->d | |
| // 単相Arrowと多相Arrowのユニフィケーション。成功する。 | |
| let left0 = Arrow(Tyvar("a"), Tycon("B", [])) | |
| let right0 = Arrow(Tycon("C",[]), Tyvar("d")) | |
| let subst = typeInfer.mgu(left0, right0, Subst.emptySubst) | |
| let (left1, right1) = subst.call(left0), subst.call(right0) | |
| assert (left1 = right1) | |
| assert (left1 = Arrow(Tycon("C",[]), Tycon("B",[]))) | |
| assert (right1 = Arrow(Tycon("C",[]), Tycon("B",[]))) | |
| let testMguTycon1() = // A[] <=> A[] | |
| // 同じ単相型コンストラクタ同士のユニフィケーション(一致する) | |
| let (left0, right0) = Tycon("A",[]), Tycon("A",[]) | |
| let subst = typeInfer.mgu(left0, right0, Subst.emptySubst) | |
| let (left1, right1) = subst.call(left0), subst.call(right0) | |
| assert (left1 = right1) | |
| let testMguTycon2() = // A[] <=> B[] | |
| // 異なる単相型コンストラクタ同士のユニフィケーション。 | |
| // 一致する置換はないので型エラー。 | |
| let (left0, right0) = Tycon("A",[]), Tycon("B",[]) | |
| let msg = shouldFail_TypeError (fun () -> | |
| typeInfer.mgu(left0, right0, Subst.emptySubst) |> ignore) | |
| assert (msg = "cannot unify A[] with B[]") | |
| let testMguTycon3() = // A[AA] <=> A[] | |
| // 異なる単相型コンストラクタ同士(引数の個数が異なる)のユニフィケーション。 | |
| // 一致する置換はないので型エラー。 | |
| // unify A[AA] and A[]. it fails because there is no valid substitution. | |
| let (left0, right0) = Tycon("A",[Tycon("AA",[])]), Tycon("A",[]) | |
| let msg = shouldFail_TypeError (fun () -> | |
| ignore <| typeInfer.mgu(left0, right0, Subst.emptySubst)) | |
| assert (msg = "cannot unify [AA[]] with [], number of type arguments are different") | |
| let testMguTycon4() = // A[AA] <=> A[AB] | |
| // 異なる単相型コンストラクタ同士(引数の値が異なる)のユニフィケーション。 | |
| // 一致する置換はないので型エラー。 | |
| // unify A[AA] and A[AB]. it fails because there is no valid substitution. | |
| let (left0, right0) = Tycon("A",[Tycon("AA",[])]), Tycon("A",[Tycon("AB",[])]) | |
| let msg = shouldFail_TypeError (fun () -> | |
| ignore <| typeInfer.mgu(left0, right0, Subst.emptySubst)) | |
| assert (msg = "cannot unify AA[] with AB[]") | |
| let testMguTyconP1() = // A[a] <=> A[a] | |
| // 同じ多相型コンストラクタ同士のユニフィケーション(一致する) | |
| // unify A[a] and A[a]. success (trivial). | |
| let (left0, right0) = Tycon("A",[Tyvar("a")]), Tycon("A",[Tyvar("a")]) | |
| let subst = typeInfer.mgu(left0, right0, Subst.emptySubst) | |
| let (left1, right1) = subst.call(left0), subst.call(right0) | |
| assert (left1 = right1) | |
| let testMguTyconP2() = // A[a] <=> A[b] | |
| // 引数が異なる型変数の多相型コンストラクタ同士のユニフィケーション。 | |
| // 型変数同士のmguによって一致する。(b=a) | |
| // unify A[a] and A[b]. success with substitiution of b->a (or a->b) | |
| let (left0, right0) = Tycon("A",[Tyvar("a")]), Tycon("A",[Tyvar("b")]) | |
| let subst = typeInfer.mgu(left0, right0, Subst.emptySubst) | |
| let (left1, right1) = subst.call(left0), subst.call(right0) | |
| assert (left1 = right1) | |
| let testMguTyconP3() = // A[a] <=> A[] (TypeError!) | |
| // 異なる多相型コンストラクタ同士(引数の個数が異なる)のユニフィケーション。 | |
| // 一致する置換はないので型エラー。 | |
| // unify A[a] and A[]. it fails because there is no valid substitution. | |
| let (left0, right0) = Tycon("A",[Tyvar("a")]), Tycon("A",[]) | |
| let msg = shouldFail_TypeError (fun () -> | |
| ignore <| typeInfer.mgu(left0, right0, Subst.emptySubst)) | |
| assert (msg = "cannot unify [a] with [], number of type arguments are different") | |
| let testMguTyconP4() = // A[a] <=> B[a] (TypeError!) | |
| // 異なる多相型コンストラクタ同士(引数の値が異なる)のユニフィケーション。 | |
| // 一致する置換はないので型エラー。 | |
| // unify A[a] and B[a]. it fails because there is no valid substitution. | |
| let (left0, right0) = Tycon("A",[Tyvar("a")]), Tycon("B",[Tyvar("a")]) | |
| let msg = shouldFail_TypeError (fun () -> | |
| ignore <| typeInfer.mgu(left0, right0, Subst.emptySubst)) | |
| assert (msg = "cannot unify A[a] with B[a]") | |
| let testMguTyvarArrow1() = // a <=> B->C | |
| // 型変数aと関数型B->Cのユニフィケーション。成功する(a=B->C) | |
| // unify type variable a and functional type B->C. succeed with a=B->C | |
| let (left0, right0) = Tyvar("a"), Arrow(Tycon("B",[]), Tycon("C",[])) | |
| let subst = typeInfer.mgu(left0, right0, Subst.emptySubst) | |
| let (left1, right1) = subst.call(left0), subst.call(right0) | |
| assert (left1 = right1) | |
| assert (left1 = Arrow(Tycon("B",[]), Tycon("C",[]))) | |
| let testMguTyvarArrow2() = // B->C <=> a | |
| // 関数型B->Cと型変数aのユニフィケーション。成功する(a=B->C)。 | |
| // unify functional type B->C and type variable a. succeed with a=B->C | |
| let (left0, right0) = Arrow(Tycon("B",[]), Tycon("C",[])), Tyvar("a") | |
| let subst = typeInfer.mgu(left0, right0, Subst.emptySubst) | |
| let (left1, right1) = subst.call(left0), subst.call(right0) | |
| assert (left1 = right1) | |
| assert (right1 = Arrow(Tycon("B",[]), Tycon("C",[]))) | |
| let testMguTyvarTycon1() = // a <=> B | |
| // 型変数aと型コンストラクタB[]のユニフィケーション。成功する(a=B[]) | |
| // unify type variable a and type constructor B[]. succeed with a=B[] | |
| let (left0, right0) = Tyvar("a"), Tycon("B",[]) | |
| let subst = typeInfer.mgu(left0, right0, Subst.emptySubst) | |
| let (left1, right1) = subst.call(left0), subst.call(right0) | |
| assert (left1 = right1) | |
| assert (left1 = Tycon("B",[])) | |
| let testMguTyvarTycon2() = // B <=> a | |
| // 型コンストラクタB[]と型変数aのユニフィケーション。成功する(a=B[])。 | |
| // unify type constructor B[] and type variable a. succeed with a=B[] | |
| let (left0, right0) = Tycon("B",[]), Tyvar("a") | |
| let subst = typeInfer.mgu(left0, right0, Subst.emptySubst) | |
| let (left1, right1) = subst.call(left0), subst.call(right0) | |
| assert (left1 = right1) | |
| assert (right1 = Tycon("B",[])) | |
| let testMguTyconArrow1() = // A <=> a->b (TypeError!) | |
| // 型コンストラクタとArrowのユニフィケーション。失敗する。 | |
| // unify type constructor and arrow. it fails. | |
| let (left0, right0) = Tycon("A",[]), Arrow(Tyvar("a"), Tyvar("b")) | |
| let msg = shouldFail_TypeError (fun () -> | |
| ignore <| typeInfer.mgu(left0, right0, Subst.emptySubst) ) | |
| assert (msg = "cannot unify A[] with (a -> b)") | |
| // let 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"]] | |
| let testTpVar1() = // [a:A] |- a : A | |
| let env : Env = Map.empty | |
| let env = env.Add("a", new TypeScheme([], Tycon("A",[]))) | |
| let typ = Tyvar("a") | |
| let subst = typeInfer.tp(env, Var("a"), typ, Subst.emptySubst) | |
| assert (subst.call(typ) = Tycon("A", [])) | |
| let testTpVar2() = // [] |- a : TypeError! | |
| let env : Env = Map.empty | |
| let typ = Tyvar("a") | |
| let msg = shouldFail_TypeError (fun () -> | |
| ignore <| typeInfer.tp(env, Var("a"), typ, Subst.emptySubst) | |
| ) | |
| assert (msg ="undefined: a") | |
| let testTpLam1() = // [1:Int] |- (\a -> a) 1 : Int | |
| let env : Env = Map.empty | |
| let env = env.Add("1", new TypeScheme([], Tycon("Int",[]))) | |
| let typ = Tyvar("a") | |
| let subst = typeInfer.tp(env, App(Lam("a", Var("a")),Var("1")), typ, Subst.emptySubst) | |
| assert (subst.call(typ) = Tycon("Int",[])) | |
| let testTpLam2() = // [true:Bool, 1:Int] |- (\a -> true) 1 : Bool | |
| let env : Env = Map.empty | |
| let env = env.Add("true", new TypeScheme([], Tycon("Boolean",[]))) | |
| let env = env.Add("1", new TypeScheme([], Tycon("Int",[]))) | |
| let typ = Tyvar("a") | |
| let subst = typeInfer.tp(env, App(Lam("a", Var("true")),Var("1")), typ, Subst.emptySubst) | |
| assert (subst.call(typ) = Tycon("Boolean",[])) | |
| let testTpLam3() = // [1:Int, a:Bool] |- (\a -> a) 1 : Int | |
| let env : Env = Map.empty | |
| let env = env.Add("1", new TypeScheme([], Tycon("Int",[]))) | |
| let env = env.Add("a", new TypeScheme([], Tycon("Boolean",[]))) | |
| let typ = Tyvar("a") | |
| let subst = typeInfer.tp(env, App(Lam("a", Var("a")),Var("1")), typ, Subst.emptySubst) | |
| assert (subst.call(typ) = Tycon("Int",[])) | |
| let testTpLam4() = // [add:Int->(Int->Int),1:Int] |- add(1)1) : Int | |
| let env : Env = Map.empty | |
| let env = env.Add("add", new TypeScheme([], Arrow(Tycon("Int",[]), Arrow(Tycon("Int",[]),Tycon("Int",[]))))) | |
| let env = env.Add("1", new TypeScheme([], Tycon("Int",[]))) | |
| let typ = Tyvar("a") | |
| let subst = typeInfer.tp(env, App(App(Var("add"), Var("1")),Var("1")), typ, Subst.emptySubst) | |
| assert (subst.call(typ) = Tycon("Int",[])) | |
| let testTpLet1() = // [1:Int] |- let a = 1 in a : Int | |
| let env : Env = Map.empty | |
| let env = env.Add("1", new TypeScheme([], Tycon("Int",[]))) | |
| let typ = Tyvar("a") | |
| let subst = typeInfer.tp(env, Let("a", Var("1"), Var("a")), typ, Subst.emptySubst) | |
| assert (subst.call(typ) = Tycon("Int",[])) | |
| let testTpLet2() = // [true:Bool, 1:Int] |- let a = 1 in true : Bool | |
| let env : Env = Map.empty | |
| let env = env.Add("true", new TypeScheme([], Tycon("Boolean",[]))) | |
| let env = env.Add("1", new TypeScheme([], Tycon("Int",[]))) | |
| let typ = Tyvar("a") | |
| let subst = typeInfer.tp(env, Let("a", Var("1"), Var("true")), typ, Subst.emptySubst) | |
| assert (subst.call(typ) = Tycon("Boolean",[])) | |
| let testTpLet3() = // [1:Int, a:Bool] |- let a = 1 in a : Int | |
| let env : Env = Map.empty | |
| let env = env.Add("1", new TypeScheme([], Tycon("Int",[]))) | |
| let env = env.Add("a", new TypeScheme([], Tycon("Boolean",[]))) | |
| let typ = Tyvar("a") | |
| let subst = typeInfer.tp(env, Let("a", Var("1"), Var("a")), typ, Subst.emptySubst) | |
| assert (subst.call(typ) = Tycon("Int",[])) | |
| let testTpLet4() = // [1:Int] |- let a = a in 1 : (TypeError!) | |
| let env : Env = Map.empty | |
| let env = env.Add("1", new TypeScheme([], Tycon("Int",[]))) | |
| let typ = Tyvar("a") | |
| let msg = shouldFail_TypeError <| fun () -> | |
| ignore <| typeInfer.tp(env, Let("a", Var("a"), Var("1")), typ, Subst.emptySubst) | |
| assert (msg = "undefined: a") | |
| let testTpLamLet1() = | |
| // [e1:Bool, 1:Int] |- (\ x -> let y=e1 in x) 1 : Int | |
| // | |
| // 「 \ x -> let y=e1 in x」のように、λ本体の中にlet式が出現す | |
| // るときに、let束縛される識別子yのために登録される型スキーマで | |
| // は、xに対応する型スキーマで使用されている型変数が全称限量対 | |
| // 象から除外される。 | |
| // | |
| let env : Env = Map.empty | |
| let env = env.Add("e1", new TypeScheme([], Tycon("Boolean",[]))) | |
| let env = env.Add("1", new TypeScheme([], Tycon("Int",[]))) | |
| let typ = Tyvar("a") | |
| let subst = typeInfer.tp(env, | |
| App( | |
| Lam("x", | |
| Let("y", Var("e1"), Var("x"))), | |
| Var("1") | |
| ), | |
| typ, Subst.emptySubst) | |
| assert (subst.call(typ) = Tycon("Int",[])) | |
| let 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. | |
| let env : Env = Map.empty | |
| let env = env.Add("s", new TypeScheme([], Tycon("String",[]))) | |
| let env = env.Add("7", new TypeScheme([], Tycon("Int",[]))) | |
| let typ = Tyvar("a") | |
| let subst = typeInfer.tp(env, | |
| App( | |
| Lam("x", | |
| App(Var("x"), Var("s"))), | |
| Lam("x", Var("7")) | |
| ), | |
| typ, Subst.emptySubst) | |
| assert (subst.call(typ) = Tycon("Int",[])) | |
| let 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. | |
| let env : Env = Map.empty | |
| let env = env.Add("add", new TypeScheme([], Arrow(Tycon("Int",[]), Arrow(Tycon("Int",[]),Tycon("Int",[]))))) | |
| let env = env.Add("c", new TypeScheme([], Tycon("Char",[]))) | |
| let env = env.Add("s", new TypeScheme([], Tycon("String",[]))) | |
| let env = env.Add("7", new TypeScheme([], Tycon("Int",[]))) | |
| let typ = Tyvar("a") | |
| let msg = shouldFail_TypeError (fun () -> | |
| ignore <| typeInfer.tp(env, | |
| App( | |
| Lam("x", | |
| App( | |
| App(Var("add"), | |
| App(Var("x"), Var("s"))), | |
| App(Var("x"), Var("c"))) | |
| ), | |
| Lam("x", Var("7")) | |
| ), | |
| typ, Subst.emptySubst) | |
| ) | |
| assert (msg = "cannot unify Char[] with String[]") | |
| let 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. | |
| let env : Env = Map.empty | |
| let env = env.Add("add", new TypeScheme([], Arrow(Tycon("Int",[]), Arrow(Tycon("Int",[]),Tycon("Int",[]))))) | |
| let env = env.Add("c", new TypeScheme([], Tycon("Char",[]))) | |
| let env = env.Add("s", new TypeScheme([], Tycon("String",[]))) | |
| let env = env.Add("7", new TypeScheme([], Tycon("Int",[]))) | |
| let typ = Tyvar("a") | |
| let subst = typeInfer.tp(env, | |
| Let("x", | |
| Lam("x", Var("7")), | |
| App( | |
| App(Var("add"), | |
| App(Var("x"), Var("s"))), | |
| App(Var("x"), Var("c"))) | |
| ), | |
| typ, Subst.emptySubst) | |
| assert (subst.call(typ) = Tycon("Int",[])) | |
| let testTpLetRec1() = // [1:Int] |- letrec a = 1 in a : Int | |
| let env : Env = Map.empty | |
| let env = env.Add("1", new TypeScheme([], Tycon("Int",[]))) | |
| let typ = Tyvar("a") | |
| let subst = typeInfer.tp(env, LetRec("a", Var("1"), Var("a")), typ, Subst.emptySubst) | |
| assert (subst.call(typ) = Tycon("Int",[])) | |
| let testTpLetRec2() = // [true:Bool, 1:Int] |- letrec a = 1 in true : Bool | |
| let env : Env = Map.empty | |
| let env = env.Add("true", new TypeScheme([], Tycon("Boolean",[]))) | |
| let env = env.Add("1", new TypeScheme([], Tycon("Int",[]))) | |
| let typ = Tyvar("a") | |
| let subst = typeInfer.tp(env, LetRec("a", Var("1"), Var("true")), typ, Subst.emptySubst) | |
| assert (subst.call(typ) = Tycon("Boolean",[])) | |
| let testTpLetRec3() = // [1:Int, a:Bool] |- letrec a = 1 in a : Int | |
| let env : Env = Map.empty | |
| let env = env.Add("1", new TypeScheme([], Tycon("Int",[]))) | |
| let env = env.Add("a", new TypeScheme([], Tycon("Boolean",[]))) | |
| let typ = Tyvar("a") | |
| let subst = typeInfer.tp(env, LetRec("a", Var("1"), Var("a")), typ, Subst.emptySubst) | |
| assert (subst.call(typ) = Tycon("Int",[])) | |
| let 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. | |
| let env : Env = Map.empty | |
| let env = env.Add("add", new TypeScheme([], Arrow(Tycon("Int",[]), Arrow(Tycon("Int",[]),Tycon("Int",[]))))) | |
| let env = env.Add("c", new TypeScheme([], Tycon("Char",[]))) | |
| let env = env.Add("s", new TypeScheme([], Tycon("String",[]))) | |
| let env = env.Add("7", new TypeScheme([], Tycon("Int",[]))) | |
| let typ = Tyvar("a") | |
| let subst = typeInfer.tp(env, | |
| LetRec("x", | |
| Lam("x", Var("7")), | |
| App( | |
| App(Var("add"), | |
| App(Var("x"), Var("s"))), | |
| App(Var("x"), Var("c"))) | |
| ), | |
| typ, Subst.emptySubst) | |
| assert (subst.call(typ) = Tycon("Int",[])) | |
| let testTpLetRec4() = // [1:Int] |- letrec a = a in 1 : Int | |
| let env : Env = Map.empty | |
| let env = env.Add("1", new TypeScheme([], Tycon("Int",[]))) | |
| let typ = Tyvar("a") | |
| let subst = typeInfer.tp(env, LetRec("a", Var("a"), Var("1")), typ, Subst.emptySubst) | |
| assert (subst.call(typ) = Tycon("Int",[])) | |
| let testTypeOf() = // [] |- (\a->a) : a->a | |
| let env : Env = Map.empty | |
| let typ = typeInfer.typeOf(env, Lam("a", Var("a"))) // a->a | |
| assert (typ |> function Arrow _ -> true | _ -> false) | |
| assert (typ |> function Arrow(t1, t2) -> t1 = t2 | _ -> false) | |
| let testPredefinedEnv() = | |
| let env = typeInfer.predefinedEnv() | |
| assert (typeInfer.typeOf(env, Var("true")) = Tycon("Boolean",[])) | |
| let 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[]") | |
| let intList = App(App(Var("cons"), | |
| Var("zero")), | |
| Var("nil")) | |
| let zero = Var("zero") | |
| let 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[]") | |
| let 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[]") | |
| let run () = | |
| let a = [3; 1; 4; 1; 5] -- [2; 4] | |
| assert (a = [3; 1; 1; 5]) | |
| [testTerms; | |
| testTermsEquals; | |
| testTermsNotEquals; | |
| testTypes1; | |
| testSubstLookup1; | |
| testSubstLookup2; | |
| testSubstCallTyvar1; | |
| testSubstCallTyvar2; | |
| testSubstCallTyvar3; | |
| testSubstCallTyvar4; | |
| testSubstCallArrow1; | |
| testSubstCallArrow2; | |
| testSubstCallTycon1; | |
| testSubstCallTycon2; | |
| testSubstCallTycon3; | |
| testSubstCallEnv1; | |
| testTypeSchemeNewInstance1; | |
| testTypeSchemeNewInstance2; | |
| testEnvLookup1; | |
| testGenType1; | |
| testGenType2; | |
| testNewTyvar1; | |
| testTyvarsType1; | |
| testTyvarsTypeScheume1; | |
| testTyvarsEnv1; | |
| testMguTyvar1; | |
| testMguTyvar2; | |
| testMguArrow1; | |
| testMguArrow2; | |
| testMguArrowP1; | |
| testMguArrowP2; | |
| testMguArrowP3; | |
| testMguTycon1; | |
| testMguTycon2; | |
| testMguTycon3; | |
| testMguTycon4; | |
| testMguTyconP1; | |
| testMguTyconP2; | |
| testMguTyconP3; | |
| testMguTyconP4; | |
| testMguTyvarArrow1; | |
| testMguTyvarArrow2; | |
| testMguTyvarTycon1; | |
| testMguTyvarTycon2; | |
| testMguTyconArrow1; | |
| testTpVar1; | |
| testTpVar2; | |
| testTpLam1; | |
| testTpLam2; | |
| testTpLam3; | |
| testTpLam4; | |
| testTpLet1; | |
| testTpLet2; | |
| testTpLet3; | |
| testTpLet4; | |
| testTpLamLet1; | |
| testTpLamP1; | |
| testTpLamP2; | |
| testTpLetP1; | |
| testTpLetRec1; | |
| testTpLetRec2; | |
| testTpLetRec3; | |
| testTpLetRecP1; | |
| testTpLetRec4; | |
| testTypeOf; | |
| testPredefinedEnv; | |
| testShowType; | |
| ] | |
| |> List.iter (fun test -> test()) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment