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

[deniok]

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

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

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

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

Comments

[nponeccop.livejournal.com]

C первым справился :)

[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 и []. В чистой лямбде.

[deni-ok.livejournal.com]

Дорога в тысячу ли... :)

[slobin.livejournal.com]

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

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

[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]

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

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

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

[slobin.livejournal.com]

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

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

[sassa-nf.livejournal.com]

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

[deni-ok.livejournal.com]

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

[sassa-nf.livejournal.com]

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

[deni-ok.livejournal.com]

Да, это кратчайшее из известных мне, даже если переписать в чистой лямбде, без (.)

Prelude> :t \f g -> g (\y -> g ((\x -> f) y))
\f g -> g (\y -> g ((\x -> f) y))
  :: (t1 -> t) -> ((t1 -> t) -> t) -> t

[deni-ok.livejournal.com]

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

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

[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]

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

[migmit.livejournal.com]

Эм...

Prelude> :t \f g -> g (\a -> g f)
\f g -> g (\a -> g f) :: (t -> t1) -> ((t -> t1) -> t1) -> t1

Первая попытка решить вторую задачу.

[slobin.livejournal.com]

Ух ты!

... Мимореальный музей ...

[deni-ok.livejournal.com]

Ты - лучший!

[ivan-gandhi.livejournal.com]

Ах какие задачки! И какие решения!

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

[nponeccop.livejournal.com]

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

[nponeccop.livejournal.com]

Сформулированы только плохо. Например, не указано исчисление и система типов.

Так, в Haskell98 одним из решений первой задачи является undefined, а в System F с самыми общими типами плохо.

Вот ещё задачка: есть ли в System F у "\f g -> g (\a -> g f)" тип, более общий, чем "милнеровский" или не сравнимый с ним.

[nivanych.livejournal.com]

А теперь — всё в категорном виде!
;-)

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

[dmytro starosud (from livejournal.com)]

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

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)]

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

[deni-ok.livejournal.com]

> Сформулированы только плохо. Например, не указано исчисление и система типов.

Ну да, согласен. Проще всего сказать, что термы - чистое лямбда-исчисление (переменные+аппликация+абстракция), а типы - Haskell98. Термин Simply typed lambda calculus не очень однозначен: некоторые под ним понимают систему, более простую чем нужно, в которой типы конструируют из стрелочек и констант (а не переменных с возможностью подстановки).

[nponeccop.livejournal.com]

Что значит "некоторые"? В lambda calculi with types Барендрегта и в википедии понимают стрелочки и константы. У вас есть источники, где понимают что-то другое?

Просто сказать "Haskell98" не годится, т.к. есть классы типов, рекурсия, алгебраики, let и undefined.

В системе Хиндли-Милнера есть let, и многие поймут её как систему Майкрофта, в которой есть также и рекурсия, или даже как весь ML.

Можно было бы сказать "prenex-фрагмент System F" (где нет let, рекурсии и undefined!) но это исчисление a la Church.

Вдобавок, есть великое множество похожих, но неэквивалентных исчислений с одинаковым названием (например, бета-ЛИ vs бетаэта-ЛИ, или ЛИ с НФ vs ЛИ с СЗНФ) и из-за того что спрашивающий и отвечающий по разному трактуют похожесть, могут возникнуть проблемы, точно указать, какие именно отличия важны, а какие - нет, практически невозможно, есть шанс что найдётся какое-то экзотическое исчисление, которое подходит под условие задачи, но точно не имеется ввиду.

Так что проще всего сказать "В Haskell 98, используя только переменные, аппликацию и лямбда-абстракцию, найти выражения ..."