Comments 27
Вполне интересно. Можно подробнее описать систему типов? Есть операторы типов высших порядков, например? Какой используется полиморфизм?
Кстати, первый пример с fib удивляет. Кажется, что fib должна быть самой настоящей total, потому что она примитивно-рекурсивна. Как доказать компилятору, что она всегда завершается?
upd. Только что увидел заявление
отсутствие сборщика мусора
Это как? Я не в теме, но как слышал, только Rust успешно смог организовать работу с функциями, чтобы обойтись без сборщика мусора, и за это заплатили цену введением неинтуитивных концепций, вроде владения. Тут такой же масштаб амбиций или имеется в виде что-то другое?
Большое спасибо за вопросы! Наверное чтобы на них ответить, мне нужно будет написать ещё один пост. К сожалению официальная документация неполна, поэтому придётся копать глубже.
Кстати, первый пример с fib удивляет. Кажется, что fib должна быть самой
настоящей total, потому что она примитивно-рекурсивна. Как доказать
компилятору, что она всегда завершается?
Меня это тоже сначало удивило. Но ведь тип int влючает в себя также и отрицательные числа, для которых fib не остановится. Попробовал сейчас этот пример при `n = -1`, и он рухнул с ошибкой сегментирования памяти. Наверное в каком нибудь Idris такое даже не скомпилировалось бы. (Но я в Idris и Agda не особо разбираюсь.)
Я не в теме, но как слышал, только Rust успешно смог
организовать работу с функциями, чтобы обойтись без сборщика мусора, и
за это заплатили цену введением неинтуитивных концепций, вроде владения.
Тут такой же масштаб амбиций или имеется в виде что-то другое?
Вот в этой статье авторы описывают алгоритм, благодаря которому они избавились от GC: Alex Reinking, Ningning Xie, Leonardo de Moura, and Daan Leijen: “Perceus: Garbage Free Reference Counting with Reuse” MSR-TR-2020-42, Nov 22, 2020. Distinguished paper at PLDI'21. https://www.microsoft.com/en-us/research/publication/perceus-garbage-free-reference-counting-with-reuse/
Примерно понятно.
Попробовал сейчас этот пример при
n = -1, и он рухнул с ошибкой сегментирования памяти.
Это и не должно работать. Функция определена так, чтоб аргумент был положительным; а по-хорошему, сигнатура должна быть соответствующей, nat -> nat.
Наверное в каком нибудь Idris такое даже не скомпилировалось бы.
Как Int -> Int, конечно, нет, а Nat -> Nat — да, причём тотальна без доп. вопросов. В Idris бывает проблема, когда функция тотальна или рассматриваемый тип не населён, но компилятор не сразу догадывается, там надо доказывать, но Idris предоставляет средства логики первого порядка для доказательств, или believe_me накрайняк.
Концепция владения в Rust скорее непривычна. В бэкграунде там простая идея, что каждое значение может использоваться максимум один раз, которая в свою очередь формализована в affine types https://en.m.wikipedia.org/wiki/Substructural_type_system .
Не споря с вами: там и одна из первых прикладных реализаций субструктурной типизации и линейной (здесь подразумевается любой вариант субструктурной типизации) логики.
@0xd34df00dвиднее, что он имел ввиду. :) Вики пишут, что ещё Clean это использовал уже 30 лет с хвостиком тому назад (я с ним не знаком, могу ошибаться. судя по описанию там это применяли для проверки корректности кода, а не управления памятью).
Писать на языке именно с линеарными типами (это когда каждое значение нужно где-то поиспользовать) наверное ацки неудобно. Интересно как там будет выглядеть применение функций в роде print (результат возврата которой придется тоже кому-то отдавать)?
Что использует Clean, виднее @vkni.
Некоторые особенности https://habr.com/ru/post/596193/comments/#comment_23858079
Что характерно, в Tackling the Awkward Squad, Саймон-Пейтон рассказывает про IO монады, фактически, переписывая всё на Clean. Ну когда он вводит на пятой странице type IO a = World -> (a, World). Только на реальном Клине там нужно ещё поставить * и заменить ключевое слово type на продукт сумрачного голландского гения:
:: IO a = *World -> *(a, *World)
судя по описанию там это применяли для проверки корректности кода, а не управления памятью
Там это применяли для реализации побочных эффектов, но без монад, т.к. Clean - это один из чистых ленивых языков, наследников Miranda. Сейчас Clean очень похож на Haskell. Реализация ввода-вывода в Clean фактически изложена на 5 странице самой понятной статьи про IO в Haskell, Tackling the Awkward Squad:... - https://www.microsoft.com/en-us/research/wp-content/uploads/2016/07/mark.pdf
Посколько голландцы, как и французы, пытались сделать что-то промышленно-годное, в отличие от англичан, они заморачивались производительностью, поэтому использовали уникальные типы не только для ввода-вывода, но и для реализации изменяемых массивов.
Удачное проведение параллелей между оператором точка в Koka и операцией |> в Elixir. Ещё бы добавить подсветку синтаксиса для Koka в highlight.js, чтобы и на Хабре улучшить отображение (выделение цветом, например).
Про подсветку Koka я тоже подумал. К слову сказать в Emacs в markdown-mode она подхватывается.
Посмотрел как добавить в highlight.js новый язык: они больше не принимают языки в саму библиотеку, все новые языки должны идти отдельными библиотеками. Но можно им написать, чтобы они добавили её себе для распространения. Поэтому автоматом на Хабре подсветка Koka не появится. https://github.com/highlightjs/highlight.js/blob/main/extra/3RD_PARTY_QUICK_START.md
Может показаться интересным https://proofassistants.stackexchange.com
Пока нет, но вы оборвали цитирование.
... "However, we have plans for future improvements: since we know statically that only mutable references are able toform a cycle, we could generate code that tracks those datatypes at run time and may perform a more efficient form of incremental cycle collection."
Начал читать и не понял зачем его создавали, в чём отличия от хаскела да идриса? По идее с этого должна начинаться статья. В коментах про отсутствие сборщика мусора, конкурент расту?
Алгебраические эффекты вместо хаскелевских монад упрощают ряд вещей, это довольно интересная тема.
А есть где сравнение упомянутых для чайников?
Есть статьи, взвешенно-нейтрально разбирающие два подхода (в общем контексте программирования на Хаскеле, чаще всего), и есть более однобокие «вводные» статьи. Приведу ссылки, а ниже изложу своё поверхностное мнение (по воспоминаниям по просмотру статей, я темой интересовался).
«Алгебраические эффекты» человеческим языком - перевод на Хабре вводной статьи прикладного программиста, который ближе к концу поясняет, что с Хаскелем он не знаком и потому научные статьи ему непонятны, он рассматривает тему с практическими примерами на JavaScript (ссылка на оригинал статьи для удобства). Более недавняя статья другого программиста с примерами на OCaml: Friendship ended with Monads: Testing out Algebraic effects in OCaml for Animations.
Научные статьи, рассматривающие алгебраические эффекты и альтернативные подходы (монадные трансформеры) в рамаках Хаскеля: Monad Transformers and Modular Algebraic Effects (What Binds Them Together), Freer Monads, More Extensible Effects. Я такие статьи, скорее, просматриваю - с Хаскелем шапочно знаком, но не программирую на нём.
Уместна ссылка на давнюю статью автора Koka: Algebraic effects for Functional Programming.
Моё поверхностное мнение: мне бы на Koka было бы удобнее программировать, чем разбираться с монадными трансформерами на Хаскеле. Koka - компактный язык, чётко иллистрирующий идею как "чисто" программировать в функциональном стиле с эффектами ("чисто" в том смысле, что нотация эффектов явная, и при этом не особо навязчивая). В плюс к этому - такое программирование хорошо укладывается у меня в голове (я "вижу", что будет происходить в машинном коде при выполнении - и при желании могу разобраться в сгенерированном компилятором Koka коде на стандартном C, реализуещем нужную семантику благодаря фиче C longjump, насколько я понимаю). Ну и -- при желании я этот код на C мог бы встроить в свою программу (на C++); не уверен, что получилось бы легко с встраиванием кода на Хаскеле.
С Rust сравнивать, наверно, можно, но осторожно - размах не тот (Rust - промышленный язык, Koka - скорее, демонстрационный, ну, как сравнивать Rust и Idris).
Странности какие-то на Хабре: заглядываю утром в статью и вижу, что слетели все ссылки. С чего бы это? Открываю статью в редакторе (markdown) и вижу, что список ссылок в конце статьи отредактирован. Это как? Автоматически? Но зачем? Или редактор? Но тогда редактору нужно поучить markdown сначала.
Для тех, кто не понял, я использую списки ссылок в формате [Название]: URL. Затем в тексте обращаюсь к ним как [Название][] или [другой текст][Название].
Обзор языка функционального программирования Koka