Как-то странно, что на РСДН ещё не появилась ссылка о сабже. Там приводится очень интересная работа Тёрнера, раскрывающая тему терминируемости алгоритмов, приводится базовый язык, в котором чётко разделяется 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-типом будут гарантированно завершаться.

Здравствуйте, deniok, Вы писали:

D>А. Пора свой язык делать?

Вместо того, чтобы трепаться на форумах?? Ну, нееееет....

Здравствуйте, lomeo, Вы писали:

L>Вот, кстати, нашёл книжку — буду читать
L>Categorical programming with inductive and coinductive types

Это ж диссертация Varmo Vene, известный текст. Он в Тарту заведующий кафедрой. Мы в своё время долго мучались над языком его презентации, оказавшимся эстонским.

Здравствуйте, Курилка, Вы писали:

К>Дак, то что нету это ясно.
К>Смотри, по Гёделю формальные алг. системы расширяются за счёт постулатов, выходящих за их рамки.
К>Получается что параморфизм есть пример подобного "выхода за рамки". Не се па?

Уи. Только, возможно, я просто чего то недоглядел в Charity.

Вот, кстати, нашёл книжку — буду читать
Categorical programming with inductive and coinductive types

Вот тут нашёл: http://www.cs.ut.ee/~varmo/papers/
Там ещё до кучи.

Здравствуйте, Курилка, Вы писали:

К>Кто-нибудь его вообще руками пробовал? Вон 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 не загружает?..

Здравствуйте, deniok, Вы писали:

D>Это всё разные примитивы (паттерны) рекурсии. Факториал "естественно" не записать как катаморфизм над Nat = Nil | Succ Nat. Параморфизм как раз об факториало-подобном паттерне.

Потому и написал — с извращением можно, например, сделать

fac n = product [1..n]

и получать текущий элемент при катаморфизме из длины формируемого списка.

Вот написал даже, чтобы оценили уровень извращённости:

rf "PRELUDE.hs".

def to = n => {| zero : () => nil
               | succ : x => cons(sub(n, length x), x)
               |} n.

def product = l => {| nil : () => one
                    | cons : (h,t) => mul(h,t)
                    |} l.

def fac = n => product to n.

Здравствуйте, lomeo, Вы писали:

L>Здравствуйте, Курилка, Вы писали:

К>>Кстати фишка — интерпретатор же нельзя будет написать для этого языка на нём самом, насколько я понимаю. Т.е. бутстрапинг идёт лесом или я что-то нпаутал?

L>Интерпретатор нельзя, но я очень плохо этот момент понял. Там приводятся аналогии, но в целом я картину не вижу.

По мне дак всё относительно просто, базис — первая теорема Гёделя о неполноте, получается что языки с "жопами" до конца не формализуемы, а бутстрапинг берёт ассемблер (или что-то подобное), где они уже "встроены". И наверное полноты по Тьюрингу может тут не хватить, хотя тут уже я как-то теряюсь.

Здравствуйте, Константин Л., Вы писали:

КЛ>Здравствуйте, Курилка, Вы писали:

КЛ>простите что влязию своей небритой глупой мордой, но где можно доходчиво почитать про ваши бананы, и прочие умные вещи. выжимки бы

К ТФП это правда отношения вроде непосредственного не имеет, но если хочется, начни с вики (статья про КАТАморфизм, он же банан, там же смотри ссылки на другие морфизмы), плюс там же ссылка на (возможно эпохальную ) статью Мейера, Фоккинги и Патерсона (вроде как Мейер по сути монады в линке к шарпу "прикрутил" )

Здравствуйте, Константин Л., Вы писали:

КЛ>простите что влязию своей небритой глупой мордой, но где можно доходчиво почитать про ваши бананы, и прочие умные вещи. выжимки бы

Бананы, линзы, оригами и примкнувшая к ним сегодня натуральность fold

Здравствуйте, geniepro, Вы писали:

G>Здравствуйте, Константин Л., Вы писали:

КЛ>>простите что влязию своей небритой глупой мордой, но где можно доходчиво почитать про ваши бананы, и прочие умные вещи. выжимки бы

G>Бананы, линзы, оригами и примкнувшая к ним сегодня натуральность fold

Раз уж тут мой блог цитируют, то продолжение конспекта Bananas in Space:
Алгебры и катаморфизмы
Коалгебры и анаморфизмы
Ну и это всё-таки весьма сжатый конспект, хотя и с подробным разбором примеров.

Здравствуйте, Константин Л., Вы писали:

КЛ>простите что влязию своей небритой глупой мордой, но где можно доходчиво почитать про ваши бананы, и прочие умные вещи. выжимки бы

Про бананы (свёртка, fold) можно почитать с самого начала в Why FP matters. Или в её русском переводе.

Вообще про свёртку рассказывается в любом учебнике ФП: SICP, The Craft of Functional Programming etc. Первое есть в русском переводе, кстати, можно в инете найти.

Интересно о свойствах свёртки написано в A tutorial on the universality and expressiveness of fold.

Более подробно про распространение свёртки на алгебраические типы, отличные от списков, можно почитать в Merging Monads and Folds for Functional Programming.

Изначально термин банан происходит из уже указывавшейся здесь классической Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire.

С точки зрения теории категорий свёртка есть катаморфизм (специальный морфизм из initial F-алгебры). Для ознакомления можно почитать статью на вики — там есть и переложение на Haskell.

Также обсуждение свёртки неоднократно встречалость в этом форуме.

Это — бананы, а другие умные вещи — это что?

Здравствуйте, lomeo, Вы писали:

L>Здравствуйте, Курилка, Вы писали:

L>>>Кстати, подумал, что в свете предложенных Тёрнером идей (не использовать head/tail, а только паттерн матчинг), проблем с эффективностью, подобных этой не будет.

К>>Ммм, почему?

L>Потому что мы не сможем написать вариант с tail — такой функции просто нет.
L>Я имел в виду существующую в Haskell ситуацию — нормальный порядок редукции, энергичный паттерн матчинг.

L>Хотя, честно говоря это очень конкретный случай, думаю, важнее то, что компилятор, зная что семантика от порядка редукции не зависит, сможет сам выбирать стратегию (либо это можно указывать в директивах, например).

По ходу и оптимизации можно будет "жёстче" делать: выбрасывать e-e и т.п. Раздолье для частичных вычислений.

Здравствуйте, lomeo, Вы писали:

L>Здравствуйте, Курилка, Вы писали:

К>>Ещё мысль-вопрос в сторону: наличие НФ для терминируемой функции в итоге даёт возможность точно определить время выполнения функции, исходя из известного времени выполнения неких "примитивных" блоков (базиса языка). Я правильно всё понимаю?

L>Нет, мне кажется. То что у выражения есть НФ не говорит о том, как она достигается. Ведь reduction sequence нам заранее не известен.

Но в языке с ограниченным набором паттернов рекурсии и отделённой кодатой такая оценка возможна, нес па? Выгоды от Тьюринг-неполноты должны же быть?

Здравствуйте, lomeo, Вы писали:

L>Здравствуйте, Курилка, Вы писали:

К>>Ну, скажем так, не исключаю такой возможности, про "отписывайся" — это подкол? (без смайла не всегда понятна интонация предложений )
К>>А то фп-фп, а толку...
К>>Хочется хоть чем-то помочь Родине

L>Никакого смайла, просто если ты будешь рисовать, то пиши, что получается интересного в процессе — это всё, что я хотел сказать.
L>Мне будет очень интересно это почитать, пообсуждать.

Ну слово "отписываться" многозначное, я не то значение выбрал, блин, думал от топика отписываться, чтоб время появилось
Думаю имеет смысл инициативную группу собрать, наверное на хугах в феврале стоит рассмотреть этот вопрос. Коллективный разум он помощнее будет, параллелизация понимаешь

Здравствуйте, geniepro, Вы писали:

G>Я вот прихожу постепенно к выводу, что Total FP в удобном (юзабельном) виде -- это фантастика. В смысле -- невозможно.

Возможно. Для меня интерес представляет сам подход. Насколько он будет юзабелен я смогу оценить только попробовав на задаче.
Что касается практической ценности, то это как с обсуждавшейся тут теоремой Ферма, в прямой ценности я сомневаюсь (что касается вещ. чисел, например), но вот кучу бенефитов при разборе этого подхода я надеюсь получить.

G>Total FP, как я понял, ориентирован на математической индукции, которая работает только на натуральных числах, и на списочной индукции. Отсюда два важных ограничения -- родными для TFP будут натуральные числа (с двумя операциями + и *) и конечные списки.

Хотя бы для какой то группы функций мы можем быть уверенными в завершимости.

G>То есть об удобной работе с вещественными числами (а возможно даже и с отрицательными целыми), похоже, придётся забыть, и некоторые удобные приёмы, связанные с ленивыми бесконечными списками, тоже отпадут. (Правда, я плохо знаю всякие там коданные/косписки/комонады/корекурсии/ко.....)

Если список бесконечен, то это кодата.
Что касается вещественных чисел, то это просто вопрос, с которым надо разобраться. Возможно, там можно принять какое то практические решение. В конце концов не считать некоторые функции гарантировано завершимыми. Это и вопрос с bottom мне, если честно, интересен не так как структурная рекурсия, например, или вывод гарантии завершимости.

