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

[deniok]

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

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

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

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

Comments

Наиболее общий тип

[dmytro starosud (from livejournal.com)]

Скажите, пожалуйста, а что значит, "Наиболее общий тип"?

Re: Наиболее общий тип

[deni-ok.livejournal.com]

Терму, к примеру, \x -> x можно приписать разные типы:

\x -> x :: Int -> Int
\x -> x :: Char -> Char
\x -> x :: (Double -> Bool) -> (Double -> Bool)
\x -> x :: (a -> b -> c) -> (a -> b -> c)
\x -> x :: a -> a

Последний является наиболее общим (главным, principle, most general), потому что все остальные могут быть получены из него подстановкой выражения типа вместо переменной типа. Вот эти подстановки:

Int -> Int = [a := Int] a -> a
Char -> Char = [a := Char] a -> a
(Double -> Bool) -> (Double -> Bool) = [a := Double -> Bool] a -> a
(a -> b -> c) -> (a -> b -> c) = [a := a -> b -> c] a -> a

Re: Наиболее общий тип

[dmytro starosud (from livejournal.com)]

Спасибо:)
То есть третье задание - написать терм с конкретным типом, наиболее общим для которого будет заданный?
*(я не мог понять, есть ли и какая разница между вторым и третьим заданием)

Re: Наиболее общий тип

[deni-ok.livejournal.com]

Задание - написать терм, наиболее общим для которого будет заданный. Что значит "с конкретным типом" - мне не очень понятно.

Re: Наиболее общий тип

[dmytro starosud (from livejournal.com)]

Конкретный - это (Int -> Char) -> ((Int -> Char) -> Char) -> Char

Re: Наиболее общий тип

[nponeccop.livejournal.com]

У терма может быть более одного типа. Среди этих типов может найтись самый общий. В третьем задании требуется найти терм по заданному самому общему типу.

Re: Наиболее общий тип

[dmytro starosud (from livejournal.com)]

То есть, решение для второго - это решение для третьего?
*(у меня плохой функциональный бекграунд, поэтому отошлите куда-то, если так будет лучше - литература имеется ввиду)

Re: Наиболее общий тип

[nponeccop.livejournal.com]

Решение для третьего является решением для второго и первого, решение для второго является решением для первого. Но не наоборот!

Re: Наиболее общий тип

[dmytro starosud (from livejournal.com)]

Скажите, пожалуйста, ниже решения для второго и третьего?
\f g -> g (\x -> g f)
\f g -> g (\y -> g ((\x -> f) y))

Re: Наиболее общий тип

[nponeccop.livejournal.com]

Любой из этих двух термов является решением всех трех задач.

Re: Наиболее общий тип

[dmytro starosud (from livejournal.com)]

Спасибо большое!
Простите, я уже наверное достал.
Скажите, пожалуйста, есть ли терм, который будет решением второго задания но не третьего? И какой?

Re: Наиболее общий тип

[deni-ok.livejournal.com]

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

Re: Наиболее общий тип

[dmytro starosud (from livejournal.com)]

Спасибо большое!