Кстати, получение факториала в терминах 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 и др. по желанию)?
Кстати хоть аналогии и зло, но вот как ты считаешь — монады стоят того, чтобы с ними заморачиваться?
Здравствуйте, geniepro, Вы писали:
G>Я вот прихожу постепенно к выводу, что Total FP в удобном (юзабельном) виде -- это фантастика. В смысле -- невозможно.
Возможно. Для меня интерес представляет сам подход. Насколько он будет юзабелен я смогу оценить только попробовав на задаче.
Что касается практической ценности, то это как с обсуждавшейся тут теоремой Ферма, в прямой ценности я сомневаюсь (что касается вещ. чисел, например), но вот кучу бенефитов при разборе этого подхода я надеюсь получить.
G>Total FP, как я понял, ориентирован на математической индукции, которая работает только на натуральных числах, и на списочной индукции. Отсюда два важных ограничения -- родными для TFP будут натуральные числа (с двумя операциями + и *) и конечные списки.
Хотя бы для какой то группы функций мы можем быть уверенными в завершимости.
G>То есть об удобной работе с вещественными числами (а возможно даже и с отрицательными целыми), похоже, придётся забыть, и некоторые удобные приёмы, связанные с ленивыми бесконечными списками, тоже отпадут. (Правда, я плохо знаю всякие там коданные/косписки/комонады/корекурсии/ко.....)
Если список бесконечен, то это кодата.
Что касается вещественных чисел, то это просто вопрос, с которым надо разобраться. Возможно, там можно принять какое то практические решение. В конце концов не считать некоторые функции гарантировано завершимыми. Это и вопрос с bottom мне, если честно, интересен не так как структурная рекурсия, например, или вывод гарантии завершимости.
G>Так что же получается? Стоит ли Total FP того, что бы с ним заморачиваться?
Думаю, да.
G>Даёт ли гарантированная останавливаемость функций достаточно бенефитов, что бы оправдать кучу неудобств?
Здравствуйте, 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
Здравствуйте, 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, достаточно группы функций, про которые я могу быть уверен в их завершимости. Пойдёт?
L>Перефразирую. Меня мало интересует тотальное отсутствие bottom, достаточно группы функций, про которые я могу быть уверен в их завершимости. Пойдёт?
А как их маркировать? Грязь прячем в IO, невозможность полного паттерн матчинга — в Maybe (ну можем, по крайней мере, если не хотим error), а отсутствие гарантий завершаемости?
Здравствуйте, deniok, Вы писали:
D>Здравствуйте, lomeo, Вы писали:
L>>Перефразирую. Меня мало интересует тотальное отсутствие bottom, достаточно группы функций, про которые я могу быть уверен в их завершимости. Пойдёт?
D>А как их маркировать? Грязь прячем в IO, невозможность полного паттерн матчинга — в Maybe (ну можем, по крайней мере, если не хотим error), а отсутствие гарантий завершаемости?
В том и фишка — ничего мы не прячем, совсем!
Только это ограничивает набор входных программ, иначе никак.