G>Так что же получается? Стоит ли Total FP того, что бы с ним заморачиваться?

Думаю, да.

G>Даёт ли гарантированная останавливаемость функций достаточно бенефитов, что бы оправдать кучу неудобств?

Думаю, зависит от.

Здравствуйте, geniepro, Вы писали:

L>> Ну и будет, что однажды зайдя в Maybe мы уже из него не выйдем, т.е. используя в своей функции функцию с Maybe типом, мы обязаны также вернуть Maybe, ну так чем это отличается от поведения error?

G>Вовсе не обязательно, это ведь не монада IO... ;о)

Э-э-э.. Не понял при чём тут IO.

G>Допустим, у нас есть некая функция, результат которой зависит от, например, операции деления, которая на некоторых параметрах этой функции даёт бесконечность.
G>В зависимости от наших задач у нас есть два варианта:
G>1) засунуть результат такой функции в Maybe;
G>2) принять в качестве деления на ноль какое-то дефолтное значение, а результат всей функции считать по-любому нормальным числом.

Да, я читал статью Тёрнера и знаю об этих вариантах.

Недостаток первого варианта я описал: однажды зайдя в Maybe, мы из него не выйдем.
Недостаток второго: неестественность некоторых результатов операций (как деление на 0, например), которая может привести к ошибкам в логике. Но тут я не поручусь — надо почитать как Runciman разбирается с этой проблемой.

Оба недостатка имеют практический характер. В первом случае неудобно, во втором противоестественно

Здравствуйте, Курилка, Вы писали:

G>>А при чём здесь монады? ???
G>>Я имел в виду обычный АлгТД Maybe a, у которого два варианта -- допустимое значение (Just a) и отсутствие такового (Nothing).
К>Ага, читаем вики хотябы.
К>Ёжики кололись, плевались, но не понимали, что использовали монады
К>В том и суть монад, что так-то это вроде как обычный АлгТД
К>(хотя тут могу врать, т.к. не знаю точного мат. смысла термина "обычный АлгТД")

АТД — это сумма произведений, или дизъюнкция конъюнкций

А суть монад в том, чтобы связывать вычисления. Если мы используем fromJust для Maybe вычисления — это уже не монадическое использование и говорить тут о монадах бессмысленно. Если же (как в ТФП) fromJust вещь запрещённая, то нам приходится протягивать значения до конца, т.е. мы получим связку типа Maybe a -> (a -> Maybe b) -> Maybe b — это уже монада.

Простой пример:

(/) :: (Num n) => n -> n -> Maybe n

Допустим мы считаем силу притяжения:

g * (m1 * m2) / (r^2)

Т.к. мы не можем сделать fromJust, то нам приходится тип этого выражения тоже выставлять в Maybe. Теперь допустим, что при расчёте числителя (или знаменателя) тоже используется (/). Значит тип у операции должен быть:

(/) :: (Num n) => Maybe a -> Maybe a -> Maybe n

Теперь предположим, что нам надо сложить что-нибудь с результатом деления (a/b + x). Значит и у операции (+) должен быть типа -> Maybe a. Таким образом, мы приходим к тому, что все операции над числами будут Maybe a -> Maybe a -> Maybe n. Зная это мы можем добавить сахара в язык и читать конструктор 123 как Just 123. Дальше — больше — какие то внешние операции, которые должны принимать только числа (а не Maybe) должны быть описаны с операцией над Nothing тоже:

printNum :: Num n => Maybe n -> IO () -> IO ()

Второй параметр — операция, в случае Nothing. Выделяя комбинатор получим:

catchNothing :: Num n => (n -> a) -> a -> Maybe n -> a

Первый параметр — работа с числом, второй — результат при Nothing, третий — собственно число. Например

printNum :: Num n => n -> IO ()
someExpr :: Num n => Maybe n

printMaybeNumWithErrorMsg = printNum `catchNothing` (print "Error!!")

main = printMaybeNumWithErrorMsg someExpr

Т.е. мы опять таки вернулись к haskell-евскому error Это именно то, о чём я говорю — при использовании Maybe мы получим поведение error. Смысл?

(Это скорее для geniepro, а не для тебя)

Здравствуйте, lomeo, Вы писали:

L>Монада — это то, что использует операцию bind. А АТД это или нет, вопрос десятый.

И return

Здравствуйте, Аноним, Вы писали:

L>>Я имел в виду, что в тотал языке нет fromJust, а значит выйти из Maybe в общем случае невозможно.

А>вобще то выйти из Maybe можно при помощи maybe или fromMaybe

Да это-то понятно, просто это всё эквивалент ручного протаскивания исключения + обработка (случай maybe), минимальная обработка (случай fromMaybe) или выпускание его на волю (fromJust)... Это всё недостаточно универсально

Здравствуйте, lomeo, Вы писали:

L>Ну и разумеется, решение, которое предлагает Turner для организации бесконечного исполнения программ — отдельные codata. Мне это было не особо интересно, потому что подобная идея — явное разделение data и codata в дизайне языка — уже рассматривалась. По крайней мере, я помню, что в паре мест я точно про это читал.

Предложения-то предложениями, вопрос гдеж язык для tfp?

Здравствуйте, Курилка, Вы писали:

К>Предложения-то предложениями, вопрос гдеж язык для tfp?

Ща... дай только полчасика

Здравствуйте, Курилка, Вы писали:

Кстати, подумал, что в свете предложенных Тёрнером идей (не использовать head/tail, а только паттерн матчинг), проблем с эффективностью, подобных этой не будет.

Здравствуйте, lomeo, Вы писали:

L>Здравствуйте, Курилка, Вы писали:

L>Кстати, подумал, что в свете предложенных Тёрнером идей (не использовать head/tail, а только паттерн матчинг), проблем с эффективностью, подобных этой не будет.

Ммм, почему?

Здравствуйте, lomeo, Вы писали:

L>Здравствуйте, Курилка, Вы писали:

К>>Предложения-то предложениями, вопрос гдеж язык для tfp?

L>Ща... дай только полчасика

Кстати фишка — интерпретатор же нельзя будет написать для этого языка на нём самом, насколько я понимаю. Т.е. бутстрапинг идёт лесом или я что-то нпаутал?

Здравствуйте, Курилка, Вы писали:

К>Кстати фишка — интерпретатор же нельзя будет написать для этого языка на нём самом, насколько я понимаю. Т.е. бутстрапинг идёт лесом или я что-то нпаутал?

Интерпретатор нельзя, но я очень плохо этот момент понял. Там приводятся аналогии, но в целом я картину не вижу.

Здравствуйте, Курилка, Вы писали:

L>>Кстати, подумал, что в свете предложенных Тёрнером идей (не использовать head/tail, а только паттерн матчинг), проблем с эффективностью, подобных этой не будет.

К>Ммм, почему?

Потому что мы не сможем написать вариант с tail — такой функции просто нет.
Я имел в виду существующую в Haskell ситуацию — нормальный порядок редукции, энергичный паттерн матчинг.

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

Здравствуйте, lomeo, Вы писали:

К>>Предложения-то предложениями, вопрос гдеж язык для tfp?

L>Ща... дай только полчасика

И? А то я тоже почитал эту статью, а что дальше?

G>И? А то я тоже почитал эту статью, а что дальше?

Похоже, придётся учить Эпиграм и какой-то там Charity

Здравствуйте, geniepro, Вы писали:

G>Похоже, придётся учить Эпиграм и какой-то там Charity

Так точно, Charity. nontermination, data/codata, bottom нет.

Здравствуйте, lomeo, Вы писали:

L>Здравствуйте, geniepro, Вы писали:

G>>Похоже, придётся учить Эпиграм и какой-то там Charity

L>Так точно, Charity. nontermination, data/codata, bottom нет.

Кто-нибудь его вообще руками пробовал? Вон thesz говорит, что его синтаксис отпугнул
Тёрнер пишет о необходимости чего-нибудь юзабельного, но пока, судя по всему, эта ниша не занята.

Здравствуйте, 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 — как блин вытащить текущее значение, а не уже отфолденный результат, я так и не понял

Здравствуйте, lomeo, Вы писали:

L>Так прикол в том, что не надо придумывать

s/Так/Там/

Здравствуйте, lomeo, Вы писали:

L>Хотя, возможно, с практической точки зрения это неудобно. Может быть использовать его как целевой язык? Хотя тут проблемы с тем же fold — как блин вытащить текущее значение, а не уже отфолденный результат, я так и не понял

Так ана- и ката- этого вроде не позволяют. Параморфизм как раз и предназначен, чтобы "eats its argument and keeps it too". Это из первых бананов (которые с конвертами и колючей проволокой).

Здравствуйте, lomeo, Вы писали:

L>Здравствуйте, lomeo, Вы писали:

L>>Так прикол в том, что не надо придумывать отдельные правила

L>s/Так/Там/

Ну вот и вопрос — что удобнее? Явное разделение прям в тексте или по направлению стрелок.
Чисто интуитивно мне кажется, что прямо в тексте лучше, т.к. не надо "дополнительно" заглядывать в домены стрелок.
Хот по сути, насколько я понимаю, решения изоморфны, а интерпретирует человек, поэтому надо с этой стороны "копать"

