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

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.10, Nov 28 2020, libc 64-bit (gcc)
|_|\_\\___/|_|\_\\__,_|       type :? for help

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.

1.2. Running the compiler

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

1.3. Running the interactive compiler

Without giving any input files, the interactive environment 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()

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

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

effect yield {
  control yield( i : int ) : bool
}
effect yieldwhy/yield: HX {
  control 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 (std/core/types/True: boolyieldwhy/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 control 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 () control 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: (int, 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 yieldwhy/yield: HX over the rest of the scope, in this case traversewhy/traverse: (xs : list<int>) -> yield ()([1,2,3,4]). 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 [15]. This (together with evidence translation [16]) 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 yielded an effect 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

Read the Perceus report on reuse analysis

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
}

Koka uses familiar curly-braces syntax where starts a line comment. Functions are declared using the fun keyword (and anonymous functions with fn).

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') 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 (std/core/types/True: boolcc: char <std/core/(<): (char, char) -> bool 'a' ||std/core/types/(||): (x : bool, y : bool) -> bool cc: char >std/core/(>): (char, char) -> bool 'z') returnreturn: char cc: char
    val basebase: int = (cc: char -std/core/(-).4: (c : char, d : char) -> total char 'a').intstd/core/int: (char) -> int
    val rotrot: int  = (basebase: int +std/core/(+): (int, int) -> int shiftshift: int) %std/core/(%): (int, int) -> int 26
    (rotrot: int.charstd/core/char: (int) -> char +std/core/(+).4: (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(length(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') 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 (std/core/types/True: boolcc: char <std/core/(<): (char, char) -> bool 'a' ||std/core/types/(||): (x : bool, y : bool) -> bool cc: char >std/core/(>): (char, char) -> bool 'z') returnreturn: char cc: char
    val basebase: int = (cc: char -std/core/(-).4: (c : char, d : char) -> total char 'a').intstd/core/int: (char) -> int
    val rotrot: int  = (basebase: int +std/core/(+): (int, int) -> int shiftshift: int) %std/core/(%): (int, int) -> int 26
    (rotrot: int.charstd/core/char: (int) -> char +std/core/(+).4: (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<e,a> (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: (int, int) -> bool 0 } {
    printlnstd/core/println.1: (i : int) -> console ()(ii: int)
    ii: local-var<$3011,int> :=std/core/types/local-set: forall<a,e,h> (v : local-var<h,a>, assigned : a) -> <local<h>|e> () ii: int -std/core/(-): (int, 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).

3.1.5. With Statements

To the best of our knowledge, Koka was the first language to have generalized dot notation and trailing lambdas. 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( fn(){
    twice( fn(){
      println("hi")
    })
  })
}
fun twicetour/twice: forall<a,e> (f : () -> e a) -> e a(ff: () -> _3532 _3533) {
  ff: () -> _3532 _3533()
  ff: () -> _3532 _3533()
}

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

where "hi" is printed four times. Using the with statement we can write this more concisely as:

public fun test-with1() {
  with twice
  with twice
  println("hi")
}
public 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 examply using foreach to span over the rest of the function body:

public fun test-with2() {
  with x = list(1,10).foreach
  println(x)
}
public 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 it 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/(+): (int, 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"); throw("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. Generally, a handler{ <ops> } expression takes as its last argument a function block so it can be used directly with with. Here is an example of an effect handler for emitting messages:

effect fun emit(msg : string) : ()

fun hello() {
  emit("hello world!")
}

public fun emit-console1() {
  with handler{ fun emit(msg){ println(msg) } }
  hello()
}
effect fun emittour/emit: (msg : string) -> emit ()(msgmsg: string : stringstd/core/types/string: V) : (std/core/types/(): V)std/core/types/(): V

fun hellotour/hello: () -> emit ()() {
  emittour/emit: (msg : string) -> emit ()("hello world!")
}

public fun emit-console1tour/emit-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 desugars to (handler{ fun emit(msg){ println(msg) } })( fn(){ hellotour/hello: () -> emit ()() } ).

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 except op(x){ <body> }
with control op(x){ <body> }
with val op = <expr> 
with fun op(x){ <body> }
with except op(x){ <body> }
with control op(x){ <body> }

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

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

public fun emit-console2() {
  with fun emit(msg){ println(msg) }
  hello()
}
public fun emit-console2tour/emit-console2: () -> console ()() {
  withhandler: (() -> <emit,console> ()) -> console () fun emitemit: (msg : string) -> console ()(msgmsg: string){ printlnstd/core/println: (s : string) -> console ()(msgmsg: string) }
  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<$8136> : liststd/core/list: V -> V<aa: V>, startstart: int : intstd/core/types/int: V, lenlen: ?int : intstd/core/types/optional: V -> V = xsxs: list<$8136>.lengthstd/core/length.1: forall<a> (xs : list<a>) -> int ) : liststd/core/list: V -> V<aa: V> {
  if (std/core/types/True: boolstartstart: int <=std/core/(<=).1: (int, int) -> bool 0) returnreturn: list<$8136> xsxs: list<$8136>.takestd/core/take: forall<a> (xs : list<a>, n : int) -> list<a>(lenlen: int)std/core/types/(): ()
  match(xsxs: list<$8136>) {
    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<$8136>) -> xxxx: list<$8136>.sublisttour/sublist: forall<a> (xs : list<a>, start : int, len : ?int) -> list<a>(startstart: int -std/core/(-): (int, 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 )
{
  function 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.double / m.double)
}

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

// Calculate a frequency table for a string
fun freqs( s : string ) : list<double> {
  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<double>, ys : list<double> ) : double {
  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<double> = [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) -> double( nn: int : intstd/core/types/int: V, mm: int : intstd/core/types/int: V ) {
  100.0 *std/core/(*).1: (double, double) -> double (nn: int.doublestd/core/double: (int) -> double /std/core/(/).1: (double, double) -> double mm: int.doublestd/core/double: (int) -> double)
}

fun rotatetour/rotate: forall<a> (xs : list<a>, n : int) -> list<a>( xsxs: list<_3219>, nn: int ) {
  xsxs: list<_3219>.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<_3219>.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<double>( ss: string : stringstd/core/types/string: V ) : liststd/core/list: V -> V<doublestd/core/types/double: V> {
  val lowerslowers: list<char> = liststd/core/list.2: (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) -> double(ii: int,totaltotal: int) } )
}

// Calculate how well two frequency tables match according
// to the _chi-square_ statistic.
fun chisqrtour/chisqr: (xs : list<double>, ys : list<double>) -> double( xsxs: list<double> : liststd/core/list: V -> V<doublestd/core/types/double: V>, ysys: list<double> : liststd/core/list: V -> V<doublestd/core/types/double: V> ) : doublestd/core/types/double: 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<double>,ysys: list<double>, fn(xx: double,yy: double){ ((xx: double -std/core/(-).3: (double, double) -> double yy: double)^std/core/(^): (d : double, p : double) -> double2.0)/std/core/(/).1: (double, double) -> doubleyy: double } ).foldrstd/core/foldr: forall<a,b,e> (xs : list<a>, z : b, f : (a, b) -> e b) -> e b(0.0,(+)std/core/(+).3: (double, double) -> double)
}

// 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<double>  = freqstour/freqs: (s : string) -> list<double>(ss: string)                   // build a frequency table for `s`
  val chitabchitab: list<double> = 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<double>, ys : list<double>) -> double( tabletable: list<double>.rotatetour/rotate: forall<a> (xs : list<a>, n : int) -> list<a>(nn: int), englishtour/english: list<double> )
               })
  val minmin: double    = chitabchitab: list<double>.minimumstd/core/minimum.1: (xs : list<double>) -> double()           // find the mininal element
  val shiftshift: int  = chitabchitab: list<double>.index-ofstd/core/index-of: forall<a> (xs : list<a>, pred : (a) -> bool) -> int( fn(ff: double){ ff: double ==std/core/(==).2: (double, double) -> bool minmin: double } ).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<double> is a list of floating point numbers (of type doublestd/core/types/double: V) denoting the average frequency for each letter. The function freqstour/freqs: (s : string) -> list<double> builds a frequency table for a specific string, while the function chisqrtour/chisqr: (xs : list<double>, ys : list<double>) -> double 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<double> 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:

fun combine-effects() {
  val i = srandom-int() // non-deterministic
  throw("oops")         // exception raising
  combine-effects()     // and non-terminating
}
fun combine-effectstour/combine-effects: forall<a> () -> <pure,ndet> a() {
  val ii: int = srandom-intstd/num/random/srandom-int: () -> ndet int() // non-deterministic
  throwstd/core/throw: forall<a> (message : string, info : ?exception-info) -> exn a("oops")         // exception raising
  combine-effectstour/combine-effects: () -> <exn,ndet,div> _5155()     // and non-terminating
}

The effect assigned to combine-effectstour/combine-effects: forall<a> () -> <pure,ndet> a are ndetstd/core/types/ndet: X, divstd/core/types/div: X, and exnstd/core/exn: HX. We can write such combination as a row of effects as <divstd/core/types/div: X,exnstd/core/exn: HX,ndetstd/core/types/ndet: X>. When you hover over the combine-effectstour/combine-effects: forall<a> () -> <pure,ndet> a identifiers, you will see that the type inferred is really <purestd/core/pure: E,ndetstd/core/types/ndet: X> where purestd/core/pure: E is a type alias defined as

alias pure = <div,exn>
alias purestd/core/pure: E = <divstd/core/types/div: X,exnstd/core/exn: HX>

3.2.3. Polymorphic effects

Many functions are polymorphic in their effect. For example, the mapstd/core/map: forall<a,b,e> (xs : list<a>, f : (a) -> e b) -> e list<b> function applies a function f to each element of a (finite) list. As such, the effect depends on the effect of f, and the type of map becomes:

map : (xs : list<a>, f : (a) -> e b) -> e list<b>
map : (xs : liststd/core/list: V -> V<a>, f : (a) -> e b) -> e liststd/core/list: V -> V<b>

We use single letters (possibly followed by digits) for polymorphic types. Here, the map functions takes a list with elements of some type a, and a function f that takes an element of type a and returns a new element of type b. The final result is a list with elements of type b. Moreover, the effect of the applied function e is also the effect of the map function itself; indeed, this function has no other effect by itself since it does not diverge, nor raises exceptions.

We can use the notation <l|e> to extend an effect e with another effect l. This is used for example in the whilestd/core/while: forall<e> (predicate : () -> <div|e> bool, action : () -> <div|e> ()) -> <div|e> () function which has type: whilestd/core/while: forall<e> (predicate : () -> <div|e> bool, action : () -> <div|e> ()) -> <div|e> () : ( pred : () -> <divstd/core/types/div: X|e> boolstd/core/types/bool: V, action : () -> <divstd/core/types/div: X|e> () ) -> <divstd/core/types/div: X|e> (). The whilestd/core/while: forall<e> (predicate : () -> <div|e> bool, action : () -> <div|e> ()) -> <div|e> () function takes a predicate function and an action to perform, both with effect <divstd/core/types/div: X|e>. Indeed, since while may diverge depending on the predicate its effect must include divergence.

The reader may be worried that the type of whilestd/core/while: forall<e> (predicate : () -> <div|e> bool, action : () -> <div|e> ()) -> <div|e> () forces the predicate and action to have exactly the same effect <divstd/core/types/div: X|e>, which even includes divergence. However, when effects are inferred at the call-site, both the effects of predicate and action are extended automatically until they match. This ensures we take the union of the effects in the predicate and action. Take for example the following loop

fun looptest() {
  while { is-odd(srandom-int()) } {
    throw("odd")
  }
}
fun looptesttour/looptest: () -> <pure,ndet> ()() {
  whilestd/core/while: forall<e> (predicate : () -> <div|e> bool, action : () -> <div|e> ()) -> <div|e> () { is-oddstd/core/is-odd: (int) -> bool(srandom-intstd/num/random/srandom-int: () -> ndet int()) } {
    throwstd/core/throw: forall<a> (message : string, info : ?exception-info) -> exn a("odd")
  }
}

Koka infers that the predicate odd(srandom-int()) has effect <ndetstd/core/types/ndet: X|e1> while the action has effect <exnstd/core/exn: HX|e2> for some e1 and e2. When applying whilestd/core/while: forall<e> (predicate : () -> <div|e> bool, action : () -> <div|e> ()) -> <div|e> (), those effects are unified to the type <exnstd/core/exn: HX,ndetstd/core/types/ndet: X,divstd/core/types/div: X|e3> for some e3.

3.2.4. Local Mutable Variables

The Fibonacci numbers are a sequence where each subsequent Fibonacci number is the sum of the previous two, where fibtour/fib: (n : int) -> div int(0) == 0 and fibtour/fib: (n : int) -> div int(1) == 1. We can easily calculate Fibonacci numbers using a recursive function:

fun main() { println(fib(10)) }

fun fib(n : int) : div int {
  if (n <= 0)   then 0
  elif (n == 1) then 1
  else fib(n - 1) + fib(n - 2)
}
fun fibtour/fib: (n : int) -> div int(nn: int : intstd/core/types/int: V) : divstd/core/types/div: X intstd/core/types/int: V {
  if (std/core/types/True: boolnn: int <=std/core/(<=).1: (int, int) -> bool 0)   then 0
  elif (std/core/types/True: boolnn: int ==std/core/(==).1: (int, int) -> bool 1) then 1
  else fibtour/fib: (n : int) -> div int(nn: int -std/core/(-): (int, int) -> int 1) +std/core/(+): (int, int) -> int fibtour/fib: (n : int) -> div int(nn: int -std/core/(-): (int, int) -> int 2)
}

Note that the type inference engine is currently not powerful enough to prove that this recursive function always terminates, which leads to inclusion of the divergence effect divstd/core/types/div: X in the result type.

Here is another version of the Fibonacci function but this time implemented using local mutable variables. We use the repeat function to iterate n times:

fun main() { println(fib2(10)) }

fun fib2(n) {
  var x := 0
  var y := 1
  repeat(n) {
    val y0 = y
    y := x+y
    x := y0
  }
  x
}
fun fib2tour/fib2: (n : int) -> int(nn: int) {
  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 xstd/core/types/local-scope: forall<e,a> (action : forall<h> () -> <local<h>|e> a) -> e a := 0
  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 yy: local-var<$2244,int> := 1
  repeatstd/core/repeat.1: forall<e> (n : int, action : () -> e ()) -> e ()(nn: int) {
    val y0y0: int = yy: int
    yy: local-var<$2244,int> :=std/core/types/local-set: forall<a,e,h> (v : local-var<h,a>, assigned : a) -> <local<h>|e> () xx: int+std/core/(+): (int, int) -> intyy: int
    xx: local-var<$2244,int> :=std/core/types/local-set: forall<a,e,h> (v : local-var<h,a>, assigned : a) -> <local<h>|e> () y0y0: int
  }
  xx: int
}