我終于在實(shí)驗階段解決了這個困擾了我5個月（雖然實(shí)際上我花了3個星期）的問題。目標(biāo)是這樣的：你寫程序，可以盡可能的不寫一些類型信息，譬如函數(shù)參數(shù)和返回值的類型信息等。我的編譯器幫你把它的類型算出來。

    已知函數(shù)如下：

    這里有類型list T，empty返回list T（沒有上下文的時候T不知道），list 1(list 2 empty)返回數(shù)組[1,2]。isub減法，iequ判斷是否相等。于是我寫了一個函數(shù)makearray x返回[x , x-1 , x-2 , ... , 1]。也就是說，makearray 5返回[5,4,3,2,1]，代碼如下：
    函數(shù)的意思是，如果max==0則返回空數(shù)組，否則返回[max]加上makearray (max-1)。

    現(xiàn)在我并沒有為makearray定義任何類型，所以我的編譯器必須嘗試能否產(chǎn)生一個類型給他（有可能結(jié)果是模板函數(shù)）：

    方法如下（標(biāo)紅字的部分為實(shí)際編碼中遇到困難的部分）：
    首先，根據(jù)isub的類型int->int->int，可以判斷出isub max 1的結(jié)果是int，然后假設(shè)max是int。因為如果max不是int則肯定會發(fā)生語法錯誤。因為我的語言沒有任何隱式轉(zhuǎn)換。

    其次，makearray (isub max 1)的類型計算不出來，實(shí)際上還沒計算出來。標(biāo)記類型為"?"。

    然后，list max (makearray...)了。max為int，所以現(xiàn)在list所期望的類型是int->?->?。然后根據(jù)list的實(shí)際類型T->list T->list T，我們可以得出，這個表達(dá)式返回list int。

    然后，empty返回list T。

    最后，iequ max 0顯然返回bool。根據(jù)if的類型信息bool->T->T->T，傳入?yún)?shù)bool、list T2和list int，顯然可以得到if在這個上下文中，T=list int。因此得到的結(jié)果就是makearray max返回list int。加上max是int，所以makearray的類型就是int->list int了。

    大框架出來了，只是還有三種表達(dá)式：lambda expression、let-in expression和select-case expression沒有解決。不過這個應(yīng)該不麻煩了，因為方法都差不多。

    P.S.
    為了解決這個問題，我給類型本身建模，給出了一個定義和若干操作組成一個代數(shù)系統(tǒng)。你可以——
        Apply：將模板參數(shù)替換成另一些類型，得到新的新的類型。
        Solve：對比兩個類型，如果可以通過某些Apply從類型1轉(zhuǎn)到類型2，那么給出Apply所需要的參數(shù)。
        Equal：對比兩個類型是否完全相等。
        Merge：對比兩個類型，其中兩個類型都有模板參數(shù)。如果可以通過Apply將類型1和類型2都轉(zhuǎn)換到類型3，那么給出其中一個合適的類型3。這個時候可以通過Solve去獲得轉(zhuǎn)換的方法。
    通過這四個操作互相組合，加上一些定制的策略，就可以解類型方程組了，也就是這里所解決的問題。