Здесь лежит по-моему интересная лекция с Google Talks (из серии Advanced Topics in Programming Languages Series, Mirrorer приводил не так давно другую лекцию из этой серии
: система Хиндли-Милнера, изоморфизмы Карри-Говарда, Жирарда-Рейнольдса. Довольно интересна идея "вывода кода" как изоморфизма выводу типов, только не знаю, имеет ли это реальное практическое применение.
Здравствуйте, Курилка, Вы писали:
К>Здесь лежит по-моему интересная лекция с Google Talks (из серии Advanced Topics in Programming Languages Series, Mirrorer приводил не так давно другую лекцию из этой серии
: система Хиндли-Милнера, изоморфизмы Карри-Говарда, Жирарда-Рейнольдса. Довольно интересна идея "вывода кода" как изоморфизма выводу типов, только не знаю, имеет ли это реальное практическое применение.
Прикольное видео, а как ты на него набрёл? Есть rss feed какой-то, где только по этой теме ссылки?
: система Хиндли-Милнера, изоморфизмы Карри-Говарда, Жирарда-Рейнольдса. Довольно интересна идея "вывода кода" как изоморфизма выводу типов, только не знаю, имеет ли это реальное практическое применение.
Да, Girard-Reinolds isomorphism многое проясняет. (Из кода выводим тип) изоморфно (из типа выводим код). Надо бы скачать Djinn, мне особенно понравился автоматический вывод кода монадического бинда из его типа.
Здравствуйте, deniok, Вы писали:
D>Да, Girard-Reinolds isomorphism многое проясняет. (Из кода выводим тип) изоморфно (из типа выводим код). Надо бы скачать Djinn, мне особенно понравился автоматический вывод кода монадического бинда из его типа.
Только вот примеров реальной пользы такого я чтот не могу придумать, как это дело можно "заюзать".
Здравствуйте, Курилка, Вы писали:
К>Здравствуйте, deniok, Вы писали:
D>>Да, Girard-Reinolds isomorphism многое проясняет. (Из кода выводим тип) изоморфно (из типа выводим код). Надо бы скачать Djinn, мне особенно понравился автоматический вывод кода монадического бинда из его типа.
К>Только вот примеров реальной пользы такого я чтот не могу придумать, как это дело можно "заюзать".
Да ладно там с пользой. Понять бы, как это работает. Вот я написал "монадический бинд", и по типу это так:
даём Джину тип bind для Continuation monad
bindC :: C a -> (a -> C b) -> b
и Djinn выводит
bindC x1 x2 x3 = x1 (\c15 -> x2 c15 x3)
И у меня сразу вопрос: поскольку после определения типа
type C a = (a -> Ans) -> Ans
всё остальное автоматизировано, то получается, что выполнение монадических законов сидит в этом определении типа С?
Здравствуйте, lomeo, Вы писали:
L>Здравствуйте, Курилка, Вы писали:
К>>Только вот примеров реальной пользы такого я чтот не могу придумать, как это дело можно "заюзать".
L>Умный редактор, например. Когда программируешь от типов, очень полезно, а то приходится лезть в djinn.
Типа пишешь сигнатуру, он тебе тело генерит, потом его правишь? вместо x, скажем, 2*x пишешь?
Здравствуйте, deniok, Вы писали:
D>всё остальное автоматизировано, то получается, что выполнение монадических законов сидит в этом определении типа С?
Мне кажется, что оно сидит в определении типа bind. Т.е. IMHO, если мы выводим однозначно return и bind, то законы будут соблюдаться.
Доказать не могу :-)
Здравствуйте, Курилка, Вы писали:
К>Типа пишешь сигнатуру, он тебе тело генерит, потом его правишь? вместо x, скажем, 2*x пишешь?
Ну с числовыми/символьными типами там всё посложнее будет. Например, djinn по умолчанию и не знает ничего про Int.
Но вот для State он тебе выведет инстанс монады. А я когда его писал, то писал сначала join, потом из него выводил bind.
Сейчас в подобных ситуациях я пользуюсь djinn'ом.
Здравствуйте, lomeo, Вы писали:
L>Здравствуйте, deniok, Вы писали:
D>>всё остальное автоматизировано, то получается, что выполнение монадических законов сидит в этом определении типа С?
L>Мне кажется, что оно сидит в определении типа bind. Т.е. IMHO, если мы выводим однозначно return и bind, то законы будут соблюдаться. L>Доказать не могу
Хех! То есть ты утверждаешь ещё более сильную вещь, чем я: невозможно написать валидного инстанса монады, который не удовлетворял бы монадическим законам.
В GIH сказано так
Mathematically, monads are governed by set of laws that should hold for the monadic operations. This idea of laws is not unique to monads: Haskell includes other operations that are governed, at least informally, by laws. For example, x /= y and not (x == y) ought to be the same for any type of values being compared. However, there is no guarantee of this: both == and /= are separate methods in the Eq class and there is no way to assure that == and =/ are related in this manner. In the same sense, the monadic laws presented here are not enforced by Haskell, but ought be obeyed by any instances of a monadic class. The monad laws give insight into the underlying structure of monads: by examining these laws, we hope to give a feel for how monads are used.
То есть in the same sense, что и для = и =/, относится только к are not enforced, а не к ought be obeyed?
Здравствуйте, deniok, Вы писали:
D>Хех! То есть ты утверждаешь ещё более сильную вещь, чем я: невозможно написать валидного инстанса монады, который не удовлетворял бы монадическим законам.
Нет, нет, я говорил об однозначности. Если code inference вывел нам единственную реализацию (как в случае type C a), mо она будет верной в смысле исполнения монадических законов. Когда то я раздумывал над похожими вещами. Моё заявление — отголоски тех "раздумий" ;-)
Здравствуйте, lomeo, Вы писали:
L>Здравствуйте, deniok, Вы писали:
D>>Хех! То есть ты утверждаешь ещё более сильную вещь, чем я: невозможно написать валидного инстанса монады, который не удовлетворял бы монадическим законам.
L>Нет, нет, я говорил об однозначности. Если code inference вывел нам единственную реализацию (как в случае type C a), mо она будет верной в смысле исполнения монадических законов.
Он, что, может вывести не единственную реализацию? Это интересно, а как это коррелирует с Girard-Reinolds изоморфизмом; я в лекции это место как-то не осознал до конца: в обычную-то сторону principal type выводится однозначно, значит и в другую "principal code " тоже должен быть однозначен, нет? Там в примерах были две реализации для одного типа, но лектор как-то невнятно пробормотал про их эквивалентность.
Здравствуйте, deniok, Вы писали:
D>Он, что, может вывести не единственную реализацию? Это интересно, а как это коррелирует с Girard-Reinolds изоморфизмом; я в лекции это место как-то не осознал до конца: в обычную-то сторону principal type выводится однозначно, значит и в другую "principal code " тоже должен быть однозначен, нет? Там в примерах были две реализации для одного типа, но лектор как-то невнятно пробормотал про их эквивалентность.
Да вроде внятно — код должен быть эквивалентным с точностью до изоморфизма.
Здравствуйте, Курилка, Вы писали:
К>Да вроде внятно — код должен быть эквивалентным с точностью до изоморфизма.
Вот я и пытаюсь понять: для данного монадического инстанса не может быть два разных bind'а/return'а? Если нет, то монада это или нет, задаётся самим определением этого инстанса и монадические законы должны автоматом выполняться для любой монады. Мне просто казалось, что это не так, то есть что мы это отдельно должны проверить. Мы, собственно, полгода назад здесь хором доказывали, что для Maybe они выполняются. Теперь, вроде, оказывается что это автоматом следует из того, что нам удалось написать для Maybe bind с return'ом.
Здравствуйте, Курилка, Вы писали:
К>Здесь лежит по-моему интересная лекция с Google Talks (из серии Advanced Topics in Programming Languages Series, Mirrorer приводил не так давно другую лекцию из этой серии
: система Хиндли-Милнера, изоморфизмы Карри-Говарда, Жирарда-Рейнольдса. Довольно интересна идея "вывода кода" как изоморфизма выводу типов, только не знаю, имеет ли это реальное практическое применение.
Здравствуйте, deniok, Вы писали:
D>Вот я и пытаюсь понять: для данного монадического инстанса не может быть два разных bind'а/return'а? Если нет, то монада это или нет, задаётся самим определением этого инстанса и монадические законы должны автоматом выполняться для любой монады. Мне просто казалось, что это не так, то есть что мы это отдельно должны проверить. Мы, собственно, полгода назад здесь хором доказывали, что для Maybe они выполняются. Теперь, вроде, оказывается что это автоматом следует из того, что нам удалось написать для Maybe bind с return'ом.
Всего лишь предположение! И об именно однозначном (точне — единственном) варианте.
Например для
data W a = W a a
djinn может вывести bind
f (W _ a) b = case b a of W d e -> W e d
Разумеется, закон о правом return не будет соблюдаться.
Также можно для этого типа реализовать и верный вариант (правда джин мне его не показал). Но он не единственный ;-)
