Haskell类型推导

a = a + 1

在命令式编程的时代，区分一个人是否能学会编程的关键是看他能否理解a=a+1这个违反自然规律的表达式，在函数式编程里，这个金丝雀测试变成了能否推导出下面这个函数的类型。

f = const id
--const及id是prelude库的库函数
--const的作用是对于给定的两个参数，返回第一个参数，const的类型信息如下
const :: a->b->a
--id的作用是，输入任意值，返回这个给定的值，id的类型信息如下
id :: a->a

预备知识

柯里化

对于一个有n个参数的函数，给定第一个参数，将返回一个结果是n-1个参数的函数。那些没有给出所有参数的函数应用被称为函数的不完全应用（partitial application，有时候译为偏函数调用）。而所生成的函数，就是柯里化函数。

Haskell中函数的结合顺序是左结合

f = const id

类型推导

const的类型是a->b->a，是一个有两个参数的函数，const id是对const的不完全应用，按照柯里化的定义，它会返回一个一元函数，函数的返回值类型就是函数id的类型，a->a。由此推导出f的类型: b->(a->a)。

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

b->a->a与b->(a->a)是同一类型

我们对b->a->a进行柯里化，只应用第一个参数b，则返回一个参数为a，返回值为a的函数，也就是(a->a)。因此，b->a->a与b->(a->a)是同一类型。也就是说最右边的最外层括号是可以去掉的。

f :: b->a->a

lambda演算

const id a b
运用const id a，返回函数id
运用id b，返回b
由此也可以推导出const id的类型为：b->a->a

baby step

f = const const

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

函数是左结合的，函数f是对第一个const进行柯里化，返回一个b->a的函数。而这里的a是const，它的类型是a->b->a。因此，f的类型为：

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

问题来了

f = const const

const的类型是a->b->a，对左边的const做柯里化，变成了一个参数类型被b，返回值类型为a的函数，其中a被指定为const，类型为a->b->a。
那么问题来了，为什么f的类型不是b->a->b->a呢？
原因在于a和b都是类型变量，每一次对const的应用，a和b可能代表不同的类型。也就是说左边const函数的参数b的类型与右边const的b的类型不一定相同，区别起见，分别用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对三元函数x0做了两个参数的部分应用，返回的是一个参数类型为(t1 -> t2 -> t)，返回值为t的函数。x1的参数是y，用同一个参数作为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的参数是y，由于$的作用，首先对计算右边的x1 y，即用y对x1做局部应用。记y的类型为t2，x1 y返回的柯里化函数类型是：(t2->t2->t)->t，为后文描述方便，记为函数f。
接下来对左边的x1做柯里化，x1的第一个参数的类型就是函数f的类型。注意x2对x1做了两次应用，两次应用中t的类型有可能是不一样的，为了避免混淆，做alpha替换记f的类型为：(t2->t2->t1)->t1。
用f作为t1对x1做柯里化，返回一个入参是类型是(t2->t2->t1)->t1)->((t2->t2->t1)->t1)->t，返回值类型为t的函数。
因此，x2的类型为：

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