Как-то странно, что на РСДН ещё не появилась ссылка о сабже. Там приводится очень интересная работа Тёрнера, раскрывающая тему терминируемости алгоритмов, приводится базовый язык, в котором чётко разделяется data как базис примитивных типов и codata как базис для структурной рекурсии. По сути он говорит, что даже haskell недостаточно строг (формален), т.к. допускает _|_ (bottom), однако эта нестрогость даёт достаточную свободу для решения практических задач, поэтому традиционное ФП он называет слабым, а искомую систему — сильным ФП (аналогично языкам со слабой и сильной системами типов).
Очень хорошая статья! Чуть расширю аннотацию Курилки и разбавлю собственными мыслями.
Turner пишет, что _|_ приносит в язык бОльшую сложность:
С новым значением типа рассматриваемая функция будет вести себя иначе, нежели так, как описано в коде для обычных значений, значит у нас:
1. Доказательства (equational reasoning, term rewriting, сами программы) усложняются существенно
Пример из статьи: "e — e" не всегда равно 0
2. Усложняется дизайн языка — вводятся такие понятия, как doubly-strict, left-strict, right-strict
Пример: a || b не всегда равно b || a.
Для total fp — вообще разница между нормальным и аппликативным порядком отсутствует (в смысле получения нормальной формы)
3. В total fp редукция строга по Чёрчу-Россеру — нормальная форма существует и достижима любым порядком редукции.
По сути все эти пункты есть одно и то же. Т.к. мы имеем strong Church-Rosser property (пункт 3), то выбор порядка редукции не повлияет на семантику (пункт 2), и, следовательно, как косвенное преимущество мы имеем простой equational reasoning (пункт 1).
И всё это из-за какого то bottom! На самом деле, эти проблемы не часто возникают на практике. Но очень уж неожиданно — вдруг окажется, что ListT не является монадой, потому что недостаточно ленив, ну и часто у кого нибудь из вас были проблемы с bottom с этой стороны? А вот то, что доказательства усложняются — это гораздо более важно, IMHO. Т.е. вы не пользуетесь этим ListT, а разрабатываете его. Допустить подобную ошибку (изменение семантики в зависимости от порядка редукции) очень легко. А в Haskell, например, её сделать очень легко, потому как с повсеместной ленивостью часто используется "энергичный" паттерн матчинг.
С другой стороны аналог bottom в языках с null — сам null. Ошибок с null гораздо больше, чем с bottom. Это утешает И удаление bottom из языка приносит дополнительные трудности — приходётся овладеть дисциплиной программирования на total fp. В статье приводятся примеры — quick sort, быстрое возведение в степень. Как аналог этого — использование в Haskell типов-обёрток для ряда задач — обхода ограничений тайп-чекера, привнесение строгости (тут, правда, это не в тему).
С практической точки зрения стоит вопрос — насколько большие преимущества мы получаем, по сравнению с тем, что теряем. Мне бы, например, очень хотелось попробовать, чтобы сравнить и вообще получить представление о том, как пишется при total fp. Пока у меня складывается впечатление, что я и так пишу на Haskell схожим образом, обычно не учитывая bottom, и удовлетворяюсь упрощёнными почти-доказательствами, опять таки без bottom. Соотвественно, вероятность ошибки на Haskell есть. Было бы интересно узнать насколько она существенна. С практической точки зрения.
Ну и разумеется, решение, которое предлагает Turner для организации бесконечного исполнения программ — отдельные codata. Мне это было не особо интересно, потому что подобная идея — явное разделение data и codata в дизайне языка — уже рассматривалась. По крайней мере, я помню, что в паре мест я точно про это читал.
Ну и язык не будет Turing complete. Но зато все программы с data-типом будут гарантированно завершаться.
Здравствуйте, lomeo, Вы писали:
L>Ну и разумеется, решение, которое предлагает Turner для организации бесконечного исполнения программ — отдельные codata. Мне это было не особо интересно, потому что подобная идея — явное разделение data и codata в дизайне языка — уже рассматривалась. По крайней мере, я помню, что в паре мест я точно про это читал.
Предложения-то предложениями, вопрос гдеж язык для tfp?
Кстати, подумал, что в свете предложенных Тёрнером идей (не использовать head/tail, а только паттерн матчинг), проблем с эффективностью, подобных этой не будет.
Здравствуйте, lomeo, Вы писали:
L>Здравствуйте, Курилка, Вы писали:
L>Кстати, подумал, что в свете предложенных Тёрнером идей (не использовать head/tail, а только паттерн матчинг), проблем с эффективностью, подобных этой не будет.
Здравствуйте, lomeo, Вы писали:
L>Здравствуйте, Курилка, Вы писали:
К>>Предложения-то предложениями, вопрос гдеж язык для tfp?
L>Ща... дай только полчасика
Кстати фишка — интерпретатор же нельзя будет написать для этого языка на нём самом, насколько я понимаю. Т.е. бутстрапинг идёт лесом или я что-то нпаутал?
Здравствуйте, Курилка, Вы писали:
К>Кстати фишка — интерпретатор же нельзя будет написать для этого языка на нём самом, насколько я понимаю. Т.е. бутстрапинг идёт лесом или я что-то нпаутал?
Интерпретатор нельзя, но я очень плохо этот момент понял. Там приводятся аналогии, но в целом я картину не вижу.
Здравствуйте, lomeo, Вы писали:
L>Здравствуйте, Курилка, Вы писали:
К>>Кстати фишка — интерпретатор же нельзя будет написать для этого языка на нём самом, насколько я понимаю. Т.е. бутстрапинг идёт лесом или я что-то нпаутал?
L>Интерпретатор нельзя, но я очень плохо этот момент понял. Там приводятся аналогии, но в целом я картину не вижу.
По мне дак всё относительно просто, базис — первая теорема Гёделя о неполноте, получается что языки с "жопами" до конца не формализуемы, а бутстрапинг берёт ассемблер (или что-то подобное), где они уже "встроены". И наверное полноты по Тьюрингу может тут не хватить, хотя тут уже я как-то теряюсь.
Здравствуйте, Курилка, Вы писали:
L>>Кстати, подумал, что в свете предложенных Тёрнером идей (не использовать head/tail, а только паттерн матчинг), проблем с эффективностью, подобных этой не будет.
К>Ммм, почему?
Потому что мы не сможем написать вариант с tail — такой функции просто нет.
Я имел в виду существующую в Haskell ситуацию — нормальный порядок редукции, энергичный паттерн матчинг.
Хотя, честно говоря это очень конкретный случай, думаю, важнее то, что компилятор, зная что семантика от порядка редукции не зависит, сможет сам выбирать стратегию (либо это можно указывать в директивах, например).
Здравствуйте, lomeo, Вы писали:
L>Здравствуйте, Курилка, Вы писали:
L>>>Кстати, подумал, что в свете предложенных Тёрнером идей (не использовать head/tail, а только паттерн матчинг), проблем с эффективностью, подобных этой не будет.
К>>Ммм, почему?
L>Потому что мы не сможем написать вариант с tail — такой функции просто нет. L>Я имел в виду существующую в Haskell ситуацию — нормальный порядок редукции, энергичный паттерн матчинг.
L>Хотя, честно говоря это очень конкретный случай, думаю, важнее то, что компилятор, зная что семантика от порядка редукции не зависит, сможет сам выбирать стратегию (либо это можно указывать в директивах, например).
По ходу и оптимизации можно будет "жёстче" делать: выбрасывать e-e и т.п. Раздолье для частичных вычислений.
Здравствуйте, lomeo, Вы писали:
L>Здравствуйте, geniepro, Вы писали:
G>>Похоже, придётся учить Эпиграм и какой-то там Charity
L>Так точно, Charity. nontermination, data/codata, bottom нет.
Кто-нибудь его вообще руками пробовал? Вон thesz говорит, что его синтаксис отпугнул
Тёрнер пишет о необходимости чего-нибудь юзабельного, но пока, судя по всему, эта ниша не занята.
Здравствуйте, Курилка, Вы писали:
К>Кто-нибудь его вообще руками пробовал? Вон thesz говорит, что его синтаксис отпугнул К>Тёрнер пишет о необходимости чего-нибудь юзабельного, но пока, судя по всему, эта ниша не занята.
Я сейчас ковыряю Charity. Проект, похоже, давно умер, новостей много лет (с 2000 г) уже нет.
Интерпретатор доступен в исходниках (1995 г), под винду (1997 г) и под линуху.
После Хаскелла Charity выглядит несколько непривычно, чем-то (словом def) напоминает сразу Hope, Python и Nemerle... :о)
The language charity starts from the basis that one can and should actually implement standard mathematics without trickery. Thus, we eliminate the uncomfortable transition
?
---->
discrete mathematics <---- Program
?
by basing the discrete mathematics in distributive categories and making the programming language charity which makes them the same pursuit.
Сделать факториал сходу не вышло, надо читать мануалы... :о)
По-моему, виндовый интерпретер prelud не загружает?..
Здравствуйте, geniepro, Вы писали:
G>Здравствуйте, Курилка, Вы писали:
К>>Кто-нибудь его вообще руками пробовал? Вон thesz говорит, что его синтаксис отпугнул К>>Тёрнер пишет о необходимости чего-нибудь юзабельного, но пока, судя по всему, эта ниша не занята.
G>Я сейчас ковыряю Charity. Проект, похоже, давно умер, новостей много лет (с 2000 г) уже нет.
Может просто Тёрнеру мыльнуть, спросить, смотрел ли он сей проект и есть ли другие примеры подобного?
Да и в Калгари написать, спросить, что с проектом и куда наработки пошли?
Здравствуйте, geniepro, Вы писали:
G>Сделать факториал сходу не вышло, надо читать мануалы... :о)
Я в fold не нашёл как получить само значение (не уже отфолденное, а исходное). Поэтому можно сделать с извращением через списки/косписки.
G>По-моему, виндовый интерпретер prelud не загружает?..
Charity >> rf "PRELUDE.ch".
Вообще, язык мне показался очень неудобным из-за таких мелочей.
Здравствуйте, lomeo, Вы писали:
[cut] L>Вообще, язык мне показался очень неудобным из-за таких мелочей.
Дык идеи Тёрнера как раз были про юзабилити, а юзабилити мёртвого проекта вещь, сам понимаешь, статическая — единстенный вариант оживлять его. Но так хотяб базис будет. Вопрос — нужен ли он?
Здравствуйте, Курилка, Вы писали:
К>Дык идеи Тёрнера как раз были про юзабилити, а юзабилити мёртвого проекта вещь, сам понимаешь, статическая — единстенный вариант оживлять его. Но так хотяб базис будет. Вопрос — нужен ли он?
Так прикол в том, что не надо придумывать отдельные правила для data и codata — это мне очень понравилось, т.е. мы выделяем их не ключевыми словами, а тем, с какой стороны от стрелки стоит тип — ощущение, что программируешь на языке теории категории. data у нас F-алгебра, и поэтому мы явно выписываем её сигнатуру (имеется в виду сигнатура F-алгебры), т.е. data nat -> C. А вот codata у нас F-коалгебра, и её сигнатура будет data C -> conat. Разумеется, слово data я взял из Charity в ТК его нет Ну и nat/conat здесь FC конец сигнатуры алгебры/коалгебры. Соотвественно, над intial F-алгебрами мы можем проделывать катаморфизм (fold), а над терминальной F-коалгеброй анаморфизм (unfold), что тоже явно отражено в языке.
Хотя, возможно, с практической точки зрения это неудобно. Может быть использовать его как целевой язык? Хотя тут проблемы с тем же fold — как блин вытащить текущее значение, а не уже отфолденный результат, я так и не понял
На самом деле, эти проблемы не часто возникают на практике. Но очень уж неожиданно — вдруг окажется, что ListT не является монадой, потому что недостаточно ленив, ну и часто у кого нибудь из вас были проблемы с bottom с этой стороны? А вот то, что доказательства усложняются — это гораздо более важно, IMHO. Т.е. вы не пользуетесь этим ListT, а разрабатываете его. Допустить подобную ошибку (изменение семантики в зависимости от порядка редукции) очень легко. А в Haskell, например, её сделать очень легко, потому как с повсеместной ленивостью часто используется "энергичный" паттерн матчинг.
