Как-то заглянув на GitHub, обнаружил Koka — язык функционального программирования со статической типизацией. Koka разрабатывается с 2012 года Daan Leijen в Microsoft Research, USA. Его исходники выкладываются на GitHub под лицензией Apache 2.0. Как признаются его авторы, он ещё не готов для промышленного применения: у него нет библиотек, менеджера пакетов и полной поддержки в средах разработки. При этом сам язык достаточно стабилен, а компилятор полностью разработан. Отдельными моментами язык напоминает Rust, Haskell и Scala. Сам же по себе он интересен контролем побочных эффектов. Это его основная фишка. Приглашаю познакомиться с Koka и обсудить его свойства.
fun main(): console ()
println("Hello, World!")Сначала пробежимся по свойствам языка, а затем рассмотрим один небольшой пример.
Итак, Koka обладает следующими свойствами:
- статическая типизация с выводом типов;
- функциональная парадигма;
- неизменяемость при наличии настоящих переменных;
- разделение на чистый код и код с побочными эффектами;
- синтаксис, напоминающий таковой у Rust и Scala;
- идентификаторы допускают символ дефис
-(как в Lisp); - комбинация синтаксисов со скобками и с отступами;
- типы-объединения и типы-структуры;
- полиморфизм;
- отсутствие циклов (при этом рекурсивный код при компиляции
может быть преобразован в циклический); - оператор возврата из функции необязателен:
результатом будет значение последнего выражения; - сопоставление с образцом;
- оператор точка, позволяющий заменить вложенные вызовы функций на их последовательность
(как операция|>в Elm или Elixir); - оператор
with, позволяющий избавиться от использования анонимных функций; - необязательные и именованные параметры функций;
- отсутствие сборщика мусора;
- компиляция в машинный код и другие целевые платформы;
- имеется REPL.
Подробно о языке можно почитать в официальной документации.
Инструкции по установке Koka есть на главной странице проекта. Поддерживаются только 64-х разрядные системы. Можно собрать из исходников, которые написаны на Haskell. Также дистрибутив можно получить с GitHub проекта. Например, для Debian и Ubuntu предлагаются готовые к установке пакеты.
После установки, кроме компилятора со стандартной библиотекой языка, будут установлены дополнения для подсветки синтаксиса в GNU Emacs, Atom и Visual Studio Code. В Code расширение было подхвачено автоматически. А в Emacs потребовалось написать в .emacs/init.el пару строчек:
(load "/usr/share/koka/v2.4.0/contrib/emacs/koka-mode")
(require 'koka-mode)Вычисляем числа Фибоначчи, или программирование с эффектами
Чтобы познакомиться с Koka на деле, напишем программу, которая вычисляет n-е число Фибоначчи и печатает его в консоли.
Синтаксис языка достаточно прост, чтобы набросать начальную версию программы:
fun main()
val n = 10
println(fib(n))
fun fib(n : int) : int
match n
0 -> 0
1 -> 1
_ -> fib(n - 1) + fib(n - 2)Сохраним файл с именем fibonacci.kk и попробуем скомпилировать эту программу:
koka fibonacci.kkИ получим вот такое сообщение компилятора:
compile: fibonacci.kk
loading: std/core
loading: std/core/types
loading: std/core/hnd
check : fibonacci
fibonacci.kk(5, 5): error: effects do not match
context : fib
term : fib
inferred effect: (<>)
expected effect: <div|_e>
because : effect cannot be subsumedЗдесь мы видим, что компиляция прошла успешно, то есть синтаксически программа корректна, но вот проверку программа уже не прошла: функция fib была неявно объявлена с эффектом total, коротко обозначаемым как <>, что означает чистоту. Но чекер обнаружил, что у функции эффект другого типа div. Этот тип эффектов возникает в программах, в которых не гарантируется останов. По видимому компилятор так решил, потому что наша функция рекурсивна. (Добавление проверки на отрицательный аргумент не делает функцию с точки зрения чекера тотальной. Оставлю читателю этот эксперимент в качестве упражнения.)
У нас есть два варианта:
- задать конкретный тип эффекта
div; - или попросить вывести тип эффекта, указав
_.
fun main()
val n = 10
println(fib(n))
fun fib(n : int) : _ int
match n
0 -> 0
1 -> 1
_ -> fib(n - 1) + fib(n - 2)Теперь программа успешно соберётся. Запустим и убедимся в правильности результата:
./.koka/v2.4.0/gcc-debug/fibonacciВообще, этот код с подвохом: мы не задали тип для функции main. Каков же он на самом деле? Давайте попробуем разобраться.
Запустим REPL:
kokaЗагрузим наш модуль:
:l fibonacci.kkИ запросим тип функции fib:
:t fibПолучим ожидаемое:
check : interactive
(n : int) -> div intТеперь для main:
:t mainОказывается у main тип такой:
check : interactive
() -> <console,div> ()То есть main ничего не возвращает (имеет пустой тип ()) и имеет два эффекта: div и console. Первый эффект обусловлен вызовом из main функции с таким эффектом, а второй связан с тем, что main осуществляет ввод-вывод.
В Koka есть ещё два вида эффектов:
-
exnдля функций, генерирующих исключения; -
ndetдля недетерминированных функций.
Но вы можете создавать свои собственные эффекты и их обработчики.
Так что давайте этом займёмся: добавим в наш код печать отладочной информации — будем выводить в консоль каждое вычисленное значение числа Фибоначчи. Обычное решение в этом случае — вставить в нужное место кода функцию печати:
fun debug-info(value : int) : _ int
println(value)
return value
fun fib(n : int) : _ int
debug-info(match n {
0 -> 0
1 -> 1
_ -> fib(n - 1) + fib(n - 2)})
fun main()
val n = 10
println(fib(n))Но что если мы хотим в разных местах кода для вызова fib печатать по разному? Вот здесь нам уже пригодятся эффекты с обработчиками:
effect fun debug-info(value : int) : int
fun fib(n : int) : _ int
debug-info(match n {
0 -> 0
1 -> 1
_ -> fib(n - 1) + fib(n - 2)})
fun main()
val n = 10
with handler
fun debug-info(value)
println(value)
return value
println(fib(n))
with handler
fun debug-info(value)
println("* " ++ show(value) ++ " *")
return value
println(fib(n))В первой строке кода мы объявили абстрактный эффект, а перед вызовом кода, где вычисляется fib мы определяем обработчик этого эффекта с помощью конструкции with handler.
На практике
Как уже говорилось выше, для Koka нет ни библиотек (кроме стандартной), ни менеджера пакетов, а для редакторов кода есть только синтаксическая подсветка. И кажется, что Koka никуда не годится, однако это не совсем так. Автор языка разработал на нём транслятор для markdown в HTML и PDF (с привлечением TeX) для научных текстов Madoko. (В Ubuntu для работы Madoko потребуется дополнительно установить пакет texlive-science.)
Что дальше поизучать
- Посмотреть и послушать доклад на конференции от самого автора языка Daan Leijen. Видео длинное, два с половиной часа, но достаточно интересное и понятное.
- Проштудировать официальную документацию. На одной странице рассмотрены все концепции языка.
- Ознакомиться с примерами кода в исходных текстах Koka на GitHub и с исходниками его стандартной библиотеки (там же).
- Попытаться прочитать научные статьи, в которых описывается математика языка и его компилятора. Ссылки можно найти в README исходных текстов.
© Симоненко Евгений, 2022
Комментарии (25)
csl
16.02.2022 01:03+1Удачное проведение параллелей между оператором точка в Koka и операцией |> в Elixir. Ещё бы добавить подсветку синтаксиса для Koka в highlight.js, чтобы и на Хабре улучшить отображение (выделение цветом, например).
easimonenko Автор
16.02.2022 01:08+1Про подсветку Koka я тоже подумал. К слову сказать в Emacs в markdown-mode она подхватывается.
easimonenko Автор
17.02.2022 12:10+2Посмотрел как добавить в highlight.js новый язык: они больше не принимают языки в саму библиотеку, все новые языки должны идти отдельными библиотеками. Но можно им написать, чтобы они добавили её себе для распространения. Поэтому автоматом на Хабре подсветка Koka не появится. https://github.com/highlightjs/highlight.js/blob/main/extra/3RD_PARTY_QUICK_START.md
Kroleg
16.02.2022 04:23+4Крутая фича "отсутствие сборщика мусора"
Как они это сделали? "Since mutable references are uncommon in our setting, we leave the responsibility to the programmer to break cycles"
Чуда не произошло. :-(
sashagil
16.02.2022 09:18+2Пока нет, но вы оборвали цитирование.
... "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."
worldmind
16.02.2022 08:14+2Начал читать и не понял зачем его создавали, в чём отличия от хаскела да идриса? По идее с этого должна начинаться статья. В коментах про отсутствие сборщика мусора, конкурент расту?
sashagil
16.02.2022 09:10+3Алгебраические эффекты вместо хаскелевских монад упрощают ряд вещей, это довольно интересная тема.
worldmind
16.02.2022 10:15+2А есть где сравнение упомянутых для чайников?
sashagil
16.02.2022 19:49+4Есть статьи, взвешенно-нейтрально разбирающие два подхода (в общем контексте программирования на Хаскеле, чаще всего), и есть более однобокие «вводные» статьи. Приведу ссылки, а ниже изложу своё поверхностное мнение (по воспоминаниям по просмотру статей, я темой интересовался).
«Алгебраические эффекты» человеческим языком - перевод на Хабре вводной статьи прикладного программиста, который ближе к концу поясняет, что с Хаскелем он не знаком и потому научные статьи ему непонятны, он рассматривает тему с практическими примерами на 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).
easimonenko Автор
16.02.2022 10:25+6Странности какие-то на Хабре: заглядываю утром в статью и вижу, что слетели все ссылки. С чего бы это? Открываю статью в редакторе (markdown) и вижу, что список ссылок в конце статьи отредактирован. Это как? Автоматически? Но зачем? Или редактор? Но тогда редактору нужно поучить markdown сначала.
Для тех, кто не понял, я использую списки ссылок в формате [Название]: URL. Затем в тексте обращаюсь к ним как [Название][] или [другой текст][Название].
youngmysteriouslight
Вполне интересно. Можно подробнее описать систему типов? Есть операторы типов высших порядков, например? Какой используется полиморфизм?
Кстати, первый пример с fib удивляет. Кажется, что fib должна быть самой настоящей total, потому что она примитивно-рекурсивна. Как доказать компилятору, что она всегда завершается?
upd. Только что увидел заявление
отсутствие сборщика мусора
Это как? Я не в теме, но как слышал, только Rust успешно смог организовать работу с функциями, чтобы обойтись без сборщика мусора, и за это заплатили цену введением неинтуитивных концепций, вроде владения. Тут такой же масштаб амбиций или имеется в виде что-то другое?
easimonenko Автор
Большое спасибо за вопросы! Наверное чтобы на них ответить, мне нужно будет написать ещё один пост. К сожалению официальная документация неполна, поэтому придётся копать глубже.
Меня это тоже сначало удивило. Но ведь тип int влючает в себя также и отрицательные числа, для которых fib не остановится. Попробовал сейчас этот пример при `n = -1`, и он рухнул с ошибкой сегментирования памяти. Наверное в каком нибудь Idris такое даже не скомпилировалось бы. (Но я в Idris и Agda не особо разбираюсь.)
Вот в этой статье авторы описывают алгоритм, благодаря которому они избавились от 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/
youngmysteriouslight
Примерно понятно.
Это и не должно работать. Функция определена так, чтоб аргумент был положительным; а по-хорошему, сигнатура должна быть соответствующей, nat -> nat.
Как Int -> Int, конечно, нет, а Nat -> Nat — да, причём тотальна без доп. вопросов. В Idris бывает проблема, когда функция тотальна или рассматриваемый тип не населён, но компилятор не сразу догадывается, там надо доказывать, но Idris предоставляет средства логики первого порядка для доказательств, или believe_me накрайняк.
0xd34df00d
Логика там не только первого порядка, но да, завершимость можно доказывать (я про это даже писал тут).
Другое дело, что не любой на самом деле завершимый рекурсивный терм доказуемо завершим. Гедель и Тьюринг тут где-то рядом.
funca
Концепция владения в Rust скорее непривычна. В бэкграунде там простая идея, что каждое значение может использоваться максимум один раз, которая в свою очередь формализована в affine types https://en.m.wikipedia.org/wiki/Substructural_type_system .
csl
Не споря с вами: там и одна из первых прикладных реализаций субструктурной типизации и линейной (здесь подразумевается любой вариант субструктурной типизации) логики.
https://habr.com/ru/post/497762/comments/#comment_21514808
funca
@0xd34df00dвиднее, что он имел ввиду. :) Вики пишут, что ещё Clean это использовал уже 30 лет с хвостиком тому назад (я с ним не знаком, могу ошибаться. судя по описанию там это применяли для проверки корректности кода, а не управления памятью).
Писать на языке именно с линеарными типами (это когда каждое значение нужно где-то поиспользовать) наверное ацки неудобно. Интересно как там будет выглядеть применение функций в роде print (результат возврата которой придется тоже кому-то отдавать)?
csl
Что использует Clean, виднее @vkni.
Некоторые особенности https://habr.com/ru/post/596193/comments/#comment_23858079
vkni
Clean использует unique типы, родственные линейным, где действительно можно просто "съедать" значение. Насколько я понимаю, к линейным типам это сводится если в линейных сделать какую-нибудь функцию
eat:: *a -> ().funca
Такой eat не тайпчекнится если у нас линеарные типы. Но это можно с афиными где разрешается использовать значение <=1 раз.
0xd34df00d
Да не, это все вполне пристойно засахаривается. Другое дело, что, ИМХО, не надо бросаться весь код переписывать на линейных типах, и они скорее нужны либо для корректности (ну там не забыть закрыть хендл и не закрыть его дважды), либо для производительности и мутабельности без явной ST.
vkni
Что характерно, в Tackling the Awkward Squad, Саймон-Пейтон рассказывает про IO монады, фактически, переписывая всё на Clean. Ну когда он вводит на пятой странице
type IO a = World -> (a, World). Только на реальном Клине там нужно ещё поставить * и заменить ключевое словоtypeна продукт сумрачного голландского гения::: IO a = *World -> *(a, *World)
vkni
Там это применяли для реализации побочных эффектов, но без монад, т.к. 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
Посколько голландцы, как и французы, пытались сделать что-то промышленно-годное, в отличие от англичан, они заморачивались производительностью, поэтому использовали уникальные типы не только для ввода-вывода, но и для реализации изменяемых массивов.
funca
О практическом использовании в хаскеле https://wiki.zhen-zhang.com/tech/notes/books/AT-TAPL/Substructural%20Types/