Здравствуйте, deniok, Вы писали:

D>Здравствуйте, lomeo, Вы писали:

L>>Хотя, возможно, с практической точки зрения это неудобно. Может быть использовать его как целевой язык? Хотя тут проблемы с тем же fold — как блин вытащить текущее значение, а не уже отфолденный результат, я так и не понял

D>Так ана- и ката- этого вроде не позволяют. Параморфизм как раз и предназначен, чтобы "eats its argument and keeps it too". Это из первых бананов (которые с конвертами и колючей проволокой).

Ммм, сорри за ламерский вопрос, но бананы (параморфизм) и позволяют "повышать" уровень языка? (с т.зр. экспрессивности языка и теоремы Гёделя).
P.S. Наверное надо будет перечитать про все эти warm fuzzy things в смысле разные -морфизмы

Здравствуйте, Курилка, Вы писали:

К>Ммм, сорри за ламерский вопрос, но бананы (параморфизм) и позволяют "повышать" уровень языка? (с т.зр. экспрессивности языка и теоремы Гёделя).
К>P.S. Наверное надо будет перечитать про все эти warm fuzzy things в смысле разные -морфизмы

бананы — это ката

Здравствуйте, deniok, Вы писали:

D>Так ана- и ката- этого вроде не позволяют. Параморфизм как раз и предназначен, чтобы "eats its argument and keeps it too". Это из первых бананов (которые с конвертами и колючей проволокой).

Угу. Проблема в том, что пара- там как раз и нет.

Здравствуйте, Курилка, Вы писали:

К>Ну вот и вопрос — что удобнее? Явное разделение прям в тексте или по направлению стрелок.

Видимо, как посмотреть. С практической точки зрения (если рассматривать этот язык как инструмент для широкого применения) явное кажется посимпатичнее.

Здравствуйте, lomeo, Вы писали:

L>Здравствуйте, Курилка, Вы писали:

К>>Ммм, сорри за ламерский вопрос, но бананы (параморфизм) и позволяют "повышать" уровень языка? (с т.зр. экспрессивности языка и теоремы Гёделя).
К>>P.S. Наверное надо будет перечитать про все эти warm fuzzy things в смысле разные -морфизмы

L>бананы — это ката

А, сорри, недопонял смысла написаного, дак а что насчёт параморфизма?

Здравствуйте, Курилка, Вы писали:



К>Ммм, сорри за ламерский вопрос, но бананы (параморфизм) и позволяют "повышать" уровень языка? (с т.зр. экспрессивности языка и теоремы Гёделя).

Бананы — это ката-.
Линзы — это ана-.
А пара- — это колючая проволока.
Это всё разные примитивы (паттерны) рекурсии. Факториал "естественно" не записать как катаморфизм над Nat = Nil | Succ Nat. Параморфизм как раз об факториало-подобном паттерне.

Здравствуйте, lomeo, Вы писали:

L>Здравствуйте, Курилка, Вы писали:

К>>Ну вот и вопрос — что удобнее? Явное разделение прям в тексте или по направлению стрелок.

L>Видимо, как посмотреть. С практической точки зрения (если рассматривать этот язык как инструмент для широкого применения) явное кажется посимпатичнее.

А какие плюсы у "неявного"? Более общее решение, насколько я понимаю?

Здравствуйте, lomeo, Вы писали:

L>Здравствуйте, deniok, Вы писали:

D>>Так ана- и ката- этого вроде не позволяют. Параморфизм как раз и предназначен, чтобы "eats its argument and keeps it too". Это из первых бананов (которые с конвертами и колючей проволокой).

L>Угу. Проблема в том, что пара- там как раз и нет.
А. Пора свой язык делать?

Здравствуйте, Курилка, Вы писали:

К>Как-то странно, что на РСДН ещё не появилась ссылка о сабже. Там приводится очень интересная работа Тёрнера, раскрывающая тему терминируемости алгоритмов, приводится базовый язык, в котором чётко разделяется data как базис примитивных типов и codata как базис для структурной рекурсии. По сути он говорит, что даже haskell недостаточно строг (формален), т.к. допускает _|_ (bottom), однако эта нестрогость даёт достаточную свободу для решения практических задач, поэтому традиционное ФП он называет слабым, а искомую систему — сильным ФП (аналогично языкам со слабой и сильной системами типов).

Ещё мысль-вопрос в сторону: наличие НФ для терминируемой функции в итоге даёт возможность точно определить время выполнения функции, исходя из известного времени выполнения неких "примитивных" блоков (базиса языка). Я правильно всё понимаю?
Получаем, что фактически нам не нужны гипотетические O(n) становятся и мы можем гарантировать hard real-time, правда со скидкой на производительность и экспрессивность базиса (всёж неполное по Тьюрингу решение выходит)

Здравствуйте, deniok, Вы писали:

D>Здравствуйте, lomeo, Вы писали:
L>>Угу. Проблема в том, что пара- там как раз и нет.
D>А. Пора свой язык делать?

Вот и вопрос — имеет ли смысл за базис чарити брать?
Всёж подход Тёрнера мне кажется более вменяемым, но можно транслировать его в код на расширенном чарити...
Интерпретатор правда там на Сях
Имхо за базис Хаскель брать стоит его задницы мне более симпатичны

Здравствуйте, Курилка, Вы писали:

К>А какие плюсы у "неявного"? Более общее решение, насколько я понимаю?

Это почти язык ТК получается.

Здравствуйте, Курилка, Вы писали:

К>А, сорри, недопонял смысла написаного, дак а что насчёт параморфизма?

Нету его

Здравствуйте, Курилка, Вы писали:

К>Имхо за базис Хаскель брать стоит его задницы мне более симпатичны

Мы же, вроде, без задниц хотим. Не Тьюринг-полный, но со вшитыми паттернами для "правильных" рекурсий...

Блин, некогда Тернера дочитать, только первую половину прочёл в метро

Здравствуйте, deniok, Вы писали:

D>Здравствуйте, Курилка, Вы писали:

К>>Имхо за базис Хаскель брать стоит его задницы мне более симпатичны

D>Мы же, вроде, без задниц хотим. Не Тьюринг-полный, но со вшитыми паттернами для "правильных" рекурсий...

D>Блин, некогда Тернера дочитать, только первую половину прочёл в метро

Вот во второй половине "собака" и "порылась"
Суть в том, что целевой язык нам нужен без задниц, а вот интерпретатор (и компилятор, насколько я понимаю они изоморфны ), не может быть без задниц написан в следствие первой теоремы Гёделя о неполноте.
Это, к примеру причина того, что чарити не на чарити, ну и тех мыслей, что я про бутстраппинг приводил.

Здравствуйте, Курилка, Вы писали:

К>Вот и вопрос — имеет ли смысл за базис чарити брать?
К>Всёж подход Тёрнера мне кажется более вменяемым, но можно транслировать его в код на расширенном чарити...
К>Интерпретатор правда там на Сях
К>Имхо за базис Хаскель брать стоит его задницы мне более симпатичны

В смысле ты собираешься сделать такой язык? Отписывайся тогда плз...

Здравствуйте, Курилка, Вы писали:

К>Ещё мысль-вопрос в сторону: наличие НФ для терминируемой функции в итоге даёт возможность точно определить время выполнения функции, исходя из известного времени выполнения неких "примитивных" блоков (базиса языка). Я правильно всё понимаю?

Нет, мне кажется. То что у выражения есть НФ не говорит о том, как она достигается. Ведь reduction sequence нам заранее не известен.

Здравствуйте, lomeo, Вы писали:

L>Здравствуйте, Курилка, Вы писали:

К>>А, сорри, недопонял смысла написаного, дак а что насчёт параморфизма?

L>Нету его

Дак, то что нету это ясно.
Смотри, по Гёделю формальные алг. системы расширяются за счёт постулатов, выходящих за их рамки.
Получается что параморфизм есть пример подобного "выхода за рамки". Не се па?

Здравствуйте, lomeo, Вы писали:

L>Здравствуйте, Курилка, Вы писали:

К>>Ещё мысль-вопрос в сторону: наличие НФ для терминируемой функции в итоге даёт возможность точно определить время выполнения функции, исходя из известного времени выполнения неких "примитивных" блоков (базиса языка). Я правильно всё понимаю?

L>Нет, мне кажется. То что у выражения есть НФ не говорит о том, как она достигается. Ведь reduction sequence нам заранее не известен.

Ммм, а если задать "порядок редукции" (или как там ленивость обзывается правильно)?
Насколько я понимаю порядок тоже является морфизмом, правда параллели я с ходу боюсь проводить.

Здравствуйте, lomeo, Вы писали:

L>Здравствуйте, Курилка, Вы писали:

К>>Вот и вопрос — имеет ли смысл за базис чарити брать?
К>>Всёж подход Тёрнера мне кажется более вменяемым, но можно транслировать его в код на расширенном чарити...
К>>Интерпретатор правда там на Сях
К>>Имхо за базис Хаскель брать стоит его задницы мне более симпатичны

L>В смысле ты собираешься сделать такой язык? Отписывайся тогда плз...

