我終于在實驗階段解決了這個困擾了我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去獲得轉換的方法。
    通過這四個操作互相組合，加上一些定制的策略，就可以解類型方程組了，也就是這里所解決的問題。