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

    已知函數(shù)如下：

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

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

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

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

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

    然后，empty返回list T。

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

    大框架出來(lái)了，只是還有三種表達(dá)式：lambda expression、let-in expression和select-case expression沒(méi)有解決。不過(guò)這個(gè)應(yīng)該不麻煩了，因?yàn)榉椒ǘ疾畈欢唷?br>
    P.S.
    為了解決這個(gè)問(wèn)題，我給類(lèi)型本身建模，給出了一個(gè)定義和若干操作組成一個(gè)代數(shù)系統(tǒng)。你可以——
        Apply：將模板參數(shù)替換成另一些類(lèi)型，得到新的新的類(lèi)型。
        Solve：對(duì)比兩個(gè)類(lèi)型，如果可以通過(guò)某些Apply從類(lèi)型1轉(zhuǎn)到類(lèi)型2，那么給出Apply所需要的參數(shù)。
        Equal：對(duì)比兩個(gè)類(lèi)型是否完全相等。
        Merge：對(duì)比兩個(gè)類(lèi)型，其中兩個(gè)類(lèi)型都有模板參數(shù)。如果可以通過(guò)Apply將類(lèi)型1和類(lèi)型2都轉(zhuǎn)換到類(lèi)型3，那么給出其中一個(gè)合適的類(lèi)型3。這個(gè)時(shí)候可以通過(guò)Solve去獲得轉(zhuǎn)換的方法。
    通過(guò)這四個(gè)操作互相組合，加上一些定制的策略，就可以解類(lèi)型方程組了，也就是這里所解決的問(wèn)題。