Ну, скажем так, не исключаю такой возможности, про "отписывайся" — это подкол? (без смайла не всегда понятна интонация предложений )
А то фп-фп, а толку...
Хочется хоть чем-то помочь Родине

Здравствуйте, Курилка, Вы писали:

К>Ну, скажем так, не исключаю такой возможности, про "отписывайся" — это подкол? (без смайла не всегда понятна интонация предложений )
К>А то фп-фп, а толку...
К>Хочется хоть чем-то помочь Родине

Никакого смайла, просто если ты будешь рисовать, то пиши, что получается интересного в процессе — это всё, что я хотел сказать.
Мне будет очень интересно это почитать, пообсуждать.

Здравствуйте, Курилка, Вы писали:

К>Ммм, а если задать "порядок редукции" (или как там ленивость обзывается правильно)?
К>Насколько я понимаю порядок тоже является морфизмом, правда параллели я с ходу боюсь проводить.

Я не про порядок говорил, а про последовательность — она сильно зависит от данных и то, что в данном случае мы можем быть уверены в терминируемости никак не поможет нам в анализе сложности.

А порядок сам по себе здесь не особо важен — в любом случае НФ будет достигнута. Вопрос в том, как.

Здравствуйте, deniok, Вы писали:

D>Но в языке с ограниченным набором паттернов рекурсии и отделённой кодатой такая оценка возможна, нес па? Выгоды от Тьюринг-неполноты должны же быть?

Возможно, я просто не вижу, как её сделать. И потом я говорил не про паттерны рекурсии (типа ката-, ана-) — не про Charity, а про total language вообще — у Тёрнера это, например, структурная декомпозиция.

Не знаю, если честно. Надо подумать.

Здравствуйте, lomeo, Вы писали:

L>Здравствуйте, Курилка, Вы писали:

К>>Дак, то что нету это ясно.
К>>Смотри, по Гёделю формальные алг. системы расширяются за счёт постулатов, выходящих за их рамки.
К>>Получается что параморфизм есть пример подобного "выхода за рамки". Не се па?

L>Уи. Только, возможно, я просто чего то недоглядел в Charity.

L>Вот, кстати, нашёл книжку — буду читать
L>Categorical programming with inductive and coinductive types

L>Вот тут нашёл: http://www.cs.ut.ee/~varmo/papers/
L>Там ещё до кучи.

У, вкусно
Ещёб время на всё.
Кстати там же внутри система Мартина-Лёфа, помнится nponeccop давал ссылку на Programming in Martin-Lof’s Type Theory — An Introduction, правда тогда я ещё не догнал этого, а Тёрнер её приводит, так что думаю имеет смысл и туда глянуть. Кстати он же делает компилятор, правда ничего не слышно последнюю пару месяцев. Правда на перле и что-то он с комбинаторами мутил (а в комбинаторной логике я слабоват)

Здравствуйте, Курилка, Вы писали:

К>Думаю имеет смысл инициативную группу собрать, наверное на хугах в феврале стоит рассмотреть этот вопрос. Коллективный разум он помощнее будет, параллелизация понимаешь

В московскую я запостил, deniok — стукнешься в питерской, пожалуйста?

Здравствуйте, lomeo, Вы писали:

L>Здравствуйте, Курилка, Вы писали:

К>>Ммм, а если задать "порядок редукции" (или как там ленивость обзывается правильно)?
К>>Насколько я понимаю порядок тоже является морфизмом, правда параллели я с ходу боюсь проводить.

L>Я не про порядок говорил, а про последовательность — она сильно зависит от данных и то, что в данном случае мы можем быть уверены в терминируемости никак не поможет нам в анализе сложности.

Тогда можешь пояснить, что тут под последовательностью понимается?

L>А порядок сам по себе здесь не особо важен — в любом случае НФ будет достигнута. Вопрос в том, как.

Извини меня, но "как" по-моему не может не влиять на скорость (если ты в Питер через Владивосток поедешь, то есть подозрение, что это будет дольше чем напрямую, правда влияет ещё и механизм перемещения). Нам не нужна НФ. Считаем, что компилятор уже её сгенерил (пофигу каким образом). Речь о том, что передавая параметры мы в интерпретаторе мы получаем некую искомую НФ, в простейшем случае число (e.g. для вычисления факториала), хотя можно его в нумералах Чёрча изображать, тока нафиг?

Здравствуйте, deniok, Вы писали:

D>Здравствуйте, lomeo, Вы писали:

L>>Вот, кстати, нашёл книжку — буду читать
L>>Categorical programming with inductive and coinductive types

D>Это ж диссертация Varmo Vene, известный текст. Он в Тарту заведующий кафедрой. Мы в своё время долго мучались над языком его презентации, оказавшимся эстонским.

Коль ты знаешь его труды, то у него всё в греческих буквочках, практических вариантов нема?

Здравствуйте, Курилка, Вы писали:

К>Кстати там же внутри система Мартина-Лёфа, помнится nponeccop давал ссылку на Programming in Martin-Lof’s Type Theory — An Introduction, правда тогда я ещё не догнал этого, а Тёрнер её приводит, так что думаю имеет смысл и туда глянуть. Кстати он же делает компилятор, правда ничего не слышно последнюю пару месяцев. Правда на перле и что-то он с комбинаторами мутил (а в комбинаторной логике я слабоват)

Много слышал, не читал о Мартин-Лёф ТТ, надо наконец, воспольнить этот пробел. В ТТ разбирается palm_mute, надо его спросить.
Насчёт nponeccop-овского NH0 — то, насколько я понял он транслирует в комбинаторны (какие именно у него рассказыватся). Базис у него, неполный (K не напишешь), но он говорит, что это и не нужно в практических задачах. Смысл, насколько я понял в оптимизации типа суперкомпиляции, но я не уверен.

Здравствуйте, deniok, Вы писали:

D>Это ж диссертация Varmo Vene, известный текст. Он в Тарту заведующий кафедрой. Мы в своё время долго мучались над языком его презентации, оказавшимся эстонским.

А точно! У меня, кстати, такое ощущение было, что я этот текст уже листал. Но не читал, точно

Здравствуйте, Курилка, Вы писали:

К>Думаю имеет смысл инициативную группу собрать, наверное на хугах в феврале стоит рассмотреть этот вопрос. Коллективный разум он помощнее будет, параллелизация понимаешь

О, молодец! Хорошая идея.

Здравствуйте, Курилка, Вы писали:

К>Здравствуйте, Курилка, Вы писали:

К>>Думаю имеет смысл инициативную группу собрать, наверное на хугах в феврале стоит рассмотреть этот вопрос. Коллективный разум он помощнее будет, параллелизация понимаешь

К>В московскую я запостил, deniok — стукнешься в питерской, пожалуйста?
Да, только надо сформулировать

Здравствуйте, Курилка, Вы писали:

К>Тогда можешь пояснить, что тут под последовательностью понимается?

Исполнение программы — сначала эту редукцию выполняем, потом эту и так до НФ...

L>>А порядок сам по себе здесь не особо важен — в любом случае НФ будет достигнута. Вопрос в том, как.

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

НФ не генерится компилятором. НФ — это то, что мы получаем в результате исполнения программы. И, да, "как" влияет на скорость — я о том и говорил, погляди на выделенное в моем сообщении.

К>Речь о том, что передавая параметры мы в интерпретаторе мы получаем некую искомую НФ, в простейшем случае число (e.g. для вычисления факториала), хотя можно его в нумералах Чёрча изображать, тока нафиг?

Попробую пояснить свою мысль. Значит, мы доходим до НФ в результате исполнения программы. От выбора порядка редукции, разумеется, зависит то, какой будет последовательность этих редукций (исполнение программы). Но сам по себе порядок не важен — просто, зная его, мы знаем, что будет редуцировано на следующем шаге при конкретных данных. Так вот, моя мысль была в том, что автоматический анализ того, какая будет последовательность — сложен. Т.е. "возможность возможность точно определить время выполнения функции" может у нас и есть, только она уж очень теоретическая IMHO.

Но моё "нет" там слишком категорическое. Я погорячился. Надо подумать.

Здравствуйте, lomeo, Вы писали:

Кстати, получение факториала в терминах initial F-алгебры сводится таким образом к получению списка [1..n]. Или, если добавить сюда terminal F-коалгебру, к получению функции типа nat * inflist(A) -> list(A), получающий список первых N элементов бесконечного списка.

Я тут попробовал и честно написать такое у меня не получается. Есть идеи?

Здравствуйте, deniok, Вы писали:

D>Здравствуйте, Курилка, Вы писали:

К>>Здравствуйте, Курилка, Вы писали:

К>>>Думаю имеет смысл инициативную группу собрать, наверное на хугах в феврале стоит рассмотреть этот вопрос. Коллективный разум он помощнее будет, параллелизация понимаешь

К>>В московскую я запостил, deniok — стукнешься в питерской, пожалуйста?
D>Да, только надо сформулировать

Ну можно какую-нибудь Хартию Священного Таинства Стрелок замутить, но сейчас некогда, сорри

Здравствуйте, lomeo, Вы писали:

L>Здравствуйте, Курилка, Вы писали:

К>>Тогда можешь пояснить, что тут под последовательностью понимается?

L>Исполнение программы — сначала эту редукцию выполняем, потом эту и так до НФ...

