deniok: (Default)
deniok ([personal profile] deniok) wrote2012-06-28 05:04 pm

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

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

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

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

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

[identity profile] deni-ok.livejournal.com 2012-06-28 03:26 pm (UTC)(link)
а такого требования и нет.
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
В системах в стиле Карри терму можно приписать бесконечное множество типов.

[identity profile] slobin.livejournal.com 2012-06-28 03:49 pm (UTC)(link)
Может быть, стоит в формулировке вопроса заменить "терм типа" на "терм, которому можно приписать тип". Тогда как бы ясно, что можно и другие. Но я не знаю, какая терминология тут является общепринятой. :-(

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

[identity profile] deni-ok.livejournal.com 2012-06-28 04:13 pm (UTC)(link)
Мне кажется, что это синонимы.

[identity profile] sassa-nf.livejournal.com 2012-06-28 03:53 pm (UTC)(link)
ну я прочитал задание так, что если можно приписать a->d, то можно приписать c=a->d, а стало быть не подходит под условие второго вопроса.