http://community.livejournal.com/ru_lambda/95113.html

А как можно определить операцию minus, для простой реализации лямбда исчисленя на хаскеле?
Проблема в том, что выражения вида pred (pred three) прекрасно работают, а вот для эквивалентного two pred three, автоматом тип уже не выводится.

---

Декремент определяется так

pred cn f x = fst (cn (\(i,j)->(j,f i)) xx) where
  xx = (x,x) -- тогда pred zero == zero
  -- либо
  xx = (error "ушли в минус",x) -- тогда pred zero = (_|_)

В исходном варианте он определяется на ленивой паре, if selector then first_part else second_part, ну это не очень принципиально.

Проблема не в ограниченности вывода типов.
Обычно нумерал имеет тип

type CN t = (t->t)->t->t

zero :: CN t -- хотя это просто канцелятор : (flip const) :: t1->t2->t2
one  :: CN t -- хотя это просто аппликатор : (.) :: (t1->t2)->t1->t2

А здесь мы видим, что

pred :: (CN (t,t)) -> (CN t)

На самом деле, конечно, :t pred покажет, что там задействована туча типов — но это лишь от лишней общности формулы, точно так же, как в случае с zero и one.

Вот тут и затаилось западло: pred не замкнут, значит, он не подходит как аргумент для нумерала в функции вычитания a `minus` b = b pred a
Вот если бы объявить

type CN = forall t . (t->t)->t->t -- за синтаксис не ручаюсь

или что-то в таком роде... Тут я, к сожалению, не копенгаген.
То есть, нужно сделать стирание типа — но не полностью на всё лямбда-исчисление, а прицельно на нумералы.