Это лишь одна редукция
На самом деле их 2, правда может быть и больше, но для начала надо 2 сделать

L>>>А порядок сам по себе здесь не особо важен — в любом случае НФ будет достигнута. Вопрос в том, как.

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

L>НФ не генерится компилятором. НФ — это то, что мы получаем в результате исполнения программы. И, да, "как" влияет на скорость — я о том и говорил, погляди на выделенное в моем сообщении.

Вот тут у нас разногласие в понимании. Компилятор берёт терм на языке пользователя, там остаются параметры, этот терм даёт НФ со свободными параметрами это даёт экзешник. Экзешник же подстановкой параметров даёт НФ на выходе, в нужном базисе.

К>>Речь о том, что передавая параметры мы в интерпретаторе мы получаем некую искомую НФ, в простейшем случае число (e.g. для вычисления факториала), хотя можно его в нумералах Чёрча изображать, тока нафиг?

L>Попробую пояснить свою мысль. Значит, мы доходим до НФ в результате исполнения программы. От выбора порядка редукции, разумеется, зависит то, какой будет последовательность этих редукций (исполнение программы). Но сам по себе порядок не важен — просто, зная его, мы знаем, что будет редуцировано на следующем шаге при конкретных данных. Так вот, моя мысль была в том, что автоматический анализ того, какая будет последовательность — сложен. Т.е. "возможность возможность точно определить время выполнения функции" может у нас и есть, только она уж очень теоретическая IMHO.

L>Но моё "нет" там слишком категорическое. Я погорячился. Надо подумать.

Сложности нехилые, согласен. Вопрос — что делать со свободными параметрами...
Но вот принципиальных проблем я не вижу

Здравствуйте, Курилка, Вы писали:

К>Вот тут у нас разногласие в понимании. Компилятор берёт терм на языке пользователя, там остаются параметры, этот терм даёт НФ со свободными параметрами это даёт экзешник. Экзешник же подстановкой параметров даёт НФ на выходе, в нужном базисе.

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

Здравствуйте, lomeo, Вы писали:

L>Здравствуйте, Курилка, Вы писали:

К>>Вот тут у нас разногласие в понимании. Компилятор берёт терм на языке пользователя, там остаются параметры, этот терм даёт НФ со свободными параметрами это даёт экзешник. Экзешник же подстановкой параметров даёт НФ на выходе, в нужном базисе.

L>Ну поскольку мы говорили о сложности программы, я даже как-то не думал, что ты говоришь о компиляторе

Дак, блин тут вся и сложность — когда есть несколько слоёв абстракций, то порой путаница в каком слое находишься, так-то кругом одни стрелки

На дружественном сайте я затеял обcуждение проблем TFP, там, правда, функциональщиков мало, а тема интересная, но тут она почему-то заглохла... Может продолжим? (Там или тут -- не важно...)

Здравствуйте, geniepro, Вы писали:

G>На дружественном сайте я затеял обcуждение проблем TFP, там, правда, функциональщиков мало, а тема интересная, но тут она почему-то заглохла... Может продолжим? (Там или тут -- не важно...)

Может тогда всё таки тут?

Там читать неудобно — снизу-вверх и выискивать ветки, устал

Здравствуйте, lomeo, Вы писали:

L>Может тогда всё таки тут?

Давайте тут.

Я вот прихожу постепенно к выводу, что Total FP в удобном (юзабельном) виде -- это фантастика. В смысле -- невозможно.

Нет, можно, конечно, обрезать Хаскелл по самый bottom, что бы убрать всю нетотальность, однако...

Total FP, как я понял, ориентирован на математической индукции, которая работает только на натуральных числах, и на списочной индукции. Отсюда два важных ограничения -- родными для TFP будут натуральные числа (с двумя операциями + и *) и конечные списки.
То есть об удобной работе с вещественными числами (а возможно даже и с отрицательными целыми), похоже, придётся забыть, и некоторые удобные приёмы, связанные с ленивыми бесконечными списками, тоже отпадут. (Правда, я плохо знаю всякие там коданные/косписки/комонады/корекурсии/ко.....)

Так что же получается? Стоит ли Total FP того, что бы с ним заморачиваться?
Даёт ли гарантированная останавливаемость функций достаточно бенефитов, что бы оправдать кучу неудобств?

Здравствуйте, geniepro, Вы писали:

G>Здравствуйте, lomeo, Вы писали:

L>>Может тогда всё таки тут?

G>Давайте тут.

Я ещё в ру_лямбду всё собираюсь написать, а воз и ныне там.

G>Я вот прихожу постепенно к выводу, что Total FP в удобном (юзабельном) виде -- это фантастика. В смысле -- невозможно.
Ну если так подходить, то Хаскель невозможен в принципе
И машины Тьюринга тоже не существует — у нас ведь нет бесконечной ленты.

G>Нет, можно, конечно, обрезать Хаскелл по самый bottom, что бы убрать всю нетотальность, однако...

Ты видел у lomeo про :k (->) ?

G>Total FP, как я понял, ориентирован на математической индукции, которая работает только на натуральных числах, и на списочной индукции. Отсюда два важных ограничения -- родными для TFP будут натуральные числа (с двумя операциями + и *) и конечные списки.
G>То есть об удобной работе с вещественными числами (а возможно даже и с отрицательными целыми), похоже, придётся забыть, и некоторые удобные приёмы, связанные с ленивыми бесконечными списками, тоже отпадут. (Правда, я плохо знаю всякие там коданные/косписки/комонады/корекурсии/ко.....)
Есть ощущение — зря что не знаешь. (бесконечные списки реализуются вродь как "в лёт")
Про вещественные числа имхо — решаемая задача, хотяб можно с фиксированной запятой обойтись, если задача позволяет, с плавающей судить не берусь.

G>Так что же получается? Стоит ли Total FP того, что бы с ним заморачиваться?
G>Даёт ли гарантированная останавливаемость функций достаточно бенефитов, что бы оправдать кучу неудобств?
Про кучу неудобств — спорно.
Имхо надо решать исходя из задачи, или у тебя все задачи решаются только на C++ (можно подставить VB/Java/PHP и др. по желанию)?
Кстати хоть аналогии и зло, но вот как ты считаешь — монады стоят того, чтобы с ними заморачиваться?

Здравствуйте, lomeo, Вы писали:

L>Что касается вещественных чисел, то это просто вопрос, с которым надо разобраться. Возможно, там можно принять какое то практические решение. В конце концов не считать некоторые функции гарантировано завершимыми. Это и вопрос с bottom мне, если честно, интересен не так как структурная рекурсия, например, или вывод гарантии завершимости.

Можно пояснить последнее предложение? Толи ты знаки пунктуации странно расставил, толи я сильно туплю...

Здравствуйте, Курилка, Вы писали:

L>>Что касается вещественных чисел, то это просто вопрос, с которым надо разобраться. Возможно, там можно принять какое то практические решение. В конце концов не считать некоторые функции гарантировано завершимыми. Это и вопрос с bottom мне, если честно, интересен не так как структурная рекурсия, например, или вывод гарантии завершимости.

К>Можно пояснить последнее предложение? Толи ты знаки пунктуации странно расставил, толи я сильно туплю...



Мне малоинтересны вопросы: 1. полное (по всему языку) тотал фп; 2. отсутствие задницы.
Мне многоинтересны вопросы: 1. структурная рекурсия; 2. гаранитии завершимости.

Здравствуйте, lomeo, Вы писали:

L>Здравствуйте, Курилка, Вы писали:

L>>>Что касается вещественных чисел, то это просто вопрос, с которым надо разобраться. Возможно, там можно принять какое то практические решение. В конце концов не считать некоторые функции гарантировано завершимыми. Это и вопрос с bottom мне, если честно, интересен не так как структурная рекурсия, например, или вывод гарантии завершимости.

К>>Можно пояснить последнее предложение? Толи ты знаки пунктуации странно расставил, толи я сильно туплю...

L>

L>Мне малоинтересны вопросы: 1. полное (по всему языку) тотал фп; 2. отсутствие задницы.
L>Мне многоинтересны вопросы: 1. структурная рекурсия; 2. гаранитии завершимости.

Точно — теперь прочёл и дошло.
А я вот думаю, что можно получить и то и другое
Правда хз как.
Первоначальная идея — _|_ для даты будет 1 для кодаты, и наоборот (1 для даты будет _|_ для кодаты). Как гипотезу я сегодня это уже в топике про ЛИ vs ЛИСП писал, правда там вместо даты/кодаты нетипизированное и типизированное ЛИ (а роль 1/_|_ играет наличие НФ у терма).
Есть ощущение, что моя гипотеза тоже может попасть в копилку "недоказуемых" (т.е. в _|_ )

Здравствуйте, Курилка, Вы писали:

K> Ты видел у lomeo про :k (->) ?

Честно говоря, не помню.
GHCi забавный ответ даёт на этот запрос... :о)

К> Кстати хоть аналогии и зло, но вот как ты считаешь — монады стоят того, чтобы с ними заморачиваться?

Даже не знаю, я всё никак не выделю время для заморочек с монадами... :о)

Здравствуйте, lomeo, Вы писали:

L> Если список бесконечен, то это кодата.

