摘要：提供了類型推導(dǎo)來解決這個(gè)問題。函數(shù)式語言里比較經(jīng)典的類型推導(dǎo)的方法是，并且它是在里首先使用的。的類型推導(dǎo)有一點(diǎn)點(diǎn)不同，不過思想上是一致的推導(dǎo)所有的約束條件，然后統(tǒng)一到一個(gè)類型上。而推導(dǎo)器是所有類型推導(dǎo)器的基礎(chǔ)。

之劍

2016.5.1 00:38:12

根據(jù)Picrce的說法：“類型系統(tǒng)是一個(gè)可以根據(jù)代碼段計(jì)算出來的值對(duì)它們進(jìn)行分類，然后通過語法的手段來自動(dòng)檢測程序錯(cuò)誤的系統(tǒng)?！?/p>

類型可以讓你表示函數(shù)的域和值域。例如，在數(shù)學(xué)里，我們經(jīng)常看到下面的函數(shù)：

f: R -> N

這個(gè)定義告訴我們函數(shù)”f”的作用是把實(shí)數(shù)集里的數(shù)映射到自然集里。

抽象地說，這才是具體意義上的類型。類型系統(tǒng)給了我們一些表示這些集合的更強(qiáng)大的方式。

有了這些類型標(biāo)識(shí)，編譯器現(xiàn)在可以 靜態(tài)地(在編譯期)判斷這個(gè)程序是正確的。

換句話說，如果一個(gè)值（在運(yùn)行期）不能夠滿足程序里的限制條件的話，那么在編譯期就會(huì)出錯(cuò)。

通常來說，類型檢測器(typechecker)只能夠保證不正確的的程序不能通過編譯。但是，它不能夠保證所有正確的程序都能通過編譯。

由于類型系統(tǒng)的表達(dá)能力不斷增加，使得我們能夠生成出更加可靠的代碼，因?yàn)樗沟梦覀兡軌蚩刂瞥绦蛏系牟豢勺?，即是是程序還沒有運(yùn)行的情況下（在類型上限制bug的出現(xiàn)）。學(xué)術(shù)界一直在努力突破類型系統(tǒng)的表達(dá)能力的極限，包含值相關(guān)的類型。

注意，所有的類型信息都會(huì)在編譯期擦除。后面不再需要。這個(gè)被稱為類型擦除。比如,Java里面的泛型的實(shí)現(xiàn).

Scala強(qiáng)大的類型系統(tǒng)讓我們可以使用更具有表現(xiàn)力的表達(dá)式。一些主要的特點(diǎn)如下：

支持參數(shù)多態(tài)，泛型編程

支持（局部）類型推導(dǎo)，這就是你為什么不需要寫val i: Int = 12: Int

支持存在向量(existential quantification)，給一些沒有名稱的類型定義一些操作

支持視圖。 給定的值從一個(gè)類型到其他類型的“可轉(zhuǎn)換性”

多態(tài)可以用來編寫泛型代碼（用于處理不同類型的值)，并且不會(huì)減少靜態(tài)類型的表達(dá)能力。

例如，沒有參數(shù)多態(tài)的話，一個(gè)泛型的列表數(shù)據(jù)結(jié)構(gòu)通常會(huì)是下面這樣的寫法（在Java還沒有泛型的時(shí)候，確實(shí)是這樣的）：

scala> 2 :: 1 :: "bar" :: "foo" :: Nil

res5: List[Any] = List(2, 1, bar, foo)

這樣的話，我們就不能夠恢復(fù)每個(gè)元素的類型信息。

scala> res5.head

res6: Any = 2

這樣一來，我們的應(yīng)用里會(huì)包含一系列的類型轉(zhuǎn)換(“asInstanceOf[]“)，代碼會(huì)缺少類型安全（因?yàn)樗麄兌际莿?dòng)態(tài)類型的）。

多態(tài)是通過指定類型變量來達(dá)到的。

scala> def drop1[A](l: List[A]) = l.tail

drop1: [A](l: List[A])List[A]

 

scala> drop1(List(1,2,3))

res1: List[Int] = List(2, 3)

簡單來說，這意味著有一些你想在Scala里表達(dá)的類型概念會(huì)顯得“太過于泛型”，從而導(dǎo)致編譯器無法理解。所有的類型變量在運(yùn)行期必須是確定的。

對(duì)于靜態(tài)類型的一個(gè)比較常見的缺陷就是有太多的類型語法。Scala提供了類型推導(dǎo)來解決這個(gè)問題。

