Задачка

[deniok]

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

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

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

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

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

Comments

[kodt-rsdn.livejournal.com]

Конечно, имеет.
Просто позабавило. Допустим, мы руками напишем инстанцию класса

instance Num (a->a)->(a->a) where
  0 = \f -> id
  m + n = \f -> m f . n f
  m * n = \f -> m (n f)
  m - n = ?????
  .....

И как компилятор сможет родить нумерал из 123 ?

[migmit.livejournal.com]

При помощи функции fromInteger из того же класса Num. А что?

[kodt-rsdn.livejournal.com]

А, точно. Слона-то я и не приметил.