search

koka-lang / koka

Koka language compiler and interpreter
http://koka-lang.org
Other
3.16k stars 151 forks source link
algebraic-effects effect-handlers handler haskell koka

readme

 

Koka: a Functional Language with Effects

Koka v3 is a research language that is currently under development and not quite ready for production use.

Latest release: v3.1.2, 2024-05-30 (Install).

Koka is a strongly typed functional-style language with effect types and handlers.

To learn more:

Enjoy, Daan Leijen

Special thanks to: Tim Whiting and Fredrik Wieczerkowski for their work on the VS Code language integration, Anton Lorenzen for his work on one-hole context (pdf), fully in-place programming [11] and frame-limited reuse in Perceus [10], Ningning Xie for her work on the theory and practice of evidence passing [9,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.

Recent Releases

Install

Koka has binary installers for Windows (x64), macOS (x64, M1), and Linux (x64) For other platforms, you need to build the compiler from source.

Build from Source

Koka has few dependencies and should build from source without problems on most common platforms, e.g. Windows (including WSL), macOS, and Unix. The following programs are required to build Koka:

Now clone the repository and build the compiler as:

$ git clone --recursive https://github.com/koka-lang/koka
$ cd koka
$ stack update
$ stack build
$ stack exec koka

(Note: if you forgot to pass --recursive on cloning, you will get errors when compiling Koka modules -- you can correct this by running git submodule update --init --recursive).

You can also use stack build --fast to build a debug version of the compiler, and use stack test --fast to run the test-suite.

To run a single test you can run stack test filtering based on paths such as stack test --test-arguments '-m "lib"'. This will run all tests that are under the test/lib directory.

(See the build notes below if you have issues when running- or installing stack).

Create an Install Bundle

Koka can generate a binary install bundle that can be installed on the local machine:

$ stack exec koka -- -e util/bundle
...
distribution bundle created.
  bundle : bundle/v2.3.9/koka-v2.3.9-linux-x64.tar.gz
  cc     : gcc
  version: v2.3.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, you can install it locally as:

$ util/install.sh  bundle/v2.3.9/koka-v2.3.9-linux-x64.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 Unix and macOS the default prefix is /usr/local while on Windows the default prefix is %LOCALAPPDATA%\koka.

It is also possible to generate installation packages for various Linux platforms (RHEL, Debian, Alpine, etc.). See the [readme][util/packaging] for further information.

Benchmarks

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.

Tasks

Please help develop Koka: there are many opportunities to improve Koka or do research with Koka. We need:

More advanced projects:

Master/PhD level:

Currently being worked on:

The following is the immediate todo list to be completed in the coming months:

LSP Related Tasks:

Extension Related Tasks:

VSCode:

Contact me if you are interested in tackling some of these :-)

Build Notes

Branches

The main development branches are:

Building on macOS M1

You need at least stack version >= 2.11 Furthermore, you may need to add the brew installed LLVM to your path afterwards, or otherwise stack cannot find the LLVM tools. Add the following to your ~/.zshrc script and open an fresh prompt:

export PATH=/opt/homebrew/opt/llvm/bin:$PATH

Building with Cabal

Some platforms (like Linux arm64 and FreeBSD) do not always support stack well. In these cases we can also use ghc and cabal directly. Install these packages as:

$ sudo apt update
$ sudo apt install ghc cabal-install

On macOS (x64 and arm64) we use brew instead:

$ brew install pkg-config ghc cabal-install

On FreeBSD, use pkg:

$ sudo pkg update
$ sudo pkg install ghc hs-cabal-install   # or: hs-haskell-platform

Optionally, install vcpkg as well. If you install this in the ~/vcpkg directory Koka will find it automatically when needed:

~$ git clone https://github.com/microsoft/vcpkg
~$ ./vcpkg/bootstrap-vcpkg.sh
~$ vcpkg/vcpkg install pcre

We can now build the compiler using cabal as:

~$ git clone --recursive https://github.com/koka-lang/koka
~$ cd koka
~/koka$ cabal new-update
~/koka$ cabal new-build
~/koka$ cabal new-run koka

We can also run tests as:

~/koka$ cabal new-run koka-test

or create an installer:

~/koka$ cabal new-run koka -- -e util/bundle

Building with minbuild

If neither stack nor cabal are functional, you may try to run the minimal build script to build Koka:

~/koka$ ./util/minbuild.sh

which directly invokes ghc to build the compiler. You can create an install bundle from a minbuild as:

~/koka$ .koka/minbuild/koka -e util/bundle.kk -- --koka=.koka/minbuild/koka

Windows C Compilers

The Koka compiler on Windows requires a C compiler. By default when using stack exec koka the C compiler supplied with ghc is used (mingw) but that is only visible within a stack environmet.

It is therefore recommended to install the clang compiler for Windows (which is automatically installed when running util/install.bat). However, Koka can also use the Microsoft Visual C++ compiler (cl) if you run koka from a Visual Studio x64 toolset command prompt (in order to link correctly with the Windows system libraries).

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

Language Server

See the support/vscode/README.md for how to build the VS Code language server.

Older Release Notes

References

  1. 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.

  2. Daan Leijen. “Koka: Programming with Row Polymorphic Effect Types.” In Mathematically Structured Functional Programming 2014. EPTCS. Mar. 2014. arXiv:1406.2061.

  3. 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].

  4. Daan Leijen. “Type Directed Compilation of Row-Typed Algebraic Effects.” In Proceedings of Principles of Programming Languages (POPL’17). Paris, France. Jan. 2017.

  5. 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

  6. 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. See also [9] which improves upon this work.

  7. Ningning Xie and Daan Leijen. “Effect Handlers in Haskell, Evidently” The 13th ACM SIGPLAN International Haskell Symposium, August 2020. pdf See also the Ev.Eff and Mp.Eff repositories.

  8. 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. pdf

  9. Ningning Xie and Daan Leijen. “ Generalized Evidence Passing for Effect Handlers” In The 26th ACM SIGPLAN International Conference on Functional Programming (ICFP), August 2021. Also as MSR-TR-2021-5, Mar, 2021. pdf

  10. Anton Lorenzen and Daan Leijen. “ Reference Counting with Frame-Limited Reuse” Microsoft Research technical report MSR-TR-2021-30, Nov 2021, (updated Mar 2022, v2). pdf

  11. Anton Lorenzen, Daan Leijen, and Wouter Swierstra. “FP2: Fully in-Place Functional Programming” The 28th ACM SIGPLAN International Conference on Functional Programming (ICFP), September 2023. pdf (extended tech. report MSR-TR-2023-19, May 2023).