函數(shù)式語言里比較經(jīng)典的類型推導(dǎo)的方法是 Hindlry-Milner，并且它是在ML里首先使用的。

Scala的類型推導(dǎo)有一點(diǎn)點(diǎn)不同，不過思想上是一致的：推導(dǎo)所有的約束條件，然后統(tǒng)一到一個(gè)類型上。

在Scala里，例如，你不能這樣寫：

scala> { x => x }

:7: error: missing parameter type

       { x => x }

但是在OCaml里，你可以:

# fun x -> x;;

- : "a -> "a =

在Scala里，所有的類型推導(dǎo)都是局部的。Scala一次只考慮一個(gè)表達(dá)式。例如：

scala> def id[T](x: T) = x

id: [T](x: T)T

 

scala> val x = id(322)

x: Int = 322

 

scala> val x = id("hey")

x: java.lang.String = hey

 

scala> val x = id(Array(1,2,3,4))

x: Array[Int] = Array(1, 2, 3, 4)

在這里，類型都被隱藏了。Scala編譯器自動(dòng)推導(dǎo)參數(shù)的類型。注意我們也沒有必要顯示指定返回值的類型了。

Scala的類型系統(tǒng)需要把類的繼承關(guān)系和多態(tài)結(jié)合起來。類的繼承使得類之間存在父子的關(guān)系。當(dāng)把面向?qū)ο蠛投鄳B(tài)結(jié)合在一起時(shí)，一個(gè)核心的問題就出來了：如果T"是T的子類，那么Container[T"]是不是Container[T]的子類呢？Variance注釋允許你在類繼承和多態(tài)類型之間表達(dá)下面的這些關(guān)系：

子類關(guān)系的真正意思是：對(duì)于一個(gè)給定的類型T，如果T’是它的子類，那么T’可以代替T嗎？

scala> class Contravariant[-A]

defined class Contravariant

 

scala> val cv: Contravariant[String] = new Contravariant[AnyRef]

cv: Contravariant[AnyRef] = Contravariant@49fa7ba

 

scala> val fail: Contravariant[AnyRef] = new Contravariant[String]

:6: error: type mismatch;

 found   : Contravariant[String]

 required: Contravariant[AnyRef]

       val fail: Contravariant[AnyRef] = new Contravariant[String]     

有時(shí)候你不需要給一個(gè)類型變量以名稱，例如

scala> def count[A](l: List[A]) = l.size

count: [A](List[A])Int

你可以用“通配符”來替代：

scala> def count(l: List[_]) = l.size

count: (List[_])Int

先看個(gè)代碼：

Map> m = new HashMap>(); 

是啊, 這簡直太長了,我們不禁感嘆,這編譯器也太愚蠢了.幾乎一半字符都是重復(fù)的!

針對(duì)泛型定義和實(shí)例太過繁瑣的問題,在java 7 中引入了鉆石運(yùn)算符. 神奇的Coin項(xiàng)目,滿足了你的心愿.

于是,你在java 7之后可以這樣寫了:

Map> m = new HashMap(); 

鉆石運(yùn)算符通常用于簡化創(chuàng)建帶有泛型對(duì)象的代碼，可以避免運(yùn)行時(shí) 的異常，并且它不再要求程序員在編碼時(shí)顯示書寫冗余的類型參數(shù)。實(shí)際上，編譯器在進(jìn)行詞法解析時(shí)會(huì)自動(dòng)推導(dǎo)類型，自動(dòng)為代碼進(jìn)行補(bǔ)全，并且編譯的字節(jié)碼與 以前無異。

當(dāng)時(shí)在提案中,這個(gè)問題叫"Improved Type Inference for Generic Instance Creation",縮寫ITIGIX聽起來怪怪的,但是為啥叫鉆石算法? 世界上, 哪有那么多為什么.

Scala正是因?yàn)樽隽祟愋屯茖?dǎo), 讓Coders感覺仿佛在寫動(dòng)態(tài)語言的代碼.

在Scala中,高階函數(shù)經(jīng)常傳遞匿名函數(shù).舉個(gè)栗子:

一段定義泛型函數(shù)的代碼

def dropWhile[A](list: List[A], f: A => Boolean): List[A]

當(dāng)我們傳入一個(gè)匿名函數(shù)f來調(diào)用它,

val mylist: List[Int] = List(1,2,3,4,5) 

val listDropped = dropWhile( mylist, (x: Int) => x < 4 )

listDropped的值是List(4,5)