Нет ли где внятного описания всей этой кухни?
Что-то мне кажется, что бесконечные косписки в TFP -- это что-то вроде монадического ввода/вывода в Хаскелле... Такой же хак по сравнению с основной идеологией...

L> Что касается вещественных чисел, то это просто вопрос, с которым надо разобраться. Возможно, там можно принять какое то практические решение. В конце концов не считать некоторые функции гарантировано завершимыми.

Если не будет гарантированной завершимости, то не будет и Total FP.
Более практичным, например, будет признание того, что некоторые функции могут быть определены частично, и поэтому их результаты должны быть упакованы в Maybe.
С делением на ноль -- предложение Тёрнера (x/0 == x) мне кажется сомнительным. Также, что делать с log(0)? Такие функции лучше обернуть в Maybe...

L> Это и вопрос с bottom мне, если честно, интересен не так как структурная рекурсия, например, или вывод гарантии завершимости.

Вывод гарантии завершимости -- это, по сути, вывод отстутствия bottom. Как можно интересоваться одним и игнорировать другое, если они друг через друга определяются?

Здравствуйте, geniepro, Вы писали:

G>Здравствуйте, lomeo, Вы писали:

L>> Если список бесконечен, то это кодата.

G>Нет ли где внятного описания всей этой кухни?
G>Что-то мне кажется, что бесконечные косписки в TFP -- это что-то вроде монадического ввода/вывода в Хаскелле... Такой же хак по сравнению с основной идеологией...
Монады нифига не хак, хак это unsafePerformIO, который в монаду IO запрятан по сути...

L>> Что касается вещественных чисел, то это просто вопрос, с которым надо разобраться. Возможно, там можно принять какое то практические решение. В конце концов не считать некоторые функции гарантировано завершимыми.

G>Если не будет гарантированной завершимости, то не будет и Total FP.
+1
G>Более практичным, например, будет признание того, что некоторые функции могут быть определены частично, и поэтому их результаты должны быть упакованы в Maybe.
G>С делением на ноль -- предложение Тёрнера (x/0 == x) мне кажется сомнительным. Также, что делать с log(0)? Такие функции лучше обернуть в Maybe...
тыж вроде монады не разобрал ещё?
По поводу делений на 0 логарифмов от 0 и т.п. — по моему эти случаи "идут лесом". Тотальное ФП потому и даёт гарантии, что входные программы ограничиваются. Можно ли обойтись без них — не знаю. По сути Тёрнер же говорит, что в качестве чисел надо Nat использовать. Также пойдут лесом иррациональные числа и непонятно что делать с приближёнными вычислениями.
Хотя тут есть интересный пункт — если результатом функции в ТФП является кодата, то мы получим по идее _|_, а если дата — то гарантию завершения и конкр. результат.
Только вот как будут работать серверные программы, для которых _|_ есть нормальное поведение (т.к. бесконечный цикл должен быть), я пока чтот "не догоняю".

L>> Это и вопрос с bottom мне, если честно, интересен не так как структурная рекурсия, например, или вывод гарантии завершимости.

G>Вывод гарантии завершимости -- это, по сути, вывод отстутствия bottom. Как можно интересоваться одним и игнорировать другое, если они друг через друга определяются?
+1

Здравствуйте, Курилка, Вы писали:

К>Первоначальная идея — _|_ для даты будет 1 для кодаты, и наоборот (1 для даты будет _|_ для кодаты).

Поясни, или дай ссылку на то, где писал, а то я сходу не пойму о чём речь.

Здравствуйте, geniepro, Вы писали:

L>> Если список бесконечен, то это кодата.

G>Нет ли где внятного описания всей этой кухни?

Теория категорий?

http://sigfpe.blogspot.com/2007/07/data-and-codata.html
Был ещё хороший пост у кого то про codata и corecursion. Не могу к сожалению найти.

G>Что-то мне кажется, что бесконечные косписки в TFP -- это что-то вроде монадического ввода/вывода в Хаскелле... Такой же хак по сравнению с основной идеологией...

Ничего не понимаю, но пусть будет, как ты скажешь

G>Если не будет гарантированной завершимости, то не будет и Total FP.

Он будет total для подмножества функций.

G>Более практичным, например, будет признание того, что некоторые функции могут быть определены частично, и поэтому их результаты должны быть упакованы в Maybe.

А ни один фиг — error или Maybe? Единственное отличие, которое я вижу, это то, что в случае с Maybe мы должны всё делать явно. Это и преимущества (бьём по рукам для деления на ноль) и недостатки (с практической точки зрения это тихий ужас). А так — reasoning будет таким одинаково сложным.

G>С делением на ноль -- предложение Тёрнера (x/0 == x) мне кажется сомнительным. Также, что делать с log(0)? Такие функции лучше обернуть в Maybe...

Ну и будет, что однажды зайдя в Maybe мы уже из него не выйдем, т.е. используя в своей функции функцию с Maybe типом, мы обязаны также вернуть Maybe, ну так чем это отличается от поведения error?

G>Вывод гарантии завершимости -- это, по сути, вывод отстутствия bottom. Как можно интересоваться одним и игнорировать другое, если они друг через друга определяются?

Перефразирую. Меня мало интересует тотальное отсутствие bottom, достаточно группы функций, про которые я могу быть уверен в их завершимости. Пойдёт?

Здравствуйте, lomeo, Вы писали:


L>Перефразирую. Меня мало интересует тотальное отсутствие bottom, достаточно группы функций, про которые я могу быть уверен в их завершимости. Пойдёт?

А как их маркировать? Грязь прячем в IO, невозможность полного паттерн матчинга — в Maybe (ну можем, по крайней мере, если не хотим error), а отсутствие гарантий завершаемости?

Здравствуйте, deniok, Вы писали:

D>Здравствуйте, lomeo, Вы писали:


L>>Перефразирую. Меня мало интересует тотальное отсутствие bottom, достаточно группы функций, про которые я могу быть уверен в их завершимости. Пойдёт?

D>А как их маркировать? Грязь прячем в IO, невозможность полного паттерн матчинга — в Maybe (ну можем, по крайней мере, если не хотим error), а отсутствие гарантий завершаемости?

В том и фишка — ничего мы не прячем, совсем!
Только это ограничивает набор входных программ, иначе никак.

Здравствуйте, lomeo, Вы писали:

L>Здравствуйте, Курилка, Вы писали:

К>>Первоначальная идея — _|_ для даты будет 1 для кодаты, и наоборот (1 для даты будет _|_ для кодаты).

L>Поясни, или дай ссылку на то, где писал, а то я сходу не пойму о чём речь.

Чтот найти не могу, в общем идея какая — типизированное ЛИ ты можешь написать на нетипизированном (что ты вроде как и сделал) и наоборот. Написать же обе можно лишь на языке, который будет противоречивым, к примеру на хаскеле с _|_ или, как Charity, на C (с другими проблеммами). В итоге мы нарвёмся или на зацикливание (хотя выполнимая в ТФП фунция такого не сделает) или на ограничения по времени/объёму памяти.
Я понимаю, что аналогия с датой/кодатой фиговая, но вот такая идея.

Здравствуйте, Курилка, Вы писали:

К>Здравствуйте, lomeo, Вы писали:

L>>Здравствуйте, Курилка, Вы писали:

К>>>Первоначальная идея — _|_ для даты будет 1 для кодаты, и наоборот (1 для даты будет _|_ для кодаты).

L>>Поясни, или дай ссылку на то, где писал, а то я сходу не пойму о чём речь.

К>Чтот найти не могу, в общем идея какая — типизированное ЛИ ты можешь написать на нетипизированном (что ты вроде как и сделал) и наоборот. Написать же обе можно лишь на языке, который будет противоречивым, к примеру на хаскеле с _|_ или, как Charity, на C (с другими проблеммами). В итоге мы нарвёмся или на зацикливание (хотя выполнимая в ТФП фунция такого не сделает) или на ограничения по времени/объёму памяти.
К>Я понимаю, что аналогия с датой/кодатой фиговая, но вот такая идея.

Ты, когда говоришь про типизированную лямбду, какую вершину лямбда-куба имеешь в виду? Потому что в язычке интерпретатора lomeo типизация ad hoc, простенькая и для одной утилитарной цели — удобства построения интерпретатора.

Здравствуйте, Курилка, Вы писали:

К>Чтот найти не могу, в общем идея какая — типизированное ЛИ ты можешь написать на нетипизированном (что ты вроде как и сделал) и наоборот.

Я сделал нетипизированное на нетипизированном

К>Написать же обе можно лишь на языке, который будет противоречивым, к примеру на хаскеле с _|_ или, как Charity, на C (с другими проблеммами). В итоге мы нарвёмся или на зацикливание (хотя выполнимая в ТФП фунция такого не сделает) или на ограничения по времени/объёму памяти.

Да, типизированное ЛИ (если имеется в виду simply-typed, без fix) невозможно написать на нём самом.

К>Я понимаю, что аналогия с датой/кодатой фиговая, но вот такая идея.

Я просто её вообще не вижу

Здравствуйте, deniok, Вы писали:

D>А как их маркировать? Грязь прячем в IO, невозможность полного паттерн матчинга — в Maybe (ну можем, по крайней мере, если не хотим error), а отсутствие гарантий завершаемости?

