Задачка

[deniok]

Хорошая задачка из Herman Geuvers, Introduction to Type Theory (упражнение 3.17):

Построить лямбда-терм с типом ((α → β) → α) → (α → α → β) → β.

Ответы скринить не буду.

UPD: Имеется в виду просто типизированная лямбда. То есть fix и прочие Y-комбинаторы нам недоступны.

UPD2: Рекурсия ни в каком виде недоступна!

Comments

[asviraspossible.livejournal.com]

Если поменять местами, то:

f :: ((a -> b) -> a) -> (a -> (a -> b)) -> b
f a b = b x x
  where x = fix (a . b)

[deni-ok.livejournal.com]

А без fix?

[asviraspossible.livejournal.com]

Что-то пока не получается без fix :(... Попозже попробую...