我們用大腦可以輕易判斷, 當(dāng)list: List[A] 中的類型A在mylist聲明的時(shí)候已經(jīng)指定了Int, 那么很明顯, 在第二個(gè)參數(shù)中,我們的x也必是Int.

很幸運(yùn)Scala設(shè)計(jì)者們早已考慮到這一點(diǎn),Scala編譯器可以推導(dǎo)這種情況.但是你得按照Scala的規(guī)范限制來寫你的dropWhile函數(shù)的簽名(柯里化的): dropWhile( mylist )( f )

def dropWhile[A] ( list: List[A] ) ( f: A => Boolean ) : List[A] = list match {

case Cons(h,t) if f(h) => dropWhile(t)(f)

case _ => list

}

如此而來,我們就可以直接像下面這樣使用這個(gè)函數(shù)了:

val mylist: List[Int] = List(1,2,3,4,5)

val droppedList = dropWhile( mylist ) ( x => x < 4 )

注意, x參數(shù)沒有指定Int類型, 因?yàn)榫幾g器直接通過mylist的泛型信息Int推導(dǎo)出x的類型也是Int.

類型推導(dǎo)是一門博大的學(xué)問，背后有繁冗的理論, 這在編譯器設(shè)計(jì)開發(fā)的時(shí)候需要解決的問題.

在《Programming in Scala》一書中提到基于流的類型推斷有它的局限性，但是對(duì)于面向?qū)ο蟮姆种ь愋吞幚肀菻indley-Mlner更加優(yōu)雅。

基于流的類型推導(dǎo)在偏應(yīng)用函數(shù)場景下，不能對(duì)參數(shù)類型省略

類型推導(dǎo)（Type Inference）是現(xiàn)代高級(jí)語言中一個(gè)越來越常見的特性。其實(shí)，這個(gè)特性在函數(shù)式語言

中早有了廣泛應(yīng)用。而HindleyMilner推導(dǎo)器是所有類型推導(dǎo)器的基礎(chǔ)。

