Термы с заданными типами

[deniok]

Три задачки с экзамена, в порядке усложнения условия.

Написать замкнутый терм типа (a -> b) -> ((a -> b) -> b) -> b.

Написать замкнутый терм типа (a -> b) -> ((a -> b) -> b) -> b, которому нельзя приписать тип c -> (c -> b) -> b.

Написать замкнутый терм с наиболее общим типом (a -> b) -> ((a -> b) -> b) -> b.

Comments

[slobin.livejournal.com]

1. \f g -> g f
   
2. \f g -> g (\x -> f x)
   
3. \f g -> g(\x -> head[f x, g f])
   

(я не настоящий хаскелист, я каску на стройке нашёл, если что)

... Управление текстовым редактором в нетрезвом состоянии ...

[deni-ok.livejournal.com]

Да, так, только последнее желательно без всяких внешних конструкций типа head и []. В чистой лямбде.

[slobin.livejournal.com]

Я сам понимаю, что желательно. Но пока торможу. :-(

... Какой я математик? Я флюктуация. ...

[slobin.livejournal.com]

\f g -> (\i -> i $ g (\x -> i $ f x))(\x -> x)

Наверное, это можно как-то покороче записать, но в таком виде оно мне в голову пришло.

... Старый, нищий, уродливый и бездарный оптимист ...

[deni-ok.livejournal.com]

Да, там ниже sassa_nf привёл более компактное решение.

[sassa-nf.livejournal.com]

так а в 2. вроде не видно, что f обязательно a->b, а не a->c.

[deni-ok.livejournal.com]

а такого требования и нет.

Prelude> :t (\f g -> g (\x -> f x)) :: (a -> b) -> ((a -> b) -> b) -> b
(\f g -> g (\x -> f x)) :: (a -> b) -> ((a -> b) -> b) -> b
  :: (a -> b) -> ((a -> b) -> b) -> b

В системах в стиле Карри терму можно приписать бесконечное множество типов.

[slobin.livejournal.com]

Может быть, стоит в формулировке вопроса заменить "терм типа" на "терм, которому можно приписать тип". Тогда как бы ясно, что можно и другие. Но я не знаю, какая терминология тут является общепринятой. :-(

... Три категории предвкушения чего-то приятного ...

[deni-ok.livejournal.com]

Мне кажется, что это синонимы.

[sassa-nf.livejournal.com]

ну я прочитал задание так, что если можно приписать a->d, то можно приписать c=a->d, а стало быть не подходит под условие второго вопроса.