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

[deniok]

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

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

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

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

Comments

[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, а стало быть не подходит под условие второго вопроса.