Scala實(shí)現(xiàn)的一個(gè)簡單的HindleyMilner推導(dǎo)器:

    /*

     * http://dysphoria.net/code/hindley-milner/HindleyMilner.scala

     * Andrew Forrest

     *

     * Implementation of basic polymorphic type-checking for a simple language.

     * Based heavily on Nikita Borisov’s Perl implementation at

     * http://web.archive.org/web/20050420002559/www.cs.berkeley.edu/~nikitab/courses/cs263/hm.html

     * which in turn is based on the paper by Luca Cardelli at

     * http://lucacardelli.name/Papers/BasicTypechecking.pdf

     *

     * If you run it with "scala HindleyMilner.scala" it will attempt to report the types

     * for a few example expressions. (It uses UTF-8 for output, so you may need to set your

     * terminal accordingly.)

     *

     * Changes

     * June 30, 2011 by Liang Kun(liangkun(AT)baidu.com)

     * 1. Modify to enhance readability

     * 2. Extend to Support if expression in syntax

     *

     *

     *

     * Do with it what you will. :)

     */



    /** Syntax definition. This is a simple lambda calculous syntax.

     * Expression ::= Identifier

     * | Constant

     * | "if" Expression "then" Expression "else" Expression

     * | "lambda(" Identifier ") " Expression

     * | Expression "(" Expression ")"

     * | "let" Identifier "=" Expression "in" Expression

     * | "letrec" Identifier "=" Expression "in" Expression

     * | "(" Expression ")"

     * See the examples below in main function.

     */

    sealed abstract class Expression



    case class Identifier(name: String) extends Expression {

        override def toString = name

    }



    case class Constant(value: String) extends Expression {

        override def toString = value

    }



    case class If(condition: Expression, then: Expression, other: Expression) extends Expression {

        override def toString = "(if " + condition + " then " + then + " else " + other + ")"

    }



    case class Lambda(argument: Identifier, body: Expression) extends Expression {

        override def toString = "(lambda " + argument + " → " + body + ")"

    }



    case class Apply(function: Expression, argument: Expression) extends Expression {

        override def toString = "(" + function + " " + argument + ")"

    }



    case class Let(binding: Identifier, definition: Expression, body: Expression) extends Expression {

        override def toString = "(let " + binding + " = " + definition + " in " + body + ")"

    }



    case class Letrec(binding: Identifier, definition: Expression, body: Expression) extends Expression {

        override def toString = "(letrec " + binding + " = " + definition + " in " + body + ")"

    }





    /** Exceptions may happened */

    class TypeError(msg: String) extends Exception(msg)

    class ParseError(msg: String) extends Exception(msg)





    /** Type inference system */

    object TypeSystem {

        type Env = Map[Identifier, Type]

        val EmptyEnv: Map[Identifier, Type] = Map.empty



        // type variable and type operator

        sealed abstract class Type

        case class Variable(id: Int) extends Type {

            var instance: Option[Type] = None

            lazy val name = nextUniqueName()



            override def toString = instance match {

                case Some(t) => t.toString

                case None => name

            }

        }



        case class Operator(name: String, args: Seq[Type]) extends Type {

            override def toString = {

                if (args.length == 0)

                    name

                else if (args.length == 2)

                    "[" + args(0) + " " + name + " " + args(1) + "]"

                else

                    args.mkString(name + "[", ", ", "]")

            }

        }



        // builtin types, types can be extended by environment

        def Function(from: Type, to: Type) = Operator("→", Array(from, to))

        val Integer = Operator("Integer", Array[Type]())

        val Boolean = Operator("Boolean", Array[Type]())





        protected var _nextVariableName = "α";

        protected def nextUniqueName() = {

            val result = _nextVariableName

            _nextVariableName = (_nextVariableName.toInt + 1).toChar

            result.toString

        }

        protected var _nextVariableId = 0

        def newVariable(): Variable = {

            val result = _nextVariableId

            _nextVariableId += 1

            Variable(result)

        }





        // main entry point

        def analyze(expr: Expression, env: Env): Type = analyze(expr, env, Set.empty)

        def analyze(expr: Expression, env: Env, nongeneric: Set[Variable]): Type = expr match {

            case i: Identifier => getIdentifierType(i, env, nongeneric)



            case Constant(value) => getConstantType(value)



            case If(cond, then, other) => {

                val condType = analyze(cond, env, nongeneric)

                val thenType = analyze(then, env, nongeneric)

                val otherType = analyze(other, env, nongeneric)

                unify(condType, Boolean)

                unify(thenType, otherType)

                thenType

            }



            case Apply(func, arg) => {

                val funcType = analyze(func, env, nongeneric)

                val argType = analyze(arg, env, nongeneric)

                val resultType = newVariable()

                unify(Function(argType, resultType), funcType)

                resultType

            }



            case Lambda(arg, body) => {

                val argType = newVariable()

                val resultType = analyze(body,

                                         env + (arg -> argType),

                                         nongeneric + argType)

                Function(argType, resultType)

            }



            case Let(binding, definition, body) => {

                val definitionType = analyze(definition, env, nongeneric)

                val newEnv = env + (binding -> definitionType)

                analyze(body, newEnv, nongeneric)

            }



            case Letrec(binding, definition, body) => {

                val newType = newVariable()

                val newEnv = env + (binding -> newType)

                val definitionType = analyze(definition, newEnv, nongeneric + newType)

                unify(newType, definitionType)

                analyze(body, newEnv, nongeneric)

            }

        }



        protected def getIdentifierType(id: Identifier, env: Env, nongeneric: Set[Variable]): Type = {

            if (env.contains(id))

                fresh(env(id), nongeneric)

            else

                throw new ParseError("Undefined symbol: " + id)

        }



        protected def getConstantType(value: String): Type = {

            if(isIntegerLiteral(value))

                Integer

            else

                throw new ParseError("Undefined symbol: " + value)

        }



        protected def fresh(t: Type, nongeneric: Set[Variable]) = {

            import scala.collection.mutable

            val mappings = new mutable.HashMap[Variable, Variable]

            def freshrec(tp: Type): Type = {

                prune(tp) match {

                    case v: Variable =>

                        if (isgeneric(v, nongeneric))

                            mappings.getOrElseUpdate(v, newVariable())

                        else

                            v



                    case Operator(name, args) =>

                        Operator(name, args.map(freshrec(_)))

                }

            }



            freshrec(t)

        }



        protected def unify(t1: Type, t2: Type) {

            val type1 = prune(t1)

            val type2 = prune(t2)

            (type1, type2) match {

                case (a: Variable, b) => if (a != b) {

                    if (occursintype(a, b))

                        throw new TypeError("Recursive unification")

                    a.instance = Some(b)

                }

                case (a: Operator, b: Variable) => unify(b, a)

                case (a: Operator, b: Operator) => {

                    if (a.name != b.name ||

                        a.args.length != b.args.length) throw new TypeError("Type mismatch: " + a + " ≠ " + b)

                    

                    for(i <- 0 until a.args.length)

                        unify(a.args(i), b.args(i))

                }

            }

        }



        // Returns the currently defining instance of t.

        // As a side effect, collapses the list of type instances.

        protected def prune(t: Type): Type = t match {

            case v: Variable if v.instance.isDefined => {

                val inst = prune(v.instance.get)

                v.instance = Some(inst)

                inst

            }

            case _ => t

        }



        // Note: must be called with v "pre-pruned"

        protected def isgeneric(v: Variable, nongeneric: Set[Variable]) = !(occursin(v, nongeneric))



        // Note: must be called with v "pre-pruned"

        protected def occursintype(v: Variable, type2: Type): Boolean = {

            prune(type2) match {

                case `v` => true

                case Operator(name, args) => occursin(v, args)

                case _ => false

            }

        }



        protected def occursin(t: Variable, list: Iterable[Type]) =

            list exists (t2 => occursintype(t, t2))



        protected val checkDigits = "^(d+)$".r

        protected def isIntegerLiteral(name: String) = checkDigits.findFirstIn(name).isDefined

    }





    /** Demo program */

    object HindleyMilner {

        def main(args: Array[String]){

            Console.setOut(new java.io.PrintStream(Console.out, true, "utf-8"))



            // extends the system with a new type[pair] and some builtin functions

            val left = TypeSystem.newVariable()

            val right = TypeSystem.newVariable()

            val pairType = TypeSystem.Operator("×", Array(left, right))



            val myenv: TypeSystem.Env = TypeSystem.EmptyEnv ++ Array(

                Identifier("pair") -> TypeSystem.Function(left, TypeSystem.Function(right, pairType)),

                Identifier("true") -> TypeSystem.Boolean,

                Identifier("false")-> TypeSystem.Boolean,

                Identifier("zero") -> TypeSystem.Function(TypeSystem.Integer, TypeSystem.Boolean),

                Identifier("pred") -> TypeSystem.Function(TypeSystem.Integer, TypeSystem.Integer),

                Identifier("times")-> TypeSystem.Function(TypeSystem.Integer,

                        TypeSystem.Function(TypeSystem.Integer, TypeSystem.Integer))

            )



            // example expressions

            val pair = Apply(

                Apply(

                    Identifier("pair"), Apply(Identifier("f"), Constant("4"))

                ),

                Apply(Identifier("f"), Identifier("true"))

            )

            val examples = Array[Expression](

                // factorial

                Letrec(Identifier("factorial"), // letrec factorial =

                    Lambda(Identifier("n"), // lambda n =>

                        If(

                            Apply(Identifier("zero"), Identifier("n")),



                            Constant("1"),



                            Apply(

                                Apply(Identifier("times"), Identifier("n")),

                                Apply(

                                    Identifier("factorial"),

                                    Apply(Identifier("pred"), Identifier("n"))

                                )

                            )

                        )

                    ), // in

                    Apply(Identifier("factorial"), Constant("5"))

                ),



                // Should fail:

                // fn x => (pair(x(3) (x(true))))

                Lambda(Identifier("x"),

                    Apply(

                        Apply(Identifier("pair"),

                            Apply(Identifier("x"), Constant("3"))

                        ),

                        Apply(Identifier("x"), Identifier("true"))

                    )

                ),



                // pair(f(3), f(true))

                Apply(

                    Apply(Identifier("pair"), Apply(Identifier("f"), Constant("4"))),

                    Apply(Identifier("f"), Identifier("true"))

                ),





                // letrec f = (fn x => x) in ((pair (f 4)) (f true))

                Let(Identifier("f"), Lambda(Identifier("x"), Identifier("x")), pair),



                // Should fail:

                // fn f => f f

                Lambda(Identifier("f"), Apply(Identifier("f"), Identifier("f"))),



                // let g = fn f => 5 in g g

                Let(

                    Identifier("g"),

                    Lambda(Identifier("f"), Constant("5")),

                    Apply(Identifier("g"), Identifier("g"))

                ),



                // example that demonstrates generic and non-generic variables:

                // fn g => let f = fn x => g in pair (f 3, f true)

                Lambda(Identifier("g"),

                    Let(Identifier("f"),

                        Lambda(Identifier("x"), Identifier("g")),

                        Apply(

                            Apply(Identifier("pair"),

                                  Apply(Identifier("f"), Constant("3"))

                            ),

                            Apply(Identifier("f"), Identifier("true"))

                        )

                    )

                ),



                // Function composition

                // fn f (fn g (fn arg (f g arg)))

                Lambda( Identifier("f"),

                    Lambda( Identifier("g"),

                        Lambda( Identifier("arg"),

                            Apply(Identifier("g"), Apply(Identifier("f"), Identifier("arg")))

                        )

                    )

                )

            )



            for(eg <- examples){

                tryexp(myenv, eg)

            }

        }



        def tryexp(env: TypeSystem.Env, expr: Expression) {

            try {

                val t = TypeSystem.analyze(expr, env)

                print(t)



            }catch{

                case t: ParseError => print(t.getMessage)

                case t: TypeError => print(t.getMessage)

            }

            println(":	" + expr)

        }

    }



    HindleyMilner.main(argv)

