1. Getting started

Welcome to Koka – a strongly typed functional-style language with effect types and handlers.

Why Koka? A Tour of Koka Install Discussion forum Github Libraries

1.1. Installing the compiler

On macOS (x64, M1), you can install and upgrade Koka using Homebrew:

brew install koka

On Windows (x64), open a cmd prompt and use:

curl -sSL -o %tmp%\install-koka.bat https://github.com/koka-lang/koka/releases/latest/download/install.bat && %tmp%\install-koka.bat

On Linux (x64, arm64) and FreeBSD (x64) (and macOS), you can install Koka using:

curl -sSL https://github.com/koka-lang/koka/releases/latest/download/install.sh | sh

There are also installation packages for various Linux distributions: Ubuntu/Debian (x64, arm64), Alpine (x64, arm64), Arch (x64, arm64), Red Hat (x64), and openSUSE (x64).

After installation, verify if Koka installed correctly:

$ koka
 _         _
| |       | |
| | _ ___ | | _ __ _
| |/ / _ \| |/ / _' |  welcome to the koka interactive compiler
|   ( (_) |   ( (_| |  version 2.4.0, Feb  7 2022, libc x64 (gcc)
|_|\_\___/|_|\_\__,_|  type :? for help, and :q to quit

loading: std/core
loading: std/core/types
loading: std/core/hnd
>

Type :q to exit the interactive environment.

For detailed installation instructions and other platforms see the releases page. It is also straightforward to build the compiler from source.

1.2. Running the compiler

You can compile a Koka source as (note that all samples are pre-installed):

$ koka samples/basic/caesar.kk
compile: samples/basic/caesar.kk
loading: std/core
loading: std/core/types
loading: std/core/hnd
loading: std/num/float64
loading: std/text/parse
loading: std/num/int32
check  : samples/basic/caesar
linking: samples_basic_caesar
created: .koka/v2.3.1/gcc-debug/samples_basic_caesar

and run the resulting executable:

$ .koka/v2.3.1/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 -o kk-rbtree samples/basic/rbtree.kk
...
linking: samples_basic_rbtree
created: .koka/v2.3.1/gcc-drelease/samples_basic_rbtree
created: kk-rbtree

$ time ./kk-rbtree
420000
real    0m0.626s
...

(On Windows you can give the --kktime option to see the elapsed time). 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.3.1/lib/samples/basic/rbtree.cpp
$ time ./cpp-rbtree
420000
real    0m0.667s
...

The excellent performance relative to C++ here (on Ubuntu 20.04 with an AMD 5950X) 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.

1.3. Running the interactive compiler

Without giving any input files, the interactive environment runs by default:

$ koka
 _         _
| |       | |
| | _ ___ | | _ __ _
| |/ / _ \| |/ / _' |  welcome to the koka interactive compiler
|   ( (_) |   ( (_| |  version 2.3.1, Sep 21 2021, libc x64 (clang-cl)
|_|\_\___/|_|\_\__,_|  type :? for help, and :q to quit

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: .koka\v2.3.1\clang-cl-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: .koka\v2.3.1\clang-cl-debug\interactive

The 10000th fibonacci number is 33644764876431783266621612005107543310302148460680063906564769974680081442166662368155595513633734025582065332680836159373734790483865268263040892463056431887354544369559827491606602099884183933864652731300088830269235673613135117579297437854413752130520504347701602264758318906527890855154366159582987279682987510631200575428783453215515103870818298969791613127856265033195487140214287532698187962046936097879900350962302291026368131493195275630227837628441540360584402572114334961180023091208287046088923962328835461505776583271252546093591128203925285393434620904245248929403901706233888991085841065183173360437470737908552631764325733993712871937587746897479926305837065742830161637408969178426378624212835258112820516370298089332099905707920064367426202389783111470054074998459250360633560933883831923386783056136435351892133279732908133732642652633989763922723407882928177953580570993691049175470808931841056146322338217465637321248226383092103297701648054726243842374862411453093812206564914032751086643394517512161526545361333111314042436854805106765843493523836959653428071768775328348234345557366719731392746273629108210679280784718035329131176778924659089938635459327894523777674406192240337638674004021330343297496902028328145933418826817683893072003634795623117103101291953169794607632737589253530772552375943788434504067715555779056450443016640119462580972216729758615026968443146952034614932291105970676243268515992834709891284706740862008587135016260312071903172086094081298321581077282076353186624611278245537208532365305775956430072517744315051539600905168603220349163222640885248852433158051534849622434848299380905070483482449327453732624567755879089187190803662058009594743150052402532709746995318770724376825907419939632265984147498193609285223945039707165443156421328157688908058783183404917434556270520223564846495196112460268313970975069382648706613264507665074611512677522748621598642530711298441182622661057163515069260029861704945425047491378115154139941550671256271197133252763631939606902895650288268608362241082050562430701794976171121233066073310059947366875

You can also set command line options in the interactive environment using :set <options>. For example, we can load the rbtree example again and print out the elapsed runtime with --showtime:

> :set --showtime

> :l samples/basic/rbtree.kk
...
linking: interactive
created: .koka\v2.3.1\clang-cl-debug\interactive

> main()
...
420000
info: elapsed: 4.104s, user: 4.046s, sys: 0.062s, rss: 231mb

and then enable optimizations with -O2 and run again (on Windows with an AMD 5950X):

> :set -O2

> :r 
...
linking: interactive
created: .koka\v2.3.1\clang-cl-drelease\interactive

> main()
...
420000
info: elapsed: 0.670s, user: 0.656s, sys: 0.015s, rss: 198mb

And finally we quit the interpreter:

> :q

I think of my body as a side effect of my mind.
  -- Carrie Fisher (1956)

1.4. Samples and Editors

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 manually), you can type :e in the interactive prompt to edit your program further. For example,

> :l samples/basic/caesar
...
modules:
    samples/basic/caesar

> :e 

<edit the source and reload>

> :r
...
modules:
    samples/basic/caesar

> main()

What next?

Basic Koka syntax Browse the Library documentation

2. Why Koka?

There are many new languages being designed, but only few bring fundamentally new concepts – like Haskell with pure versus monadic programming, or Rust with borrow checking. Koka distinguishes itself through effect typing, effect handlers, and Perceus memory management:

2.1. Minimal but General

Koka has a small core set of orthogonal, well-studied language features – but each of these is as general and composable as possible, such that we do not need further “special” extensions. Core features include first-class functions, a higher-rank impredicative polymorphic type- and effect system, algebraic data types, and effect handlers.

fun hello-ten()
  var i := 0
  while { i < 10 }
    println("hello")
    i := i + 1
fun hello-ten()
  var i := 0
  while { i < 10 }
    println("hello")
    i := i + 1

As an example of the min-gen design principle, Koka implements most control-flow primitives as regular functions. An anonymous function can be written as fn(){ <body> }; but as a syntactic convenience, any function without arguments can be shortened further to use just braces, as { <body> }. Moreover, using brace elision, any indented block automatically gets curly braces.

We can write a whilestd/core/while: forall<e> (predicate : () -> <div|e> bool, action : () -> <div|e> ()) -> <div|e> () loop now using regular function calls as shown in the example, where the call to whilestd/core/while: forall<e> (predicate : () -> <div|e> bool, action : () -> <div|e> ()) -> <div|e> () is desugared to whilestd/core/while: forall<e> (predicate : () -> <div|e> bool, action : () -> <div|e> ()) -> <div|e> ()( fn(){ i < 10 }, fn(){ ... } ).

This also naturally leads to consistency: an expression between parenthesis is always evaluated before a function call, whereas an expression between braces (ah, suspenders!) is suspended and may be never evaluated or more than once (as in our example). This is inconsistent in most other languages where often the predicate of a whilestd/core/while: forall<e> (predicate : () -> <div|e> bool, action : () -> <div|e> ()) -> <div|e> () loop is written in parenthesis but may be evaluated multiple times.

Learn more about basic syntax

2.2. Effect Typing

Koka infers and tracks the effect of every function in its type – and a function type has 3 parts: the argument types, the effect type, and the type of the result. For example:

fun sqr    : (int) -> total int       // total: mathematical total function    
fun divide : (int,int) -> exn int     // exn: may raise an exception (partial)  
fun turing : (tape) -> div int        // div: may not terminate (diverge)  
fun print  : (string) -> console ()   // console: may write to the console  
fun rand   : () -> ndet int           // ndet: non-deterministic  
fun sqr    : (intstd/core/types/int: V) -> totalstd/core/total: E intstd/core/types/int: V       // total: mathematical total function    
fun divide : (intstd/core/types/int: V,intstd/core/types/int: V) -> exnstd/core/exn: HX intstd/core/types/int: V     // exn: may raise an exception (partial)  
fun turing : (tape) -> divstd/core/types/div: X intstd/core/types/int: V        // div: may not terminate (diverge)  
fun print  : (stringstd/core/types/string: V) -> consolestd/core/console: X ()   // console: may write to the console  
fun rand   : () -> ndetstd/core/types/ndet: X intstd/core/types/int: V           // ndet: non-deterministic  

The precise effect typing gives Koka rock-solid semantics and deep safety guarantees backed by well-studied category theory, which makes Koka particularly easy to reason about for both humans and compilers. (Given the importance of effect typing, the name Koka was derived from the Japanese word for effective (効果, こうか, Kōka)).

A function without any effect is called totalstd/core/total: E and corresponds to mathematically total functions – a good place to be. Then we have effects for partial functions that can raise exceptions (exnstd/core/exn: HX), and potentially non-terminating functions as divstd/core/types/div: X (divergent). The combination of exnstd/core/exn: HX and divstd/core/types/div: X is called purestd/core/pure: E as that corresponds to Haskell's notion of purity. On top of that we find mutability (as ststd/core/types/st: H -> E) up to full non-deterministic side effects in iostd/core/io: E.

Effects can be polymorphic as well. Consider mapping a function over a list:

fun map( xs : list<a>, f : a -> e b ) : e list<b> 
  match xs
    Cons(x,xx) -> Cons( f(x), map(xx,f) )
    Nil        -> Nil  
fun map( xs : liststd/core/list: V -> V<a>, f : a -> e b ) : e liststd/core/list: V -> V<b> 
  match xs
    Consstd/core/Cons: forall<a> (head : a, tail : list<a>) -> list<a>(x,xx) -> Consstd/core/Cons: forall<a> (head : a, tail : list<a>) -> list<a>( f(x), map(xx,f) )
    Nilstd/core/Nil: forall<a> list<a>        -> Nilstd/core/Nil: forall<a> list<a>  

Single letter types are polymorphic (aka, generic), and Koka infers that you map from a list of elements a to a list of elements of type b. Since map itself has no intrinsic effect, the effect of applying map is exactly the effect of the function f that is applied, namely e.

Learn more about effect types

2.3. Effect Handlers

Another example of the min-gen design principle: instead of various special language and compiler extensions to support exceptions, generators, async/await etc., Koka has full support for algebraic effect handlers – these lets you define advanced control abstractions like async/await as a user library in a typed and composable way.

Here is an example of an effect definition with one control (ctl) operation to yield intstd/core/types/int: V values:

effect yield
  ctl yield( i : int ) : bool
effect yieldwhy/yield: HX
  ctl yieldwhy/yield: (i : int) -> yield bool( ii: int : intstd/core/types/int: V ) : boolstd/core/types/bool: V

Once the effect is declared, we can use it for example to yield the elements of a list:

fun traverse( xs : list<int> ) : yield () 
  match xs 
    Cons(x,xx) -> if yield(x) then traverse(xx) else ()
    Nil        -> ()
fun traversewhy/traverse: (xs : list<int>) -> yield ()( xsxs: list<int> : liststd/core/list: V -> V<intstd/core/types/int: V> ) : yieldwhy/yield: HX (std/core/types/(): V)std/core/types/(): V 
  match xsxs: list<int> 
    Consstd/core/Cons: forall<a> (head : a, tail : list<a>) -> list<a>(xx: int,xxxx: list<int>) -> if yieldwhy/yield: (i : int) -> yield bool(xx: int) then traversewhy/traverse: (xs : list<int>) -> yield ()(xxxx: list<int>) else (std/core/types/(): ())std/core/types/(): ()
    Nilstd/core/Nil: forall<a> list<a>        -> (std/core/types/(): ())std/core/types/(): ()

The traversewhy/traverse: (xs : list<int>) -> yield () function calls yield and therefore gets the yieldwhy/yield: HX effect in its type, and if we want to use traversewhy/traverse: (xs : list<int>) -> yield (), we need to handle the yieldwhy/yield: HX effect. This is much like defining an exception handler, except we can receive values (here an intstd/core/types/int: V), and we can resume with a result (which determines if we keep traversing):

fun print-elems() : console () 
  with ctl yield(i)
    println("yielded " ++ i.show)
    resume(i<=2)
  traverse([1,2,3,4])
fun print-elemswhy/print-elems: () -> console ()() : consolestd/core/console: X (std/core/types/(): V)std/core/types/(): V 
  withhandler: (() -> <yield,console> ()) -> console () ctl yieldyield: (i : int, resume : (bool) -> console ()) -> console ()(ii: int)
    printlnstd/core/println: (s : string) -> console ()("yielded " ++std/core/(++).1: (x : string, y : string) -> string ii: int.showstd/core/show: (i : int) -> string)
    resumeresume: (bool) -> console ()(ii: int<=std/core/(<=).1: (x : int, y : int) -> bool2)
  traversewhy/traverse: (xs : list<int>) -> yield ()([std/core/Cons: forall<a> (head : a, tail : list<a>) -> list<a>1,2,3,4]std/core/Nil: forall<a> list<a>)

The with statement binds the handler for yield control operation over the rest of the scope, in this case traversewhy/traverse: (xs : list<int>) -> yield ()([1,2,3,4]). Every time yield is called, our control handler is called, prints the current value, and resumes to the call site with a boolean result (indeed, dynamic binding with static typing!). Note how the handler discharges the yieldwhy/yield: HX effect – and replaces it with a consolestd/core/console: X effect. When we run the example, we get:

yielded: 1
yielded: 2
yielded: 3

Learn more about with statements

Learn more about effect handlers

2.4. Perceus Optimized Reference Counting

Perceus is the compiler optimized reference counting technique that Koka uses for automatic memory management [11, 18]. This (together with evidence passing [19–21]) enables Koka to compile directly to plain C code without needing a garbage collector or runtime system.

Perceus uses extensive static analysis to aggressively optimize the reference counts. Here the strong semantic foundation of Koka helps a lot: inductive data types cannot form cycles, and potential sharing across threads can be reliably determined.

Normally we need to make a fundamental choice when managing memory:

• We either use manual memory management (C, C++, Rust) and we get the best performance but at a significant programming burden,
• Or, we use garbage collection (OCaml, C#, Java, Go, etc.) but but now we need a runtime system and pay a price in performance, memory usage, and unpredictable latencies.

With Perceus, we hope to cross this gap and our goal is to be within 2x of the performance of C/C++. Initial benchmarks are encouraging and show Koka to be close to C performance on various memory intensive benchmarks.

See benchmarks

Read the Perceus technical report

2.5. Reuse Analysis

Perceus also performs reuse analysis as part of reference counting analysis. This pairs pattern matches with constructors of the same size and reuses them in-place if possible. Take for example, the map function over lists:

fun map( xs : list<a>, f : a -> e b ) : e list<b>
  match xs
    Cons(x,xx) -> Cons( f(x), map(xx,f) )
    Nil        -> Nil
fun map( xs : liststd/core/list: V -> V<a>, f : a -> e b ) : e liststd/core/list: V -> V<b>
  match xs
    Consstd/core/Cons: forall<a> (head : a, tail : list<a>) -> list<a>(x,xx) -> Consstd/core/Cons: forall<a> (head : a, tail : list<a>) -> list<a>( f(x), map(xx,f) )
    Nilstd/core/Nil: forall<a> list<a>        -> Nilstd/core/Nil: forall<a> list<a>

Here the matched Consstd/core/Cons: forall<a> (head : a, tail : list<a>) -> list<a> can be reused by the new Consstd/core/Cons: forall<a> (head : a, tail : list<a>) -> list<a> in the branch. This means if we map over a list that is not shared, like list(1,100000).map(sqr).sumstd/core/sum: (xs : list<int>) -> int, then the list is updated in-place without any extra allocation. This is very effective for many functional style programs.

void map( list_t xs, function_t f, 
          list_t* res) 
{
  while (is_Cons(xs)) {
    if (is_unique(xs)) {    // if xs is not shared..
      box_t y = apply(dup(f),xs->head);      
      if (yielding()) { ... } // if f yields to a general ctl operation..
      else {
        xs->head = y;      
        *res = xs;          // update previous node in-place
        res = &xs->tail;    // set the result address for the next node
        xs = xs->tail;      // .. and continue with the next node
      }
    }
    else { ... }            // slow path allocates fresh nodes
  }
  *res = Nil;  
}

Moreover, the Koka compiler also implements tail-recursion modulo cons (TRMC) and instead of using a recursive call, the function is eventually optimized into an in-place updating loop for the fast path, similar to the C code example on the right.

Importantly, the reuse optimization is guaranteed and a programmer can see when the optimization applies. This leads to a new programming technique we call FBIP: functional but in-place. Just like tail-recursion allows us to express loops with regular function calls, reuse analysis allows us to express many imperative algorithms in a purely functional style.

Learn more about FBIP

2.6. Specialization

As another example of the effectiveness of Perceus and the strong semantics of the Koka core language, we can look at the red-black tree example and look at the code generated when folding a binary tree. The red-black tree is defined as:

type color  
  Red
  Black

type tree<k,a> 
  Leaf
  Node(color : color, left : tree<k,a>, key : k, value : a, right : tree<k,a>)
type colorwhy/color: V  
  Redwhy/Red: color
  Blackwhy/Black: color

type treewhy/tree: (V, V) -> V<kk: V,aa: V> 
  Leafwhy/Leaf: forall<a,b> tree<a,b>
  Nodewhy/Node: forall<a,b> (color : color, left : tree<a,b>, key : a, value : b, right : tree<a,b>) -> tree<a,b>(colorcolor: color : colorwhy/color: V, leftleft: tree<19,20> : treewhy/tree: (V, V) -> V<kk: V,aa: V>, keykey: 19 : kk: V, valuevalue: 20 : aa: V, rightright: tree<19,20> : treewhy/tree: (V, V) -> V<kk: V,aa: V>)

We can generically fold over a tree t with a function f as:

fun fold(t : tree<k,a>, acc : b, f : (k, a, b) -> b) : b
  match t
    Node(_,l,k,v,r) -> r.fold( f(k,v,l.fold(acc,f)), f)
    Leaf            -> acc
fun foldwhy/fold: forall<a,b,c> (t : tree<c,a>, acc : b, f : (c, a, b) -> b) -> b(tt: tree<$166,$164> : treewhy/tree: (V, V) -> V<kk: V,aa: V>, accacc: $165 : bb: V, ff: ($166, $164, $165) -> $165 : (kk: V, aa: V, bb: V) -> bstd/core/types/(<>): E) : bstd/core/types/(<>): E
  match tt: tree<$166,$164>
    Nodewhy/Node: forall<a,b> (color : color, left : tree<a,b>, key : a, value : b, right : tree<a,b>) -> tree<a,b>(_,ll: tree<$166,$164>,kk: $166,vv: $164,rr: tree<$166,$164>) -> rr: tree<$166,$164>.foldwhy/fold: forall<a,b,c> (t : tree<c,a>, acc : b, f : (c, a, b) -> b) -> b( ff: ($166, $164, $165) -> $165(kk: $166,vv: $164,ll: tree<$166,$164>.foldwhy/fold: forall<a,b,c> (t : tree<c,a>, acc : b, f : (c, a, b) -> b) -> b(accacc: $165,ff: ($166, $164, $165) -> $165)), ff: ($166, $164, $165) -> $165)
    Leafwhy/Leaf: forall<a,b> tree<a,b>            -> accacc: $165

This is used in the example to count all the Truestd/core/types/True: bool values in a tree t : treewhy/tree: (V, V) -> V<k,boolstd/core/types/bool: V> as:

val count = t.fold(0, fn(k,v,acc) if v then acc+1 else acc)
val count = t.foldwhy/fold: forall<a,b,c> (t : tree<c,a>, acc : b, f : (c, a, b) -> b) -> b(0, fn(k,v,acc) if v then acc+1 else acc)

This may look quite expensive where we pass a polymorphic first-class function that uses arbitrary precision integer arithmetic. However, the Koka compiler first specializes the foldwhy/fold: forall<a,b,c> (t : tree<c,a>, acc : b, f : (c, a, b) -> b) -> b definition to the passed function, then simplifies the resulting monomorphic code, and finally applies Perceus to insert reference count instructions. This results in the following internal core code:

fun spec-fold(t : tree<k,bool>, acc : int) : int
  match t
    Node(_,l,k,v,r) -> 
      if unique(t) then { drop(k); free(t) } else { dup(l); dup(r) } // perceus inserted
      val x = if v then 1 else 0
      spec-fold(r, spec-fold(l,acc) + x) 
    Leaf -> 
      drop(t)
      acc

val count = spec-fold(t,0)
fun spec-fold(t : treewhy/tree: (V, V) -> V<k,boolstd/core/types/bool: V>, acc : intstd/core/types/int: V) : intstd/core/types/int: V
  match t
    Nodewhy/Node: forall<a,b> (color : color, left : tree<a,b>, key : a, value : b, right : tree<a,b>) -> tree<a,b>(_,l,k,v,r) -> 
      if uniquestd/core/unique: () -> ndet int(t) then { dropstd/core/drop: forall<a> (xs : list<a>, n : int) -> list<a>(k); free(t) } else { dup(l); dup(r) } // perceus inserted
      val x = if v then 1 else 0
      spec-fold(r, spec-fold(l,acc) + x) 
    Leafwhy/Leaf: forall<a,b> tree<a,b> -> 
      dropstd/core/drop: forall<a> (xs : list<a>, n : int) -> list<a>(t)
      acc

val count = spec-fold(t,0)

When compiled via the C backend, the generated assembly instructions on arm64 become:

spec_fold:
  ...                       
  LBB15_3:   
    mov  x21, x0              ; x20 is t, x21 = acc (x19 = koka context _ctx)
  LBB15_4:                    ; the "match(t)" point
    cmp  x20, #9              ; is t a Leaf?
    b.eq LBB15_1              ;   if so, goto Leaf brach
  LBB15_5:                    ;   otherwise, this is the Cons(_,l,k,v,r) branch
    mov  x23, x20             ; load the fields of t:
    ldp  x22, x0, [x20, #8]   ;   x22 = l, x0 = k   (ldp == load pair)
    ldp  x24, x20, [x20, #24] ;   x24 = v, x20 = r  
    ldr  w8, [x23, #4]        ;   w8 = reference count (0 is unique)
    cbnz w8, LBB15_11         ; if t is not unique, goto cold path to dup the members
    tbz  w0, #0, LBB15_13     ; if k is allocated (bit 0 is 0), goto cold path to free it
  LBB15_7:                   
    mov  x0, x23              ; call free(t)  
    bl   _mi_free
  LBB15_8:              
    mov  x0, x22              ; call spec_fold(l,acc,_ctx)
    mov  x1, x21              
    mov  x2, x19
    bl   spec_fold
    cmp  x24, #1              ; boxed value is False? 
    b.eq LBB15_3              ;   if v is False, the result in x0 is the accumulator
    add  x21, x0, #4          ; otherwise add 1 (as a small int 4*n)
    orr  x8, x21, #1          ;   check for bigint or overflow in one test 
    cmp  x8, w21, sxtw        ;   (see kklib/include/integer.h for details)
    b.eq LBB15_4              ; and tail-call into spec_fold if no overflow or bigint
    mov  w1, #5               ; otherwise, use generic bigint addition              
    mov  x2, x19
    bl   _kk_integer_add_generic
    b    LBB15_3
  ...

The polymorphic foldwhy/fold: forall<a,b,c> (t : tree<c,a>, acc : b, f : (c, a, b) -> b) -> b with its higher order parameter is eventually compiled into a tight loop with close to optimal assembly instructions.

Read the technical report on garbage-free and frame-limited reuse

3. A Tour of Koka

This is a short introduction to the Koka programming language.

Koka is a function-oriented language that separates pure values from side-effecting computations (The word ‘kōka’ (or 効果) means “effect” or “effective” in Japanese). Koka is also flexible and fun: Koka has many features that help programmers to easily change their data types and code organization correctly even in large-scale programs, while having a small strongly-typed language core with a familiar brace syntax.

3.1. Basics

3.1.1. Hello world

As usual, we start with the familiar Hello world program:

fun main()
  println("Hello world!") // println output
fun maintour/main: () -> console ()()
  printlnstd/core/println: (s : string) -> console ()("Hello world!") // println output

Functions are declared using the fun keyword (and anonymous functions with fn). Due to brace elision, any indented blocks implicitly get curly braces, and the example can also be written as:

fun main() {
  println("Hello world!") // println output
}
fun maintour/main: () -> console ()() {
  println("Hello world!") // println output
}

using explicit braces. Here is another short example program that encodes a string using the Caesar cipher, where each lower-case letter in a string is replaced by the letter three places up in the alphabet:

fun main() { println(caesar("koka is fun")) }

fun encode( s : string, shift : int )
  fun encode-char(c) 
    if c < 'a' || c > 'z' then return c
    val base = (c - 'a').int
    val rot  = (base + shift) % 26
    (rot.char + 'a')  
  s.map(encode-char)

fun caesar( s : string ) : string 
  s.encode( 3 )
fun encodetour/encode: (s : string, shift : int) -> string( ss: string : stringstd/core/types/string: V, shiftshift: int : intstd/core/types/int: V )
  fun encode-charencode-char: (c : char) -> char(cc: char) 
    if cc: char <std/core/(<): (char, char) -> bool 'a' ||std/core/types/(||): (x : bool, y : bool) -> bool cc: char >std/core/(>): (char, char) -> bool 'z' then returnreturn: char cc: char
    val basebase: int = (cc: char -std/core/(-).3: (c : char, d : char) -> total char 'a').intstd/core/int: (char) -> int
    val rotrot: int  = (basebase: int +std/core/(+).4: (x : int, y : int) -> int shiftshift: int) %std/core/(%): (int, int) -> int 26
    (rotrot: int.charstd/core/char: (i : int) -> char +std/core/(+).3: (c : char, d : char) -> total char 'a')  
  ss: string.mapstd/core/map.6: forall<e> (s : string, f : (char) -> e char) -> e string(encode-charencode-char: (c : char) -> char)

fun caesartour/caesar: (s : string) -> string( ss: string : stringstd/core/types/string: V ) : stringstd/core/types/string: V 
  ss: string.encodetour/encode: (s : string, shift : int) -> string( 3 )

In this example, we declare a local function encode-char which encodes a single character c. The final statement s.map(encode-char) applies the encode-char function to each character in the string s, returning a new string where each character is Caesar encoded. The result of the final statement in a function is also the return value of that function, and you can generally leave out an explicit return keyword.

3.1.2. Dot selection

Koka is a function-oriented language where functions and data form the core of the language (in contrast to objects for example). In particular, the expression s.encodetour/encode: (s : string, shift : int) -> string(3) does not select the encodetour/encode: (s : string, shift : int) -> string method from the stringstd/core/types/string: V object, but it is simply syntactic sugar for the function call encodetour/encode: (s : string, shift : int) -> string(s,3) where s becomes the first argument. Similarly, c.int converts a character to an integer by calling int(c) (and both expressions are equivalent). The dot notation is intuïtive and quite convenient to chain multiple calls together, as in:

fun showit( s : string ) 
  s.encode(3).count.println
fun showittour/showit: (s : string) -> console ()( ss: string : stringstd/core/types/string: V ) 
  ss: string.encodetour/encode: (s : string, shift : int) -> string(3).countstd/core/count.1: (s : string) -> int.printlnstd/core/println.1: (i : int) -> console ()

for example (where the body desugars as println(count(encodetour/encode: (s : string, shift : int) -> string(s,3)))). An advantage of the dot notation as syntactic sugar for function calls is that it is easy to extend the ‘primitive’ methods of any data type: just write a new function that takes that type as its first argument. In most object-oriented languages one would need to add that method to the class definition itself which is not always possible if such class came as a library for example.

3.1.3. Type Inference

Koka is also strongly typed. It uses a powerful type inference engine to infer most types, and types generally do not get in the way. In particular, you can always leave out the types of any local variables. This is the case for example for base and rot values in the previous example; hover with the mouse over the example to see the types that were inferred by Koka. Generally, it is good practice though to write type annotations for function parameters and the function result since it both helps with type inference, and it provides useful documentation with better feedback from the compiler.

For the encodetour/encode: (s : string, shift : int) -> string function it is actually essential to give the type of the s parameter: since the map function is defined for both liststd/core/list: V -> V and stringstd/core/types/string: V types and the program is ambiguous without an annotation. Try to load the example in the editor and remove the annotation to see what error Koka produces.

3.1.4. Anonymous Functions and Trailing Lambdas

Koka also allows for anonymous function expressions using the fn keyword. For example, instead of declaring the encode-char function, we can also pass it directly to the map function as a function expression:

fun encode2( s : string, shift : int )
  s.map( fn(c)
    if c < 'a' || c > 'z' then return c
    val base = (c - 'a').int
    val rot  = (base + shift) % 26
    (rot.char + 'a')
  )
fun encode2tour/encode2: (s : string, shift : int) -> string( ss: string : stringstd/core/types/string: V, shiftshift: int : intstd/core/types/int: V )
  ss: string.mapstd/core/map.6: forall<e> (s : string, f : (char) -> e char) -> e string( fn(cc: char)
    if cc: char <std/core/(<): (char, char) -> bool 'a' ||std/core/types/(||): (x : bool, y : bool) -> bool cc: char >std/core/(>): (char, char) -> bool 'z' then returnreturn: char cc: char
    val basebase: int = (cc: char -std/core/(-).3: (c : char, d : char) -> total char 'a').intstd/core/int: (char) -> int
    val rotrot: int  = (basebase: int +std/core/(+).4: (x : int, y : int) -> int shiftshift: int) %std/core/(%): (int, int) -> int 26
    (rotrot: int.charstd/core/char: (i : int) -> char +std/core/(+).3: (c : char, d : char) -> total char 'a')
  )

It is a bit annoying we had to put the final right-parenthesis after the last brace in the previous example. As a convenience, Koka allows anonymous functions to follow the function call instead – this is also known as trailing lambdas. For example, here is how we can print the numbers 1 to 10:

fun main() { print10() }

fun print10()
  for(1,10) fn(i) {
    println(i)  
  }
fun print10tour/print10: () -> console ()()
  forstd/core/for: forall<e> (start : int, end : int, action : (int) -> e ()) -> e ()(1,10) fn(ii: int) {
    printlnstd/core/println.1: (i : int) -> console ()(ii: int)  
  }

which is desugared to forstd/core/for: forall<e> (start : int, end : int, action : (int) -> e ()) -> e ()( 1, 10, fn(i){ println(i) } ). (In fact, since we pass the i argument directly to println, we could have also passed the function itself directly, and write forstd/core/for: forall<e> (start : int, end : int, action : (int) -> e ()) -> e ()(1,10,println).)

Anonymous functions without any arguments can be shortened further by leaving out the fn keyword as well and just use braces directly. Here is an example using the repeat function:

fun main() { printhi10() }

fun printhi10()
  repeat(10) {
    println("hi")  
  }
fun printhi10tour/printhi10: () -> console ()()
  repeatstd/core/repeat.1: forall<e> (n : int, action : () -> e ()) -> e ()(10) {
    printlnstd/core/println: (s : string) -> console ()("hi")  
  }

where the body desugars to repeat( 10, fn(){println(hi)} ). The is especially convenient for the whilestd/core/while: forall<e> (predicate : () -> <div|e> bool, action : () -> <div|e> ()) -> <div|e> () loop since this is not a built-in control flow construct but just a regular function:

fun main() { print11() }

fun print11()
  var i := 10
  while { i >= 0 } {
    println(i)
    i := i - 1
  }
fun print11tour/print11: () -> <console,div> ()()
  varstd/core/hnd/local-var: forall<a,b,e,h> (init : a, action : (l : local-var<h,a>) -> <local<h>|e> b) -> <local<h>|e> b istd/core/types/local-scope: forall<a,e> (action : forall<h> () -> <local<h>|e> a) -> e a := 10
  whilestd/core/while: forall<e> (predicate : () -> <div|e> bool, action : () -> <div|e> ()) -> <div|e> () { ii: int >=std/core/(>=).1: (x : int, y : int) -> bool 0 } {
    printlnstd/core/println.1: (i : int) -> console ()(ii: int)
    ii: local-var<$2683,int> :=std/core/types/local-set: forall<a,e,h> (v : local-var<h,a>, assigned : a) -> <local<h>|e> () ii: int -std/core/(-).4: (x : int, y : int) -> int 1
  }

Note how the first argument to whilestd/core/while: forall<e> (predicate : () -> <div|e> bool, action : () -> <div|e> ()) -> <div|e> () is in braces instead of the usual parenthesis. In Koka, an expression between parenthesis is always evaluated before a function call, whereas an expression between braces (ah, suspenders!) is suspended and may be never evaluated or more than once (as in our example).

Of course, the previous examples can also use identation and elide the braces (see Section 4.3), and a more typical way of writing these is:

fun printhi10()
  repeat(10)
    println("hi")

fun print11()
  var i := 10
  while { i >= 0 }
    println(i)
    i := i - 1  
fun printhi10tour/printhi10: () -> console ()()
  repeat(10)
    println("hi")

fun print11tour/print11: () -> <console,div> ()()
  var i := 10
  whilestd/core/while: forall<e> (predicate : () -> <div|e> bool, action : () -> <div|e> ()) -> <div|e> () { i >= 0 }
    println(i)
    i := i - 1  

3.1.5. With Statements

To the best of our knowledge, Koka was the first language to have generalized trailing lambdas. It was also one of the first languages to have dot notation (This was independently developed but it turns out the D language has a similar feature (called UFCS) which predates dot-notation). Another novel syntactical feature is the with statement. With the ease of passing a function block as a parameter, these often become nested. For example:

fun twice(f) 
  f()
  f()

fun test-twice() 
  twice 
    twice
      println("hi")
fun twicetour/twice: forall<a,e> (f : () -> e a) -> e a(ff: () -> _3028 _3029) 
  ff: () -> _3028 _3029()
  ff: () -> _3028 _3029()

fun test-twicetour/test-twice: () -> console ()() 
  twicetour/twice: forall<a,e> (f : () -> e a) -> e a 
    twicetour/twice: forall<a,e> (f : () -> e a) -> e a
      printlnstd/core/println: (s : string) -> console ()("hi")

where "hi" is printed four times (note: this desugars to twicetour/twice: forall<a,e> (f : () -> e a) -> e a( fn(){ twicetour/twice: forall<a,e> (f : () -> e a) -> e a( fn(){ println("hi") }) })). Using the with statement we can write this more concisely as:

pub fun test-with1()
  with twice
  with twice
  println("hi")
pub fun test-with1tour/test-with1: () -> console ()()
  with twicetour/twice: forall<a,e> (f : () -> e a) -> e a
  with twicetour/twice: forall<a,e> (f : () -> e a) -> e a
  printlnstd/core/println: (s : string) -> console ()("hi")

The with statement essentially puts all statements that follow it into an anynomous function block and passes that as the last parameter. In general:

with f(e1,...,eN)
<body>
with f(e1,...,eN)
<body>

f(e1,...,eN, fn(){ <body> })
f(e1,...,eN, fn(){ <body> })

Moreover, a with statement can also bind a variable parameter as:

with x <- f(e1,...,eN)
<body>
with x <- f(e1,...,eN)
<body>

f(e1,...,eN, fn(x){ <body> })
f(e1,...,eN, fn(x){ <body> })

Here is an example using foreach to span over the rest of the function body:

pub fun test-with2() {
  with x <- list(1,10).foreach
  println(x)
}
pub fun test-with2tour/test-with2: () -> console ()() {
  with xx: int <- liststd/core/list: (lo : int, hi : int) -> total list<int>(1,10).foreachstd/core/foreach: forall<a,e> (xs : list<a>, action : (a) -> e ()) -> e ()
  printlnstd/core/println.1: (i : int) -> console ()(xx: int)
}

which desugars to list(1,10).foreach( fn(x){ println(x) } ). This is a bit reminiscent of Haskell do notation. Using the with statement this way may look a bit strange at first but is very convenient in practice – it helps thinking of with as a closure over the rest of the lexical scope.

With Finally

As another example, the finallystd/core/hnd/finally: forall<a,e> (fin : () -> e (), action : () -> e a) -> e a function takes as its first argument a function that is run when exiting the scope – either normally, or through an “exception” (i.e. when an effect operation does not resume). Again, with is a natural fit:

fun test-finally() 
  with finally{ println("exiting..") }
  println("entering..")
  throw("oops") + 42
fun test-finallytour/test-finally: () -> <console,exn> int() 
  with finallystd/core/hnd/finally: forall<a,e> (fin : () -> e (), action : () -> e a) -> e a{ printlnstd/core/println: (s : string) -> console ()("exiting..") }
  printlnstd/core/println: (s : string) -> console ()("entering..")
  throwstd/core/throw: forall<a> (message : string, info : ?exception-info) -> exn a("oops") +std/core/(+).4: (x : int, y : int) -> int 42

which desugars to finallystd/core/hnd/finally: forall<a,e> (fin : () -> e (), action : () -> e a) -> e a(fn(){ println... }, fn(){ println("entering"); throwstd/core/throw: forall<a> (message : string, info : ?exception-info) -> exn a("oops") + 42 }), and prints:

entering..
exiting..
uncaught exception: oops

This is another example of the min-gen principle: many languages have have special built-in support for this kind of pattern, like a defer statement, but in Koka it is all just function applications with minimal syntactic sugar.

Read more about initially and finally handlers

With Handlers

The with statement is especially useful in combination with effect handlers. An effect describes an abstract set of operations whose concrete implementation can be supplied by a handler.

Here is an example of an effect handler for emitting messages:

// Emitting messages; how to emit is TBD.  Just one abstract operation: emit.
effect fun emit(msg : string) : ()

// Emits a standard greeting.
fun hello()
  emit("hello world!")

// Emits a standard greeting to the console.
pub fun hello-console1()
  with handler
    fun emit(msg) println(msg) 
  hello()
// Emitting messages; how to emit is TBD.  Just one abstract operation: emit.
effect fun emittour/emit: (msg : string) -> emit ()(msgmsg: string : stringstd/core/types/string: V) : (std/core/types/(): V)std/core/types/(): V

// Emits a standard greeting.
fun hellotour/hello: () -> emit ()()
  emittour/emit: (msg : string) -> emit ()("hello world!")

// Emits a standard greeting to the console.
pub fun hello-console1tour/hello-console1: () -> console ()()
  with handlerhandler: (() -> <emit,console> ()) -> console ()
    fun emitemit: (msg : string) -> console ()(msgmsg: string) printlnstd/core/println: (s : string) -> console ()(msgmsg: string) 
  hellotour/hello: () -> emit ()()

In this example, the with expression desugars to (handler{ fun emit(msg){ println(msg) } })( fn(){ hellotour/hello: () -> emit ()() } ). Generally, a handler{ <ops> } expression takes as its last argument a function block so it can be used directly with with.

Moreover, as a convenience, we can leave out the handler keyword for effects that define just one operation (like emittour/emit: HX):

with val op = <expr> 
with fun op(x){ <body> }
with ctl op(x){ <body> }
with val op = <expr> 
with fun op(x){ <body> }
with ctl op(x){ <body> }

with handler{ val op = <expr> }
with handler{ fun op(x){ <body> } }
with handler{ ctl op(x){ <body> } }
with handler{ val op = <expr> }
with handler{ fun op(x){ <body> } }
with handler{ ctl op(x){ <body> } }

Using this convenience, we can write the previous example in a more concise and natural way as:

pub fun hello-console2()
  with fun emit(msg) println(msg)
  hello()
pub fun hello-console2()
  with fun emit(msg) println(msg)
  hellotour/hello: () -> emit ()()

Intuitively, we can view the handler with fun emit as a dynamic binding of the function emit over the rest of the scope.

Read more about effect handlers

Read more about val operations

3.1.6. Optional and Named Parameters

Being a function-oriented language, Koka has powerful support for function calls where it supports both optional and named parameters. For example, the function replace-allstd/core/replace-all: (s : string, pattern : string, repl : string) -> string takes a string, a pattern (named pattern), and a replacement string (named repl):

fun main() { println(world()) }

fun world() 
  replace-all("hi there", "there", "world")  // returns "hi world"
fun worldtour/world: () -> string() 
  replace-allstd/core/replace-all: (s : string, pattern : string, repl : string) -> string("hi there", "there", "world")  // returns "hi world"

Using named parameters, we can also write the function call as:

fun main() { println(world2()) }

fun world2()
  "hi there".replace-all( repl="world", pattern="there" )
fun world2tour/world2: () -> string()
  "hi there".replace-allstd/core/replace-all: (s : string, pattern : string, repl : string) -> string( repl="world", pattern="there" )

Optional parameters let you specify default values for parameters that do not need to be provided at a call-site. As an example, let's define a function sublisttour/sublist: forall<a> (xs : list<a>, start : int, len : ?int) -> list<a> that takes a list, a start position, and the length len of the desired sublist. We can make the len parameter optional and by default return all elements following the start position by picking the length of the input list by default:

fun main() { println( ['a','b','c'].sublist(1).string ) }

fun sublist( xs : list<a>, start : int, len : int = xs.length ) : list<a>
  if start <= 0 return xs.take(len)
  match xs
    Nil        -> Nil
    Cons(_,xx) -> xx.sublist(start - 1, len)
fun sublisttour/sublist: forall<a> (xs : list<a>, start : int, len : ?int) -> list<a>( xsxs: list<$7057> : liststd/core/list: V -> V<aa: V>, startstart: int : intstd/core/types/int: V, lenlen: ?int : intstd/core/types/optional: V -> V = xsxs: list<$7057>.lengthstd/core/length.1: forall<a> (xs : list<a>) -> int ) : liststd/core/list: V -> V<aa: V>
  if startstart: int <=std/core/(<=).1: (x : int, y : int) -> bool 0 returnreturn: list<$7057> xsxs: list<$7057>.takestd/core/take: forall<a> (xs : list<a>, n : int) -> list<a>(lenlen: int)std/core/types/(): ()
  match xsxs: list<$7057>
    Nilstd/core/Nil: forall<a> list<a>        -> Nilstd/core/Nil: forall<a> list<a>
    Consstd/core/Cons: forall<a> (head : a, tail : list<a>) -> list<a>(_,xxxx: list<$7057>) -> xxxx: list<$7057>.sublisttour/sublist: forall<a> (xs : list<a>, start : int, len : ?int) -> list<a>(startstart: int -std/core/(-).4: (x : int, y : int) -> int 1, lenlen: int)

Hover over the sublisttour/sublist: forall<a> (xs : list<a>, start : int, len : ?int) -> list<a> identifier to see its full type, where the len parameter has gotten an optional intstd/core/types/int: V type signified by the question mark: :?int.

3.1.7. A larger example: cracking Caesar encoding

fun main() 
  test-uncaesar()

fun encode( s : string, shift : int )
  fun encode-char(c) 
    if c < 'a' || c > 'z' return c
    val base = (c - 'a').int
    val rot  = (base + shift) % 26
    (rot.char + 'a')  
  s.map(encode-char)

// The letter frequency table for English
val english = [8.2,1.5,2.8,4.3,12.7,2.2,
               2.0,6.1,7.0,0.2,0.8,4.0,2.4,
               6.7,7.5,1.9,0.1, 6.0,6.3,9.1,
               2.8,1.0,2.4,0.2,2.0,0.1]

// Small helper functions
fun percent( n : int, m : int )
  100.0 * (n.float64 / m.float64)

fun rotate( xs, n )
  xs.drop(n) ++ xs.take(n)

// Calculate a frequency table for a string
fun freqs( s : string ) : list<float64>
  val lowers = list('a','z')
  val occurs = lowers.map( fn(c) s.count(c.string) )
  val total  = occurs.sum
  occurs.map( fn(i) percent(i,total) )

// Calculate how well two frequency tables match according
// to the _chi-square_ statistic.
fun chisqr( xs : list<float64>, ys : list<float64> ) : float64
  zipwith(xs,ys, fn(x,y) ((x - y)^2.0)/y ).foldr(0.0,(+))

// Crack a Caesar encoded string
fun uncaesar( s : string ) : string
  val table  = freqs(s)                   // build a frequency table for `s`
  val chitab = list(0,25).map fn(n)       // build a list of chisqr numbers for each shift between 0 and 25
                 chisqr( table.rotate(n), english )               

  val min    = chitab.minimum()           // find the mininal element
  val shift  = chitab.index-of( fn(f) f == min ).negate  // and use its position as our shift
  s.encode( shift )

fun test-uncaesar()
  println( uncaesar( "nrnd lv d ixq odqjxdjh" ) )
// The letter frequency table for English
val englishtour/english: list<float64> = [std/core/Cons: forall<a> (head : a, tail : list<a>) -> list<a>8.2,1.5,2.8,4.3,12.7,2.2,
               2.0,6.1,7.0,0.2,0.8,4.0,2.4,
               6.7,7.5,1.9,0.1, 6.0,6.3,9.1,
               2.8,1.0,2.4,0.2,2.0,0.1]std/core/Nil: forall<a> list<a>

// Small helper functions
fun percenttour/percent: (n : int, m : int) -> float64( nn: int : intstd/core/types/int: V, mm: int : intstd/core/types/int: V )
  100.0 *std/core/(*).1: (float64, float64) -> float64 (nn: int.float64std/core/float64: (i : int) -> float64 /std/core/(/).1: (float64, float64) -> float64 mm: int.float64std/core/float64: (i : int) -> float64)

fun rotatetour/rotate: forall<a> (xs : list<a>, n : int) -> list<a>( xsxs: list<_2845>, nn: int )
  xsxs: list<_2845>.dropstd/core/drop: forall<a> (xs : list<a>, n : int) -> list<a>(nn: int) ++std/core/(++): forall<a> (xs : list<a>, ys : list<a>) -> list<a> xsxs: list<_2845>.takestd/core/take: forall<a> (xs : list<a>, n : int) -> list<a>(nn: int)

// Calculate a frequency table for a string
fun freqstour/freqs: (s : string) -> list<float64>( ss: string : stringstd/core/types/string: V ) : liststd/core/list: V -> V<float64std/core/types/float64: V>
  val lowerslowers: list<char> = liststd/core/list.4: (lo : char, hi : char) -> total list<char>('a','z')
  val occursoccurs: list<int> = lowerslowers: list<char>.mapstd/core/map.5: forall<a,b,e> (xs : list<a>, f : (a) -> e b) -> e list<b>( fn(cc: char) ss: string.countstd/core/count: (s : string, pattern : string) -> int(cc: char.stringstd/core/string: (c : char) -> string) )
  val totaltotal: int  = occursoccurs: list<int>.sumstd/core/sum: (xs : list<int>) -> int
  occursoccurs: list<int>.mapstd/core/map.5: forall<a,b,e> (xs : list<a>, f : (a) -> e b) -> e list<b>( fn(ii: int) percenttour/percent: (n : int, m : int) -> float64(ii: int,totaltotal: int) )

// Calculate how well two frequency tables match according
// to the _chi-square_ statistic.
fun chisqrtour/chisqr: (xs : list<float64>, ys : list<float64>) -> float64( xsxs: list<float64> : liststd/core/list: V -> V<float64std/core/types/float64: V>, ysys: list<float64> : liststd/core/list: V -> V<float64std/core/types/float64: V> ) : float64std/core/types/float64: V
  zipwithstd/core/zipwith: forall<a,b,c,e> (xs : list<a>, ys : list<b>, f : (a, b) -> e c) -> e list<c>(xsxs: list<float64>,ysys: list<float64>, fn(xx: float64,yy: float64) ((xx: float64 -std/core/(-).2: (float64, float64) -> float64 yy: float64)^std/core/(^): (f : float64, p : float64) -> float642.0)/std/core/(/).1: (float64, float64) -> float64yy: float64 ).foldrstd/core/foldr: forall<a,b,e> (xs : list<a>, z : b, f : (a, b) -> e b) -> e b(0.0,(+)std/core/(+).2: (float64, float64) -> float64)

// Crack a Caesar encoded string
fun uncaesartour/uncaesar: (s : string) -> string( ss: string : stringstd/core/types/string: V ) : stringstd/core/types/string: V
  val tabletable: list<float64>  = freqstour/freqs: (s : string) -> list<float64>(ss: string)                   // build a frequency table for `s`
  val chitabchitab: list<float64> = liststd/core/list: (lo : int, hi : int) -> total list<int>(0,25).mapstd/core/map.5: forall<a,b,e> (xs : list<a>, f : (a) -> e b) -> e list<b> fn(nn: int)       // build a list of chisqr numbers for each shift between 0 and 25
                 chisqrtour/chisqr: (xs : list<float64>, ys : list<float64>) -> float64( tabletable: list<float64>.rotatetour/rotate: forall<a> (xs : list<a>, n : int) -> list<a>(nn: int), englishtour/english: list<float64> )               

  val minmin: float64    = chitabchitab: list<float64>.minimumstd/core/minimum.1: (xs : list<float64>) -> float64()           // find the mininal element
  val shiftshift: int  = chitabchitab: list<float64>.index-ofstd/core/index-of: forall<a> (xs : list<a>, pred : (a) -> bool) -> int( fn(ff: float64) ff: float64 ==std/core/(==).2: (float64, float64) -> bool minmin: float64 ).negatestd/core/negate: (i : int) -> int  // and use its position as our shift
  ss: string.encodetour/encode: (s : string, shift : int) -> string( shiftshift: int )

fun test-uncaesartour/test-uncaesar: () -> console ()()
  printlnstd/core/println: (s : string) -> console ()( uncaesartour/uncaesar: (s : string) -> string( "nrnd lv d ixq odqjxdjh" ) )

The val keyword declares a static value. In the example, the value englishtour/english: list<float64> is a list of floating point numbers (of type float64std/core/types/float64: V) denoting the average frequency for each letter. The function freqstour/freqs: (s : string) -> list<float64> builds a frequency table for a specific string, while the function chisqrtour/chisqr: (xs : list<float64>, ys : list<float64>) -> float64 calculates how well two frequency tables match. In the function crack these functions are used to find a shift value that results in a string whose frequency table matches the englishtour/english: list<float64> one the closest – and we use that to decode the string. You can try out this example directly in the interactive environment:

> :l samples/basic/caesar.kk

3.2. Effect types

A novel part about Koka is that it automatically infers all the side effects that occur in a function. The absence of any effect is denoted as totalstd/core/total: E (or <>) and corresponds to pure mathematical functions. If a function can raise an exception the effect is exnstd/core/exn: HX, and if a function may not terminate the effect is divstd/core/types/div: X (for divergence). The combination of exnstd/core/exn: HX and divstd/core/types/div: X is purestd/core/pure: E and corresponds directly to Haskell's notion of purity. Non- deterministic functions get the ndetstd/core/types/ndet: X effect. The ‘worst’ effect is iostd/core/io: E and means that a program can raise exceptions, not terminate, be non- deterministic, read and write to the heap, and do any input/output operations. Here are some examples of effectful functions:

fun square1( x : int ) : total int   { x*x }
fun square2( x : int ) : console int { println( "a not so secret side-effect" ); x*x }
fun square3( x : int ) : div int     { x * square3( x ) }
fun square4( x : int ) : exn int     { throw( "oops" ); x*x }
fun square1tour/square1: (x : int) -> total int( xx: int : intstd/core/types/int: V ) : totalstd/core/total: E intstd/core/types/int: V   { xx: int*std/core/(*): (int, int) -> intxx: int }
fun square2tour/square2: (x : int) -> console int( xx: int : intstd/core/types/int: V ) : consolestd/core/console: X intstd/core/types/int: V { printlnstd/core/println: (s : string) -> console ()( "a not so secret side-effect" ); xx: int*std/core/(*): (int, int) -> intxx: int }
fun square3tour/square3: (x : int) -> div int( xx: int : intstd/core/types/int: V ) : divstd/core/types/div: X intstd/core/types/int: V     { xx: int *std/core/(*): (int, int) -> int square3tour/square3: (x : int) -> div int( xx: int ) }
fun square4tour/square4: (x : int) -> exn int( xx: int : intstd/core/types/int: V ) : exnstd/core/exn: HX intstd/core/types/int: V     { throwstd/core/throw: forall<a> (message : string, info : ?exception-info) -> exn a( "oops" ); xx: int*std/core/(*): (int, int) -> intxx: int }

When the effect is totalstd/core/total: E we usually leave it out in the type annotation. For example, when we write:

fun square5( x : int ) : int 
  x*x
fun square5tour/square5: (x : int) -> int( xx: int : intstd/core/types/int: V ) : intstd/core/types/int: V 
  xx: int*std/core/(*): (int, int) -> intxx: int

the assumed effect is totalstd/core/total: E. Sometimes, we write an effectful function, but are not interested in explicitly writing down its effect type. In that case, we can use a wildcard type which stands for some inferred type. A wildcard type is denoted by writing an identifier prefixed with an underscore, or even just an underscore by itself:

fun square6( x : int ) : _e int
  println("I did not want to write down the \"console\" effect")
  x*x
fun square6tour/square6: (x : int) -> console int( xx: int : intstd/core/types/int: V ) : _e_e: E intstd/core/types/int: V
  printlnstd/core/println: (s : string) -> console ()("I did not want to write down the \"console\" effect")
  xx: int*std/core/(*): (int, int) -> intxx: int

Hover over square6tour/square6: (x : int) -> console int to see the inferred effect for _e.

3.2.1. Semantics of effects

The inferred effects are not just considered as some extra type information on functions. On the contrary, through the inference of effects, Koka has a very strong connection to its denotational semantics. In particular, the full type of a Koka functions corresponds directly to the type signature of the mathematical function that describes its denotational semantics. For example, using 〚t〛 to translate a type t into its corresponding mathematical type signature, we have:

In the above translation, we use as a sum where we have either a unit (i.e. exception) or a type , and we use for a product consisting of a pair of a heap and a type . From the above correspondence, we can immediately see that a totalstd/core/total: E function is truly total in the mathematical sense, while a stateful function (ststd/core/types/st: H -> E<h>) that can raise exceptions or not terminate (purestd/core/pure: E) takes an implicit heap parameter, and either does not terminate () or returns an updated heap together with either a value or an exception ().

We believe that this semantic correspondence is the true power of full effect types and it enables effective equational reasoning about the code by a programmer. For almost all other existing programming languages, even the most basic semantics immediately include complex effects like heap manipulation and divergence. In contrast, Koka allows a layered semantics where we can easily separate out nicely behaved parts, which is essential for many domains, like safe LINQ queries, parallel tasks, tier-splitting, sand-boxed mobile code, etc.

3.2.2. Combining effects

Often, a function contains multiple effects, for example: