我终于在实验阶段解决了这个困扰了我5个月（虽然实际上我花了3个星期）的问题。目标是这样的：你写程序，可以尽可能的不写一些类型信息，譬如函数参数和返回值的类型信息等。我的编译器帮你把它的类型算出来。

    已知函数如下：

    这里有类型list T，empty返回list T（没有上下文的时候T不知道），list 1(list 2 empty)返回数组[1,2]。isub减法，iequ判断是否相等。于是我写了一个函数makearray x返回[x , x-1 , x-2 , ... , 1]。也就是说，makearray 5返回[5,4,3,2,1]，代码如下：
    函数的意思是，如果max==0则返回空数组，否则返回[max]加上makearray (max-1)。

    现在我并没有为makearray定义任何类型，所以我的编译器必须尝试能否产生一个类型给他（有可能结果是模板函数）：

    方法如下（标红字的部分为实际编码中遇到困难的部分）：
    首先，根据isub的类型int->int->int，可以判断出isub max 1的结果是int，然后假设max是int。因为如果max不是int则肯定会发生语法错误。因为我的语言没有任何隐式转换。

    其次，makearray (isub max 1)的类型计算不出来，实际上还没计算出来。标记类型为"?"。

    然后，list max (makearray...)了。max为int，所以现在list所期望的类型是int->?->?。然后根据list的实际类型T->list T->list T，我们可以得出，这个表达式返回list int。

    然后，empty返回list T。

    最后，iequ max 0显然返回bool。根据if的类型信息bool->T->T->T，传入参数bool、list T2和list int，显然可以得到if在这个上下文中，T=list int。因此得到的结果就是makearray max返回list int。加上max是int，所以makearray的类型就是int->list int了。

    大框架出来了，只是还有三种表达式：lambda expression、let-in expression和select-case expression没有解决。不过这个应该不麻烦了，因为方法都差不多。

    P.S.
    为了解决这个问题，我给类型本身建模，给出了一个定义和若干操作组成一个代数系统。你可以——
        Apply：将模板参数替换成另一些类型，得到新的新的类型。
        Solve：对比两个类型，如果可以通过某些Apply从类型1转到类型2，那么给出Apply所需要的参数。
        Equal：对比两个类型是否完全相等。
        Merge：对比两个类型，其中两个类型都有模板参数。如果可以通过Apply将类型1和类型2都转换到类型3，那么给出其中一个合适的类型3。这个时候可以通过Solve去获得转换的方法。
    通过这四个操作互相组合，加上一些定制的策略，就可以解类型方程组了，也就是这里所解决的问题。