Не знаю пока. Использованием только data в параметрах, например. Вещественное число не является data, и его использование в функции делает функцию не тотальной (не проверяемой на тотальность). Или специальным ключевым словом, которое будет включать анализ на тотальность.

Да и дело не в маркировке, а в том, что автоматический анализ позволит нам точно узнать какие функции терминируемы.

Здравствуйте, deniok, Вы писали:

D>Здравствуйте, Курилка, Вы писали:

К>>Чтот найти не могу, в общем идея какая — типизированное ЛИ ты можешь написать на нетипизированном (что ты вроде как и сделал) и наоборот. Написать же обе можно лишь на языке, который будет противоречивым, к примеру на хаскеле с _|_ или, как Charity, на C (с другими проблеммами). В итоге мы нарвёмся или на зацикливание (хотя выполнимая в ТФП фунция такого не сделает) или на ограничения по времени/объёму памяти.
К>>Я понимаю, что аналогия с датой/кодатой фиговая, но вот такая идея.

D>Ты, когда говоришь про типизированную лямбду, какую вершину лямбда-куба имеешь в виду? Потому что в язычке интерпретатора lomeo типизация ad hoc, простенькая и для одной утилитарной цели — удобства построения интерпретатора.

Если честно — не готов сказать. Да и не уверен, что это тут принципиально. Я ведь не выдвигаю стройную теорию, а лишь озвучиваю свою идею, не более того.

Здравствуйте, Курилка, Вы писали:

G>> Такие функции лучше обернуть в Maybe...

K> тыж вроде монады не разобрал ещё? ???

А при чём здесь монады? ???
Я имел в виду обычный АлгТД Maybe a, у которого два варианта -- допустимое значение (Just a) и отсутствие такового (Nothing).
Вообще-то, для математических pertial-функций можно ввести спецтип, который будет включать PositiveInfinity, NegativeInfinity, Invalide, Valide...
Тогда:

1/0            == PositiveInfinity
(-1)/0         == NegativeInfinity
log 0          == NegativeInfinity, 
log (-1)       == Invalide
log (-1 :+ 0)  == Valide (0 :+ pi)
sqrt (-1)      == Invalide
sqrt (-1 :+ 0) == Valide (0 :+ 1)

ну и т.д...

Здравствуйте, geniepro, Вы писали:

G>Вообще-то, для математических pertial-функций можно ввести спецтип, который будет включать PositiveInfinity, NegativeInfinity, Invalide, Valide...
G>Тогда:
G>

1/0            == PositiveInfinity
G>(-1)/0         == NegativeInfinity
G>log 0          == NegativeInfinity, 
G>log (-1)       == Invalide
G>log (-1 :+ 0)  == Valide (0 :+ pi)
G>sqrt (-1)      == Invalide
G>sqrt (-1 :+ 0) == Valide (0 :+ 1)
G>

ну и т.д...

Уже

GHCi, version 6.8.1: http://www.haskell.org/ghc/  :? for help
Loading package base ... linking ... done.
Prelude> 1/0
Infinity
Prelude> -1/0
-Infinity
Prelude> log 0
-Infinity

Здравствуйте, lomeo, Вы писали:

L> Ну и будет, что однажды зайдя в Maybe мы уже из него не выйдем, т.е. используя в своей функции функцию с Maybe типом, мы обязаны также вернуть Maybe, ну так чем это отличается от поведения error?

Вовсе не обязательно, это ведь не монада IO... ;о)

Допустим, у нас есть некая функция, результат которой зависит от, например, операции деления, которая на некоторых параметрах этой функции даёт бесконечность.
В зависимости от наших задач у нас есть два варианта:
1) засунуть результат такой функции в Maybe;
2) принять в качестве деления на ноль какое-то дефолтное значение, а результат всей функции считать по-любому нормальным числом.

Здравствуйте, deniok, Вы писали:

Ага, но:

Prelude> 1 `div` 0
*** Exception: divide by zero

Prelude> 0 * log 0
NaN

чорт, а вот про log 0 у GHC я не знал... 8-о

Здравствуйте, geniepro, Вы писали:

G>чорт, а вот про log 0 у GHC я не знал... 8-о

Я и сам только что узнал

Здравствуйте, geniepro, Вы писали:
Эхех... "Всё уже придумано до нас!" :lol:

Prelude> :module +Complex

Prelude Complex> log (-1)
NaN

Prelude Complex> log ((-1) :+ 0)
0.0 :+ 3.141592653589793

Prelude Complex> sqrt (-1)
NaN

Prelude Complex> sqrt ((-1) :+ 0)
0.0 :+ 1.0

Здравствуйте, geniepro, Вы писали:

G>Здравствуйте, Курилка, Вы писали:

G>>> Такие функции лучше обернуть в Maybe...

K>> тыж вроде монады не разобрал ещё? ???

G>А при чём здесь монады? ???
G>Я имел в виду обычный АлгТД Maybe a, у которого два варианта -- допустимое значение (Just a) и отсутствие такового (Nothing).
Ага, читаем вики хотябы.
Ёжики кололись, плевались, но не понимали, что использовали монады
В том и суть монад, что так-то это вроде как обычный АлгТД
(хотя тут могу врать, т.к. не знаю точного мат. смысла термина "обычный АлгТД")

Здравствуйте, lomeo, Вы писали:

L>Здравствуйте, Курилка, Вы писали:

G>>>А при чём здесь монады? ???
G>>>Я имел в виду обычный АлгТД Maybe a, у которого два варианта -- допустимое значение (Just a) и отсутствие такового (Nothing).
К>>Ага, читаем вики хотябы.
К>>Ёжики кололись, плевались, но не понимали, что использовали монады
К>>В том и суть монад, что так-то это вроде как обычный АлгТД
К>>(хотя тут могу врать, т.к. не знаю точного мат. смысла термина "обычный АлгТД")

L>АТД — это сумма произведений, или дизъюнкция конъюнкций
Ну да, любой первоклассник это поймёт

L>А суть монад в том, чтобы связывать вычисления. Если мы используем fromJust для Maybe вычисления — это уже не монадическое использование и говорить тут о монадах бессмысленно. Если же (как в ТФП) fromJust вещь запрещённая, то нам приходится протягивать значения до конца, т.е. мы получим связку типа Maybe a -> (a -> Maybe b) -> Maybe b — это уже монада.

Т.е. ты считаешь что Монада не может являться АТД? Почему? Или я опять что-то неправильно понял?

Здравствуйте, Курилка, Вы писали:

К>Т.е. ты считаешь что Монада не может являться АТД? Почему? Или я опять что-то неправильно понял?

Неправильно

Монада — это то, что использует операцию bind. А АТД это или нет, вопрос десятый.

Здравствуйте, lomeo, Вы писали:

L>Здравствуйте, Курилка, Вы писали:

К>>Т.е. ты считаешь что Монада не может являться АТД? Почему? Или я опять что-то неправильно понял?

L>Неправильно

L>Монада — это то, что использует операцию bind. А АТД это или нет, вопрос десятый.

Ну значит Maybe и то и другое, а geniepro на неё (него?) посмотрел как на АТД, а я(ты?) как на монаду.
В общем — peace

Здравствуйте, lomeo, Вы писали:

L>Э-э-э.. Не понял при чём тут IO.

Ну в смысле, что если в IO попадёшь, то хрен оттуда выберешся (учитывая, что в стандарте Хаскелл-98 нет unsafePerformIO)...

L>Недостаток первого варианта я описал: однажды зайдя в Maybe, мы из него не выйдем.

Почему?

L>Недостаток второго: неестественность некоторых результатов операций (как деление на 0, например), которая может привести к ошибкам в логике. Но тут я не поручусь — надо почитать как Runciman разбирается с этой проблемой.

Рунсиман предлагает два варианта: либо x/0=x, либо x/0=infinity, где infinity=1+infinity
Первый вариант неестественнен, второй запрещён в TFP...

Здравствуйте, lomeo, Вы писали:

L> Если же (как в ТФП) fromJust вещь запрещённая, то нам приходится протягивать значения до конца, т.е. мы получим связку типа Maybe a -> (a -> Maybe b) -> Maybe b — это уже монада.

Ладно, к чёрту Maybe, забудем об этом типе, что бы не съезжать не туда из-за ненужных ассоциаций...
И fromJust тоже туда же, в (_|_)...

Создадим новый, простенький тип MathResult:

data MathResult a = Invalid | Valid a

L> Простой пример:
L> (/) :: (Num n) => n -> n -> Maybe n

L> Допустим мы считаем силу притяжения:
L> g * (m1 * m2) / (r^2)

Можно поступить не только так (Ваш пример не показателен, примем, например, расчёт корней кв. ур.):

class Num n where
    (+), (-), (*) :: n -> n -> n

class (Num n) => Floating n where
    (/)  :: n -> n -> MathResult n
    sqrt :: n -> MathResult n

roots :: Double -> Double -> Double -> (MathResult Double, MathResult Double)
roots a b c = (x1, x2)
  where
    d = sqrt (b*b - 4*a*c)
    e = 1 / (2*a)
    (x1, x2) = case d of
                 Invalid -> (Invalid, Invalid)
                 Valid d -> case e of
                              Invalid -> (Invalid, Invalid)
                              Valid e -> (Valid (((-b)+d)/e), Valid (((-b)-d)/e))

