Обзор языка функционального программирования Koka
Как-то заглянув на 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 и исходниками его стандартной библиотеки (там же).
- Попытаться прочитать научные статьи, в которых описывается математика языка и его компилятора. Ссылки можно найти в README исходных текстов.
Ссылки
- Koka Home Page
- Daan Leijen
- Koka Project in Microsoft Research
- Koka Documentation
- Koka GitHub
- Koka Releases
- Madoko
Примечание
Первоначально этот пост был опубликован на Хабре (15 февраля 2022).
(c) Симоненко Евгений, 2022