deniok

Общеизвестен способ выражения на чистой лямбде чисел Черча:

one   = \f x -> f x
two   = \f x -> f $ f x
three = \f x -> f $ f $ f x
four  = \f x -> f $ f $ f $ f x
...

Для всех из них (кроме, разумеется, one) тайпчекер выводит тип (a->a)->(a->a). Ясно как он это делает. Пусть x::a, тогда

f x         => f :: a  -> a1
f $ f x     => f :: a1 -> a2
f $ f $ f x => f :: a2 -> a3
...

где вывод о типе f берется из самого внешнего применения f и предыдущей строки; a1, a2, a3... вводятся как произвольные (пока) переменные типа. Сравнивая выведенные определения типов для f, получаем

a =a1 a1=a2
a1=a2 a2=a3
...

В результате имеем f :: a -> a, и, следовательно, лямбды типизируются так:

two   :: (a -> a) -> a -> a
three :: (a -> a) -> a -> a
four  :: (a -> a) -> a -> a
...

Эта типизация по Карри (выводимая, а не декларируемая) осуществляется "типовыводителем" по алгоритму Хиндли-Дамаса-Милнера. Но не является единственно возможной, даже в Хаскелле (не 98, конечно, а GHC-шном). Мы можем, включив поддержку полиморфных типов второго ранга (rank-2 types polymorphism) или более высокого (arbitrary-rank polymorphism), задать для нашей two другие типизации.

( Зачем оно нам? )