Haskell寫的一個(gè) 合一算法的簡單實(shí)現(xiàn):

https://github.com/yihuang/haskell-snippets/blob/master/Unif.hs

module Main where    



import Data.List (intersperse)    

import Control.Monad    



-- utils --    



mapFst :: (a -> b) -> (a, c) -> (b,   c)    

mapFst    f           (a, c) =  (f a, c)    



-- types --    



type Name = String    



data Term = Var Name    

         | App Name [Term]    



-- 表示一個(gè)替換關(guān)系    

type Sub = (Term, Name)    



-- implementation --    



-- 檢查變量 Name 是否出現(xiàn)在 Term 中    

occurs :: Name -> Term -> Bool    

occurs x t = case t of    

 (Var y)    -> x==y    

 (App _ ts) -> and . map (occurs x) $ ts    



-- 使用 Sub 對(duì) Term 進(jìn)行替換    

sub :: Sub -> Term -> Term    

sub (t1, y) t@(Var a)    

 | a==y      = t1    

 | otherwise = t    

sub s (App f ts) = App f $ map (sub s) ts    



-- 使用 Sub 列表對(duì) Term 進(jìn)行替換    

subs :: [Sub] -> Term -> Term    

subs ss t = foldl (flip sub) t ss    



-- 把兩個(gè)替換列表組合起來，同時(shí)用新加入的替換對(duì)其中所有 Term 進(jìn)行替換    

