Haskell類型推導

a = a + 1

在命令式編程的時代，區(qū)分一個人是否能學會編程的關鍵是看他能否理解a=a+1這個違反自然規(guī)律的表達式，在函數(shù)式編程里，這個金絲雀測試變成了能否推導出下面這個函數(shù)的類型。

f = const id
--const及id是prelude庫的庫函數(shù)
--const的作用是對于給定的兩個參數(shù)，返回第一個參數(shù)，const的類型信息如下
const :: a->b->a
--id的作用是，輸入任意值，返回這個給定的值，id的類型信息如下
id :: a->a

預備知識

柯里化

對于一個有n個參數(shù)的函數(shù)，給定第一個參數(shù)，將返回一個結果是n-1個參數(shù)的函數(shù)。那些沒有給出所有參數(shù)的函數(shù)應用被稱為函數(shù)的不完全應用（partitial application，有時候譯為偏函數(shù)調(diào)用）。而所生成的函數(shù)，就是柯里化函數(shù)。

Haskell中函數(shù)的結合順序是左結合

f = const id

類型推導

const的類型是a->b->a，是一個有兩個參數(shù)的函數(shù)，const id是對const的不完全應用，按照柯里化的定義，它會返回一個一元函數(shù)，函數(shù)的返回值類型就是函數(shù)id的類型，a->a。由此推導出f的類型: b->(a->a)。

f :: b->(a->a)

b->a->a與b->(a->a)是同一類型

我們對b->a->a進行柯里化，只應用第一個參數(shù)b，則返回一個參數(shù)為a，返回值為a的函數(shù)，也就是(a->a)。因此，b->a->a與b->(a->a)是同一類型。也就是說最右邊的最外層括號是可以去掉的。

f :: b->a->a

lambda演算

const id a b
運用const id a，返回函數(shù)id
運用id b，返回b
由此也可以推導出const id的類型為：b->a->a

baby step

f = const const

const :: a->b->a
f = const const

函數(shù)是左結合的，函數(shù)f是對第一個const進行柯里化，返回一個b->a的函數(shù)。而這里的a是const，它的類型是a->b->a。因此，f的類型為：

f::c->(a->b->a)
--等價方式
f::c->a->b->a

問題來了

f = const const

const的類型是a->b->a，對左邊的const做柯里化，變成了一個參數(shù)類型被b，返回值類型為a的函數(shù)，其中a被指定為const，類型為a->b->a。
那么問題來了，為什么f的類型不是b->a->b->a呢？
原因在于a和b都是類型變量，每一次對const的應用，a和b可能代表不同的類型。也就是說左邊const函數(shù)的參數(shù)b的類型與右邊const的b的類型不一定相同，區(qū)別起見，分別用b和b1代表這兩個類型。

one more step

x0 :: t1 -> t2 -> (t1 -> t2 -> t) -> t
x0 = \x y z -> z x y
x1 = \y-> x0 y y
x2 = \y-> x1 $ x1 y

x1的類型推導

x1 = \y-> x0 y y，x1對三元函數(shù)x0做了兩個參數(shù)的部分應用，返回的是一個參數(shù)類型為(t1 -> t2 -> t)，返回值為t的函數(shù)。x1的參數(shù)是y，用同一個參數(shù)作為t1和t2來部分應用x0，因此t1、t2必須有相同的類型，都是y的類型。把y的類型指定為t1，則x1的類型為：

x0 = \x y z -> z x y
x1 = \y -> x0 y y
x1 :: t1->(t1->t1->t)->t

x2的類型推導

x2 = \y -> x1 $ x1 y
x2的參數(shù)是y，由于$的作用，首先對計算右邊的x1 y，即用y對x1做局部應用。記y的類型為t2，x1 y返回的柯里化函數(shù)類型是：(t2->t2->t)->t，為后文描述方便，記為函數(shù)f。
接下來對左邊的x1做柯里化，x1的第一個參數(shù)的類型就是函數(shù)f的類型。注意x2對x1做了兩次應用，兩次應用中t的類型有可能是不一樣的，為了避免混淆，做alpha替換記f的類型為：(t2->t2->t1)->t1。
用f作為t1對x1做柯里化，返回一個入?yún)⑹穷愋褪?t2->t2->t1)->t1)->((t2->t2->t1)->t1)->t，返回值類型為t的函數(shù)。
因此，x2的類型為：

x2 ::
  t2
  -> (((t2 -> t2 -> t1) -> t1) -> ((t2 -> t2 -> t1) -> t1) 
   -> t) 
-> t