deniok

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

From:

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

From:

\f g -> g f
\f g -> g (\x -> f x)
\f g -> g(\x -> head[f x, g f])

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

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

From:

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

From:

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

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

From:

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

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

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

From:

Да, там ниже

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

From:

sassa-nf.livejournal.com

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

From:

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

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

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

From:

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

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

From:

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

From:

sassa-nf.livejournal.com

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

From:

sassa-nf.livejournal.com

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

From:

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

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

From:

migmit.livejournal.com

Эм...

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

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

From:

Ух ты!

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

From:

Ты - лучший!

From:

dmytro starosud (from livejournal.com)

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

From:

Терму, к примеру, \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

From:

dmytro starosud (from livejournal.com)

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

From:

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

From:

dmytro starosud (from livejournal.com)

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

From:

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

From:

dmytro starosud (from livejournal.com)

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

From:

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

Edited Date: 2012-06-30 08:17 am (UTC)

From:

dmytro starosud (from livejournal.com)

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

From:

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

From:

dmytro starosud (from livejournal.com)

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

From:

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

From:

dmytro starosud (from livejournal.com)

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

From:

ivan-gandhi.livejournal.com

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

From:

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

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

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

From:

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

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

From: