Koka v2 is a research language that currently under heavy development with the new C backend
Latest release: v2.0.16, 2021-02-14 (Install).
Koka is a strongly typed functional-style language with effect types and handlers.
- The core of Koka consists of a small set of well-studied language features, like first-class functions, a polymorphic type- and effect system, algebraic data types, and effect handlers. Each of these is composable and avoid the addition of “special” extensions by being as general as possible.
- Koka tracks the (side) effects of every function in its type, where pure and effectful computations are distinguished. The precise effect typing gives Koka rock-solid semantics backed by well-studied category theory, which makes Koka particularly easy to reason about for both humans and compilers.
- Effect handlers let you define advanced control abstractions, like exceptions, async/await, or probabilistic programs, as a user library in a typed and composable way.
- Perceus is an advanced compilation method for reference counting. Together with evidence translation, this lets Koka compile directly to C code without needing a garbage collector or runtime system. Perceus also performs reuse analysis and optimizes functional-style programs to use in-place updates when possible.
For more information, see:
- Why Koka?
- The Koka book for a tour of the Koka language and its specification.
- The Library documentation.
- Help with development
Enjoy, Daan Leijen
Special thanks to:
- Ningning Xie for her work on the theory and practice of evidence translation [6] and the formalization of Perceus reference counting [8].
- Alex Reinking for the implementation of the Perceus reference counting analysis [8].
- And all previous interns working on earlier versions of Koka: Daniel Hillerström, Jonathan Brachthäuser, Niki Vazou, Ross Tate, Edsko de Vries, and Dana Xu.
Releases:
v2.0.16
, 2021-02-14: bug fixes, fix short-circuit evaluation of logical operations, improved utf-8 handling.v2.0.14
, 2020-12-11: bug fixes, improved var escape checking.v2.0.12
, 2020-12-02: syntax highlighting support for VS Code and Atom, improved uninstall, more samples.v2.0.9
, 2020-11-27: now with binary releases for Windows, macOS, and Linux.v2.0.7
, 2020-11-23: more small fixes, improved scoped handlers, improved higher-rank type propagation, more samples.v2.0.5
, 2020-11-15: many bug fixes and improvements. Improved codegen, named handlers, added samples, docker support, direct C compilation, local install support.v2.0.0
, 2020-08-21: initial v2 release.
For Linux and macOS on x86 64-bit, you can install Koka using:
> curl -sSL https://github.com/koka-lang/koka/releases/latest/download/install.sh | sh
This also installs syntax highlighting for the VS Code and Atom editors. After installation, verify if Koka installed correctly:
> koka
_ _ ____
| | | | |__ \
| | __ ___ | | __ __ _ __) |
| |/ // _ \| |/ // _` || ___/ welcome to the koka interpreter
| <| (_) | <| (_| ||____| version 2.0.12, Dec 2, 2020, libc 64-bit (gcc)
|_|\_\\___/|_|\_\\__,_| type :? for help, and :q to quit
loading: std/core
loading: std/core/types
loading: std/core/hnd
Type :q
to exit the interpreter.
For detailed instructions and other platforms (including Windows) see the releases page. It is also straightforward to build the compiler from source.
You can compile a Koka source using -c
(note that all samples
are pre-installed):
> koka -c samples/basic/caesar.kk
compile: samples/basic/caesar.kk
loading: std/core
loading: std/core/types
loading: std/core/hnd
loading: std/num/double
loading: std/text/parse
loading: std/num/int32
check : samples/basic/caesar
linking: samples_basic_caesar
created: out/v2.0.9/gcc-debug/samples_basic_caesar
and run the resulting executable:
> out/v2.0.9/gcc-debug/samples_basic_caesar
plain : Koka is a well-typed language
encoded: Krnd lv d zhoo-wbshg odqjxdjh
cracked: Koka is a well-typed language
The -O2
flag builds an optimized program. Let's try it on a purely functional implementation
of balanced insertion in a red-black tree (rbtree.kk
:
> koka -O2 -c samples/basic/rbtree.kk
...
linking: samples_basic_rbtree
created: out/v2.0.10/gcc-drelease/samples_basic_rbtree
> time out/v2.0.10/gcc-drelease/samples_basic_rbtree
420000
real 0m0.750s
...
We can compare this against an in-place updating C++ implementation using stl::map
(rbtree.cpp
) (which also uses a
red-black tree internally):
> clang++ --std=c++17 -o cpp-rbtree -O3 /usr/local/share/koka/v2.0.12/lib/samples/basic/rbtree.cpp
> time ./cpp-rbtree
420000
real 0m0.864s
...
The excellent performance relative to C++ here (on an AMD 3600XT) is the result of Perceus automatically transforming the fast path of the pure functional rebalancing to use mostly in-place updates, closely mimicking the imperative rebalancing code of the hand optimized C++ library.
Without giving any input files, the interactive interpreter runs by default:
> koka
_ _ ____
| | | | |__ \
| | __ ___ | | __ __ _ __) |
| |/ // _ \| |/ // _` || ___/ welcome to the koka interpreter
| <| (_) | <| (_| ||____| version 2.0.9, Nov 27 2020, libc 64-bit (gcc)
|_|\_\\___/|_|\_\\__,_| type :? for help
loading: std/core
loading: std/core/types
loading: std/core/hnd
>
Now you can test some expressions:
> println("hi koka")
check : interactive
check : interactive
linking: interactive
created: out\v2.0.9\mingw-debug\interactive
hi koka
> :t "hi"
string
> :t println("hi")
console ()
Or load a demo (use tab
completion to avoid typing too much):
> :l samples/basic/fibonacci
compile: samples/basic/fibonacci.kk
loading: std/core
loading: std/core/types
loading: std/core/hnd
check : samples/basic/fibonacci
modules:
samples/basic/fibonacci
> main()
check : interactive
check : interactive
linking: interactive
created: out\v2.0.9\mingw-debug\interactive
The 10000th fibonacci number is 33644764876431783266621612005107543310302148460680063906564769974680081442166662368155595513633734025582065332680836159373734790483865268263040892463056431887354544369559827491606602099884183933864652731300088830269235673613135117579297437854413752130520504347701602264758318906527890855154366159582987279682987510631200575428783453215515103870818298969791613127856265033195487140214287532698187962046936097879900350962302291026368131493195275630227837628441540360584402572114334961180023091208287046088923962328835461505776583271252546093591128203925285393434620904245248929403901706233888991085841065183173360437470737908552631764325733993712871937587746897479926305837065742830161637408969178426378624212835258112820516370298089332099905707920064367426202389783111470054074998459250360633560933883831923386783056136435351892133279732908133732642652633989763922723407882928177953580570993691049175470808931841056146322338217465637321248226383092103297701648054726243842374862411453093812206564914032751086643394517512161526545361333111314042436854805106765843493523836959653428071768775328348234345557366719731392746273629108210679280784718035329131176778924659089938635459327894523777674406192240337638674004021330343297496902028328145933418826817683893072003634795623117103101291953169794607632737589253530772552375943788434504067715555779056450443016640119462580972216729758615026968443146952034614932291105970676243268515992834709891284706740862008587135016260312071903172086094081298321581077282076353186624611278245537208532365305775956430072517744315051539600905168603220349163222640885248852433158051534849622434848299380905070483482449327453732624567755879089187190803662058009594743150052402532709746995318770724376825907419939632265984147498193609285223945039707165443156421328157688908058783183404917434556270520223564846495196112460268313970975069382648706613264507665074611512677522748621598642530711298441182622661057163515069260029861704945425047491378115154139941550671256271197133252763631939606902895650288268608362241082050562430701794976171121233066073310059947366875
And quit the interpreter:
> :q
I think of my body as a side effect of my mind.
-- Carrie Fisher (1956)
The samples/syntax
and samples/basic
directories contain various basic Koka examples to start with. If you type:
> :l samples/
in the interpreter, you can tab
twice to see the available sample files and directories.
Use :s
to see the source of a loaded module.
If you use VS Code or Atom, or if you set the koka_editor
environment variable,
you can type :e
in the interactive prompt to edit your program further. For example,
> :l samples/basic/caesar
...
check : samples/basic/caesar
modules:
samples/basic/caesar
> :e
<edit the source and reload>
> :r
...
check : samples/basic/caesar
modules:
samples/basic/caesar
> main()
- Read about the core concepts of Koka.
- Read a Tour of Koka in the Koka book.
- Check the Libraries documentation.
- Write some cool Koka programs :-)
These are initial benchmarks of Koka v2 with Perceus reference counting versus state-of-the-art memory reclamation implementations in various other languages. Since we compare across languages we need to interpret these results with care -- the results depend not only on memory reclamation but also on the different optimizations performed by each compiler and how well we can translate each benchmark to that particular language. We view these results therefore mostly as evidence that the current Koka implementation of reference counting is viable and can be competitive and not as a direct comparison of absolute performance between languages and systems.
As such, we select here only benchmarks that stress memory allocation, and we tried to select mature comparison systems that use a range of memory reclamation techniques and are considered best-in-class. The systems we compare are, Koka 2.0.3 (compiling the generated C code with gcc 9.3.0), OCaml 4.08.1, Haskell GHC 8.6.5, Swift 5.3, Java SE 15.0.1 with the Hotspot G1 collector, and C++ gcc 9.3.0.
The benchmarks are all available in test/bench
(see the
readme there for build instructions), and all
stress memory allocation with little computation:
rbtree
(inserts 42 million items into a red-black tree),
rbtree-ck
(a variant of rbtree
that keeps a list of every 5th
subtree and thus shares many subtrees), deriv
(the symbolic derivative of a large expression),
nqueens
(calculates all solutions for the n-queens problem of size 13
into a list, and returns the length of that list where the solution lists
share many sub-solutions), and cfold
(constant-folding over a large symbolic expression).
Note: in C++, without automatic memory management, many benchmarks are
difficult to express directly as they use persistent and
partially shared data structures. To implement these faithfully would
essentially require manual reference counting. Instead, we use C++ as
our performance baseline: we either use in-place updates
without supporting persistence (as in rbtree
which uses std::map
)
or we do not reclaim memory at all (as in deriv
, nqueens
, and cfold
).
The execution times and peak working set averaged over 10 runs and normalized to Koka are in the figure on the right (on a 3.8Ghz AMD3600XT on Ubuntu 20.04, Nov 2020).
We can see that even though Koka has currently few optimizations besides the reference counting ones, it performs very well compared to these mature systems, often outperforming by a significant margin -- both in execution time and peak working set. Clearly, these benchmarks are allocation heavy but it is encouraging to see this initial performance from Koka.
A full discussion of these benchmarks and systems can be found in the Perceus report.
Please help develop Koka: there are many opportunities to improve Koka or do research with Koka. We need:
- Emacs and Vim syntax highlighting.
- Improve documentation, landing page etc. Make it easier for people to contribute.
- More examples
- Many library modules are incomplete (like
std/os/file
) or missing (likestd/data/map
).
More advanced projects:
- Update the JavaScript backend to 1) use proper modules instead of amdefine, 2) use the new bigints instead of bigint.js,
and 3) add support for int64. This requires mostly changes to
Backend/JS/FromCore.hs
together withlib/core/core-inline.js
. - A language server for Visual Studio Code and Atom. Koka can already generate a typed range map so this should be managable.
- Package management of Koka modules.
- Implement inline specialization where functions like
map
,fold
etc get specialized for the function with which they are called. This is an important optimization for functional style languages to reduce the allocation of lambda's. - Various standard optimizations like case-of-case, join points, case-of-known constructor, etc.
- Borrowing analysis for Perceus.
- Known reference count specialization.
The following is the immediate todo list to be completed in the coming months:
- Port all libray modules, in particular
std/text/regex
(using PCRE), andstd/async
(usinglibuv
). - Run the full test suite again.
- Run the Bayesian probalistic machine learning program with large parameters.
- Improve compilation of local state to use local variables directly (in C).
- Functions with a pattern match in the argument.
Contact me if you are interested in tackling some of these :-)
Main branches:
master
: latest stable version.dev
: current development branch -- submit PR's to this branch.v1-master
: last stable version of Koka v1: this is Koka with the Javascript (and C#) backend which does not use evidence translation. This version supportsstd/async
and should compile examples from published papers.
Koka has few dependencies and should build from source without problems on most common platforms, e.g. Windows (including WSL), macOS X, and Unix. The following programs are required to build Koka:
- Stack to run the Haskell compiler.
(use> curl -sSL https://get.haskellstack.org/ | sh
on Unix and macOS X) - CMake to compile the Koka C support library.
(use> sudo apt-get install cmake
on Ubuntu,> brew install cmake
on macOS X). - Optional: the NodeJS runtime if using the Javascript backend.
- On Windows you need Visual Studio (for the windows SDK).
Build the compiler (note the --recursive
flag):
> git clone --recursive https://github.com/koka-lang/koka
> cd koka
> stack build
> stack exec koka
You can also use stack build --fast
to build a debug version of the compiler.
You can also build a local distribution bundle yourself from source and install
that locally. The util/bundle.kk
script creates a local distribution:
> stack exec koka -- util/bundle
...
distribution bundle created.
bundle : dist/koka-v2.0.9-linux-amd64.tar.gz
cc : gcc
version: v2.0.9
This takes a while as it pre-compiles the standard libraries in three build
variants (debug
, drelease
(release with debug info), and release
).
After generating the bundle, it can be installed locally as:
> util/install.sh -b dist/koka-v2.0.9-linux-amd64.tar.gz
(use util/install.bat
on Windows). After installation, you can now directly invoke koka
:
> koka --version
Koka is by default installed for the current user in <prefix>/bin/koka
,
(with architecture specific files under <prefix>/lib/koka/v2.x.x
and libraries and samples under <prefix>/share/koka/v2.x.x
).
On Windows, the default install is to the userprofile %APPDATA%\local
which
is usually already on the search path as stack
is installed there as well.
However, when using koka
you need to have a C compiler (when
using stack exec koka
the C compiler supplied with ghc
is used (mingw
)
but that is not generally available).
Generally, you need to install and run koka
from a
Visual Studio x64 toolset command prompt.
in order to link correctly with the Windows system libraries.
Koka can use either the cl
compiler (default), or the clang-cl
compiler
(use the --cc=clang-cl
option with Koka).
To bundle for a specific compiler, use this flag when running util/bundle
as well (from a VS command prompt):
> stack exec koka -- --cc=clang-cl util/bundle
or
> stack exec koka -- --cc=cl util/bundle
Generally, for Koka code, mingw
(gcc
) optimizes best, closely followed clang-cl
.
On a 3.8Gz AMD 3600XT, with mingw
7.2.0, clang-cl
11.0.0, and cl
19.28 we get:
> stack exec out\v2.0.5\mingw-release\test_bench_koka_rbtree -- --kktime
420000
info: elapsed: 0.624s, user: 0.625s, sys: 0.000s, rss: 163mb
> out\v2.0.5\clang-cl-release\test_bench_koka_rbtree --kktime
420000
info: elapsed: 0.727s, user: 0.734s, sys: 0.000s, rss: 164mb
> out\v2.0.5\cl-release\test_bench_koka_rbtree --kktime
420000
info: elapsed: 1.483s, user: 1.484s, sys: 0.000s, rss: 164mb
-
Daniel Hillerström, and Sam Lindley. “Liberating Effects with Rows and Handlers.” In Proceedings of the 1st International Workshop on Type-Driven Development, 15--27. TyDe 2016. Nara, Japan. 2016. doi:10.1145/2976022.2976033.
-
Daan Leijen. “Koka: Programming with Row Polymorphic Effect Types.” In Mathematically Structured Functional Programming 2014. EPTCS. Mar. 2014. arXiv:1406.2061.
-
Daan Leijen. Algebraic Effects for Functional Programming. MSR-TR-2016-29. Microsoft Research. Aug. 2016. https://www.microsoft.com/en-us/research/publication/algebraic-effects-for-functional-programming. Extended version of [4].
-
Daan Leijen. “Type Directed Compilation of Row-Typed Algebraic Effects.” In Proceedings of Principles of Programming Languages (POPL’17). Paris, France. Jan. 2017.
-
Nicolas Wu, Tom Schrijvers, and Ralf Hinze. “Effect Handlers in Scope.” In Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell, 1--12. Haskell ’14. ACM, New York, NY, USA. 2014. doi:10.1145/2633357.2633358
-
Ningning Xie, Jonathan Brachthäuser, Daniel Hillerström, Philipp Schuster, Daan Leijen. “Effect Handlers, Evidently” The 25th ACM SIGPLAN International Conference on Functional Programming (ICFP), August 2020. doi:10.1145/3408981, pdf
-
Ningning Xie and Daan Leijen. “Effect Handlers in Haskell, Evidently” The 13th ACM SIGPLAN International Haskell Symposium, August 2020. pdf
-
Alex Reinking, Ningning Xie, Leonardo de Moura, and Daan Leijen: “ Perceus: Garbage Free Reference Counting with Reuse” MSR-TR-2020-42, Nov 22, 2020. pdf