Обзор языка функционального программирования 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 на GitHub и с исходниками его стандартной библиотеки (там же).
• Попытаться прочитать научные статьи, в которых описывается математика языка и его компилятора. Ссылки можно найти в README исходных текстов.

© Симоненко Евгений, 2022