compose :: [Sub] -> [Sub] -> [Sub]    

compose []     s1 = s1    

compose (s:ss) s1 = compose ss $ s : iter s s1    

 where    

   iter :: Sub -> [Sub] -> [Sub]    

   iter s ss = map (mapFst (sub s)) ss    



-- 合一函數(shù)    

unify :: Term -> Term -> Maybe [Sub]    

unify t1 t2 = case (t1, t2) of    

 (Var x,   Var y)   -> if x==y        then Just [] else Just [(t1, y)]    

 (Var x,   App _ _) -> if occurs x t2 then Nothing else Just [(t2, x)]    

 (App _ _, Var x)   -> if occurs x t1 then Nothing else Just [(t1, x)]    

 (App n1 ts1, App n2 ts2)    

                    -> if n1/=n2      then Nothing else unify_args ts1 ts2    

 where    

   unify_args [] [] = Just []    

   unify_args _  [] = Nothing    

   unify_args [] _  = Nothing    

   unify_args (t1:ts1) (t2:ts2) = do    

     u <- unify t1 t2    

     let update = map (subs u)    

     u1 <- unify_args (update ts1) (update ts2)    

     return (u1 `compose` u)    



-- display --    



instance Show Term where    

   show (Var s) = s    

   show (App name ts) = name++"("++(concat . intersperse "," $ (map show ts))++")"    



showSub (t, s) = s ++ " -> " ++ show t    



-- test cases --    



a = Var "a"    

b = Var "b"    

c = Var "c"    

d = Var "d"    

x = Var "x"    

y = Var "y"    

z = Var "z"    

f = App "f"    

g = App "g"    

j = App "j"    



test t1 t2 = do    

   putStrLn $ show t1 ++ "  <==>  " ++ show t2    

   case unify t1 t2 of    

     Nothing -> putStrLn "unify fail"    

     Just u  -> putStrLn $ concat . intersperse "
" $ map showSub u    



testcases = [(j [x,y,z],    

             j [f [y,y], f [z,z], f [a,a]])    

           ,(x,    

             f [x])    

           ,(f [x],    

             y)    

           ,(f [a, f [b, c], g [b, a, c]],    

             f [a, a, x])    

           ,(f [d, d, x],    

             f [a, f [b, c], f [b, a, c]])    

           ]    



main = forM testcases (uncurry test)