Ужос получился. :о))
Вапще-то в данной задаче другого варианта поведения вроде как и не предусмотрено, а более подходящего примера в голову не идёт, блин...
Однако предположим, что задача позволяет подставлять вместо d и e какие-то дефолтные значения в случае их невалидности. Тогда эта функция вполне может вернуть не MathResult Double, а просто Double... Неужели так трудно представить такой вариант?

Здравствуйте, Курилка, Вы писали:

К> Ну значит Maybe и то и другое, а geniepro на неё (него?) посмотрел как на АТД, а я(ты?) как на монаду.

В Хаскелле Maybe -- это обычнейший АлгТД, для которого просто-напросто реализовали в Prelude инстанс класса Monad, добавив ему монадных операций... Пользоваться или не пользоваться этими операциями -- личное дело каждого... :о)
Maybe -- не только монада, но ещё и функтор... ;о)

-- Maybe type

data  Maybe a  =  Nothing | Just a      deriving (Eq, Ord, Read, Show)

maybe              :: b -> (a -> b) -> Maybe a -> b
maybe n f Nothing  =  n
maybe n f (Just x) =  f x

instance  Functor Maybe  where
    fmap f Nothing    =  Nothing
    fmap f (Just x)   =  Just (f x)
        
instance  Monad Maybe  where
    (Just x) >>= k   =  k x
    Nothing  >>= k   =  Nothing
    return           =  Just
    fail s           =  Nothing

Вот, кстати, даже с Maybe можно делать вычисления с дефолтным результатом для невалидных аргументов... ;о)

А интересно, монаду Either никто не делал? И есть ли смысл? :о)

Здравствуйте, geniepro, Вы писали:

G>А интересно, монаду Either никто не делал? И есть ли смысл? :о)

У Either kind неподходящий для монады, слишком много типовых параметров (Either a b, целых две штуки). Можно, например, так:

instance Monad (Either String) where
 ...

и в String пихать сообщение об ошибке...

Здравствуйте, geniepro, Вы писали:

G>Можно поступить не только так (Ваш пример не показателен, примем, например, расчёт корней кв. ур.):

G>

G>roots :: Double -> Double -> Double -> (MathResult Double, MathResult Double)
G>roots a b c = (x1, x2)
G>  where
G>    d = sqrt (b*b - 4*a*c)
G>    e = 1 / (2*a)
G>    (x1, x2) = case d of
G>                 Invalid -> (Invalid, Invalid)
G>                 Valid d -> case e of
G>                              Invalid -> (Invalid, Invalid)
G>                              Valid e -> (Valid (((-b)+d)/e), Valid (((-b)-d)/e))
G>

G>Ужос получился. :о))

Это именно то, что получилось и у меня Ужасом я бы это не назвал, но удобства от такого использования мало, а если скрыть все эти валид/инвалид, как это сделано у меня, то получим тот же error:

roots :: MathResult Double -> MathResult Double -> MathResult Double -> (MathResult Double, MathResult Double)
roots a b c = (x1, x2)
  where
    d = sqrt (b*b - 4*a*c)
    e = 1 / (2*a)
    (x1, x2) = (((-b)+d)/e, ((-b)-d)/e)

G>Вапще-то в данной задаче другого варианта поведения вроде как и не предусмотрено, а более подходящего примера в голову не идёт, блин...

Увы,

G>Однако предположим, что задача позволяет подставлять вместо d и e какие-то дефолтные значения в случае их невалидности. Тогда эта функция вполне может вернуть не MathResult Double, а просто Double... Неужели так трудно представить такой вариант?

Вполне. Но мы же хотим нарисовать арифметику для тотального языка, а значит нам надо рассмотреть все классы задач. Задачи с дефолтными значениями являются всего лишь подмножеством задач с MathResult как error, вот комбинатор (аналогичный fromMaybe):

withDefault :: Num n => n -> MathResult n -> n
withDefault n Invalid   = n
withDefault _ (Valid n) = n

Обратное, в общем то, неверно.

Здравствуйте, geniepro, Вы писали:

L>>Э-э-э.. Не понял при чём тут IO.

G>Ну в смысле, что если в IO попадёшь, то хрен оттуда выберешся (учитывая, что в стандарте Хаскелл-98 нет unsafePerformIO)...

L>>Недостаток первого варианта я описал: однажды зайдя в Maybe, мы из него не выйдем.

G>Почему?

Потому что в стандарте тотал языка-08 нет fromJust (аналогичный unsafePerformIO).

Можно вытащить дефолтный параметр, но это очень специфично — зависит от задачи, т.е. как универсальное решение не проходит.

L>>Недостаток второго: неестественность некоторых результатов операций (как деление на 0, например), которая может привести к ошибкам в логике. Но тут я не поручусь — надо почитать как Runciman разбирается с этой проблемой.

G>Рунсиман предлагает два варианта: либо x/0=x, либо x/0=infinity, где infinity=1+infinity
G>Первый вариант неестественнен, второй запрещён в TFP...

Вот-вот.

Здравствуйте, lomeo, Вы писали:

L>Потому что в стандарте тотал языка-08 нет fromJust (аналогичный unsafePerformIO).

А что такое "стандарт тотал языка-08"?

Здравствуйте, Курилка, Вы писали:

L>>Потому что в стандарте тотал языка-08 нет fromJust (аналогичный unsafePerformIO).

К>А что такое "стандарт тотал языка-08"?

Смайлик забыл.

Я имел в виду, что в тотал языке нет fromJust, а значит выйти из Maybe в общем случае невозможно.

Здравствуйте, lomeo, Вы писали:

L>Здравствуйте, Курилка, Вы писали:

L>>>Потому что в стандарте тотал языка-08 нет fromJust (аналогичный unsafePerformIO).

К>>А что такое "стандарт тотал языка-08"?

L>Смайлик забыл.

Подтупливаю с утреца

L>Я имел в виду, что в тотал языке нет fromJust, а значит выйти из Maybe в общем случае невозможно.

Угу, тут возражений нету

L>Я имел в виду, что в тотал языке нет fromJust, а значит выйти из Maybe в общем случае невозможно.

вобще то выйти из Maybe можно при помощи maybe или fromMaybe

Ну так и что будем решать-то с этой арифметикой?
А то ещё хотелось бы обсудить проблемы субтипизации списков для тотальной реализации функции head...

Здравствуйте, <Аноним>, Вы писали:

L>>Я имел в виду, что в тотал языке нет fromJust, а значит выйти из Maybe в общем случае невозможно.

А>вобще то выйти из Maybe можно при помощи maybe или fromMaybe

выделено. выйдите из Maybe для 1/0.

Здравствуйте, geniepro, Вы писали:

G>Ну так и что будем решать-то с этой арифметикой?

Признать её невменяемой

Если серьёзно, то может разделить по типам. Пусть их будет две группы — одна с Maybe, другая с закрытой арифметикой.

G>А то ещё хотелось бы обсудить проблемы субтипизации списков для тотальной реализации функции head...

А зачем? Вот тут как раз всё в порядке — head вреден для здоровья.

Здравствуйте, lomeo, Вы писали:

G>>А то ещё хотелось бы обсудить проблемы субтипизации списков для тотальной реализации функции head...

L>А зачем? Вот тут как раз всё в порядке — head вреден для здоровья.

Ну, тоже решение. Хотя это уже отход от functional к declarative...

Здравствуйте, Курилка, Вы писали:

простите что влязию своей небритой глупой мордой, но где можно доходчиво почитать про ваши бананы, и прочие умные вещи. выжимки бы

Здравствуйте, deniok, Вы писали:

[]

Нам читали ФП, но то-ли я что-то прогулял, то-ли еще что, но про все это слышу в первый раз

Здравствуйте, lomeo, Вы писали:

[]

L>Это — бананы, а другие умные вещи — это что?

околобанановые темы

Здравствуйте, Константин Л., Вы писали:

L>>Это — бананы, а другие умные вещи — это что?

КЛ>околобанановые темы

"Читайте книжки, они рулез"

Здравствуйте, Константин Л., Вы писали:

КЛ>Здравствуйте, deniok, Вы писали:

КЛ>[]

КЛ>Нам читали ФП, но то-ли я что-то прогулял, то-ли еще что, но про все это слышу в первый раз

Как раз вчера обсуждали отечественные традиции преподавания курса "Функциональное и логическое программирование" Такое впечатление, что жизнь в этом мире закончилась в году 1975... Во многих местах — ЛИСП + Пролог, хорошо если ML упомянут.

Здравствуйте, deniok, Вы писали:

D>Здравствуйте, Константин Л., Вы писали:

КЛ>>Здравствуйте, deniok, Вы писали:

КЛ>>[]

КЛ>>Нам читали ФП, но то-ли я что-то прогулял, то-ли еще что, но про все это слышу в первый раз

D>Как раз вчера обсуждали отечественные традиции преподавания курса "Функциональное и логическое программирование" Такое впечатление, что жизнь в этом мире закончилась в году 1975... Во многих местах — ЛИСП + Пролог, хорошо если ML упомянут.

собсно, только лисп и пролог и были