The Koka Programming Language
(Daan Leijen, 2021-10-16)

koka-logo

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

Note: Koka v2 is a research language that is currently under development and not ready for production use. Nevertheless, the language is stable and the compiler implements the full specification. The main things lacking at the moment are libraries, package management, and deep IDE integration.

News:

  • 2021-09-01 (pinned) The ICFP'21 tutorial “Programming with Effect Handlers and FBIP in Koka” is now available on youtube.

  • 2021-10-15: Koka v2.3.2 released, with initial wasm support (use --target=wasm, and install emscripten and wasmtime), improved reuse specialization (by Anton Lorenzen), and various bug fixes.

  • 2021-09-29: Koka v2.3.1 released, with improved TRMC optimizations, and improved reuse (the rbtree benchmark is as fast as C++ now), and faster effect operations. Experimental: allow elision of -> in anonymous function expressions (e.g. xs.map( fn(x) x + 1 )) and operation clauses. Command line options changed a bit with .koka as the standard output directory.

  • 2021-09-20: Koka v2.3.0 released, with new brace elision and if/match conditions without parenthesis. Updated the javascript backend using ES6 modules and BigInt. new module std/num/int64, improved effect operation performance.

  • 2021-09-05: Koka v2.2.1 released, with initial parallel tasks, the binary-trees benchmark, and brace elision.

  • 2021-08-26: Koka v2.2.0 released, improved simplification (by Rashika B), cross-module specialization (Steven Fontanella), and borrowing annotations with improved reuse analysis (Anton Lorenzen).

  • 2021-08-26: At 12:30 EST was the live Koka tutorial at ICFP'21, see it on youtube.

  • 2021-08-23: “Generalized Evidence Passing for Effect Handlers”, by Ningning Xie and Daan Leijen presented at ICFP'21. See it on youtube or read the paper.

  • 2021-08-22: “First-class Named Effect Handlers”, by Youyou Cong, Ningning Xie, and Daan Leijen presented at HOPE'21. See it on youtube or read the paper.

  • 2021-06-23: Koka v2.1.9 released, initial cross-module specialization (by Steven Fontanella).

  • 2021-06-17: Koka v2.1.8 released, initial Apple M1 support.

  • The Perceus paper won a distinguished paper award at PLDI'21!

  • 2021-06-10: Koka v2.1.6 released.

  • 2021-05-31: Koka v2.1.4 released.

  • 2021-05-01: Koka v2.1.2 released.

  • 2021-03-08: Koka v2.1.1 released.

  • 2021-02-14: Koka v2.0.16 released.

  • 2020-12-12: Koka v2.0.14 released.

  • 2020-12-02: Koka v2.0.12 released.

  • 2020-11-29: Perceus technical report publised (pdf).

1.1. Installing the compiler

For Linux (x64, arm64) and macOS (x64, M1), you can install Koka using:

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

For 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

This also installs syntax highlighting for the VS Code and Atom editors.

After installation, verify if Koka installed correctly:

$ koka
 _         _
| |       | |
| | _ ___ | | _ __ _
| |/ / _ \| |/ / _' |  welcome to the koka interactive compiler
|   ( (_) |   ( (_| |  version 2.3.1, Sep 21 2021, 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/double
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

perceus3

Perceus is the compiler optimized reference counting technique that Koka uses for automatic memory management [15]. This (together with evidence passing [16, 17]) 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.

perceus-perf

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

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/(-).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: (i : 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' 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/(-).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: (i : 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<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<$2694,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).

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( fn(){
    twice( fn(){
      println("hi")
    })
  })
}
fun twicetour/twice: forall<a,e> (f : () -> e a) -> e a(ff: () -> _3078 _3079) {
  ff: () -> _3078 _3079()
  ff: () -> _3078 _3079()
}

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:

translation

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

$\mathpre{\rightsquigarrow}$

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

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

translation

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

$\mathpre{\rightsquigarrow}$

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:

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):

translation

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

$\mathpre{\rightsquigarrow}$

with handler{ val op = <expr> }
with handler{ fun op(x){ <body> } }
with handler{ brk op(x){ <body> } }
with handler{ ctl op(x){ <body> } }
with handler{ val op = <expr> }
with handler{ fun op(x){ <body> } }
with handler{ brk op(x){ <body> } }
with handler{ ctl 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-console2() {
  with fun emit(msg){ println(msg) }
  hellotour/hello: () -> emit ()()
}

or using brace elision 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<$7196> : liststd/core/list: V -> V<aa: V>, startstart: int : intstd/core/types/int: V, lenlen: ?int : intstd/core/types/optional: V -> V = xsxs: list<$7196>.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<$7196> xsxs: list<$7196>.takestd/core/take: forall<a> (xs : list<a>, n : int) -> list<a>(lenlen: int)std/core/types/(): ()
  match xsxs: list<$7196>
    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<$7196>) -> xxxx: list<$7196>.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 )
  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.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: (i : int) -> double /std/core/(/).1: (double, double) -> double mm: int.doublestd/core/double: (i : int) -> double)

fun rotatetour/rotate: forall<a> (xs : list<a>, n : int) -> list<a>( xsxs: list<_2856>, nn: int )
  xsxs: list<_2856>.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<_2856>.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.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) -> 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:

intstd/core/types/int: V -> totalstd/core/total: E intstd/core/types/int: V =   $\mathpre{\mathbb{Z}~\rightarrow \mathbb{Z}}$
intstd/core/types/int: V -> exnstd/core/exn: HX intstd/core/types/int: V = $\mathpre{\mathbb{Z}~\rightarrow (\mathbb{Z}~+~1)}$
intstd/core/types/int: V -> purestd/core/pure: E intstd/core/types/int: V = $\mathpre{\mathbb{Z}~\rightarrow (\mathbb{Z}~+~1)_\bot}$
intstd/core/types/int: V -> <ststd/core/types/st: H -> E<h>,purestd/core/pure: E> intstd/core/types/int: V = $\mathpre{(\mathbb{Z}~\times \mathbb{H})~\rightarrow ((\mathbb{Z}~+~1)~\times \mathbb{H})_\bot}$

In the above translation, we use $\mathpre{1~+~\tau}$ as a sum where we have either a unit $\mathpre{1}$ (i.e. exception) or a type $\mathpre{\tau}$, and we use $\mathpre{\mathbb{H}\times \tau}$ for a product consisting of a pair of a heap and a type $\mathpre{\tau}$. 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 ($\mathpre{\bot}$) or returns an updated heap together with either a value or an exception ($\mathpre{1}$).

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> _4535()     // 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 nn: int <=std/core/(<=).1: (x : int, y : int) -> bool 0   then 0
  elif nn: int ==std/core/(==).1: (x : int, y : 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<a,e> (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<$2012,int> := 1
  repeatstd/core/repeat.1: forall<e> (n : int, action : () -> e ()) -> e ()(nn: int)
    val y0y0: int = yy: int
    yy: local-var<$2012,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<$2012,int> :=std/core/types/local-set: forall<a,e,h> (v : local-var<h,a>, assigned : a) -> <local<h>|e> () y0y0: int
  xx: int

In contrast to a val declaration that binds an immutable value (as in val y0 = y), a var declaration declares a mutable variable, where the (:=) operator can assign a new value to the variable. Internally, the var declarations use a state effect handler which ensures that the state has the proper semantics even if resuming multiple times.

However, that also means that mutable local variables are not quite first-class and we cannot pass them as parameters to other functions for example (as they are always dereferenced). The lifetime of mutable local variable cannot exceed its lexical scope. For example, you get a type error if a local variable escapes through a function expression:

fun wrong() : (() -> console ())
  var x := 1
  (fn(){ x := x + 1; println(x) })
fun wrong() : (() -> consolestd/core/console: X ())
  var x := 1
  (fn(){ x := x + 1; println(x) })

This restriction allows for a clean semantics but also for (future) optimizations that are not possible for general mutable reference cells.

Read more about state and multiple resumptions

3.2.5. Reference Cells and Isolated state

Koka also has first-class heap allocated mutable reference cells. A reference to an integer is allocated using val r = refstd/core/types/ref: forall<a,h> (value : a) -> (alloc<h>) ref<h,a>(0) (since the reference itself is actually a value!), and can be dereferenced using the bang operator, as !r. We can write the Fibonacci function using reference cells as:

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

fun fib3(n)
  val x = ref(0)
  val y = ref(1)
  repeat(n) 
    val y0 = !y
    y := !x + !y
    x := y0
  !x
fun fib3tour/fib3: (n : int) -> int(nn: int)
  val xx: ref<_2168,int> = refstd/core/types/ref: forall<a,h> (value : a) -> (alloc<h>) ref<h,a>(0)
  val yy: ref<_2168,int> = refstd/core/types/ref: forall<a,h> (value : a) -> (alloc<h>) ref<h,a>(1)
  repeatstd/core/repeat.1: forall<e> (n : int, action : () -> e ()) -> e ()(nn: int) 
    val y0y0: int = !std/core/types/(!): forall<h,a,e> (ref : ref<h,a>) -> <read<h>|e> a with hdiv<h,a,e>yy: ref<_2168,int>
    yy: ref<_2168,int> :=std/core/types/set: forall<a,h> (ref : ref<h,a>, assigned : a) -> (write<h>) () !std/core/types/(!): forall<h,a,e> (ref : ref<h,a>) -> <read<h>|e> a with hdiv<h,a,e>xx: ref<_2168,int> +std/core/(+): (int, int) -> int !std/core/types/(!): forall<h,a,e> (ref : ref<h,a>) -> <read<h>|e> a with hdiv<h,a,e>yy: ref<_2168,int>
    xx: ref<_2168,int> :=std/core/types/set: forall<a,h> (ref : ref<h,a>, assigned : a) -> (write<h>) () y0y0: int
  !std/core/types/(!): forall<h,a,e> (ref : ref<h,a>) -> <read<h>|e> a with hdiv<h,a,e>xx: ref<_2168,int>

As we can see, using var declarations are generally preferred as these behave better under multiple resumptions, but also are syntactically more concise as they do not need a dereferencing operator. (Nevertheless, we still need reference cells as those are first-class while var variables cannot be passed to other functions.)

When we look at the types inferred for the references, we see that x and y have type refstd/core/types/ref: (H, V) -> V<h,intstd/core/types/int: V> which stands for a reference to a mutable value of type intstd/core/types/int: V in some heap h. The effects on heaps are allocation as heap<h>, reading from a heap as readstd/core/types/read: H -> X<h> and writing to a heap as writestd/core/types/write: H -> X<h>. The combination of these effects is called stateful and denoted with the alias ststd/core/types/st: H -> E<h>.

Clearly, the effect of the body of fib3tour/fib3: (n : int) -> int is ststd/core/types/st: H -> E<h>; but when we hover over fib3tour/fib3: (n : int) -> int, we see the type inferred is actually the totalstd/core/total: E effect: (n:intstd/core/types/int: V) -> intstd/core/types/int: V. Indeed, even though fib3tour/fib3: (n : int) -> int is stateful inside, its side-effects can never be observed. It turns out that we can safely discard the ststd/core/types/st: H -> E<h> effect whenever the heap type h cannot be referenced outside this function, i.e. it is not part of an argument or return type. More formally, the Koka compiler proves this by showing that a function is fully polymorphic in the heap type h and applies the runstd/core/types/run: forall<e,a> (action : forall<h> () -> <alloc<h>,read<h>,write<h>|e> a) -> e a function (corresponding to runST in Haskell) to discard the ststd/core/types/st: H -> E<h> effect.

The Garsia-Wachs algorithm is nice example where side-effects are used internally across function definitions and data structures, but where the final algorithm itself behaves like a pure function, see the samples/basic/garsia-wachs.kk.

3.3. Data Types

3.3.1. Structs

An important aspect of a function-oriented language is to be able to define rich data types over which the functions work. A common data type is that of a struct or record. Here is an example of a struct that contains information about a person:

struct person
  age : int
  name : string
  realname : string = name

val brian = Person( 29, "Brian" )
struct persontour/person: V
  ageage: int : intstd/core/types/int: V
  namename: string : stringstd/core/types/string: V
  realnamerealname: string : stringstd/core/types/string: V = namename: string

val briantour/brian: person = Persontour/Person: (age : int, name : string, realname : ?string) -> person( 29, "Brian" )

Every struct (and other data types) come with constructor functions to create instances, as in Persontour/Person: (age : int, name : string, realname : string) -> person(19,"Brian"). Moreover, these constructors can use named arguments so we can also call the constructor as Persontour/Person: (age : int, name : string, realname : string) -> person( nametour/name: (person : person) -> string = "Brian", agetour/age: (person : person) -> int = 19, realnametour/realname: (person : person) -> string = "Brian H. Griffin" ) which is quite close to regular record syntax but without any special rules; it is just functions all the way down!

Also, Koka automatically generates accessor functions for each field in a struct (or other data type), and we can access the agetour/age: (person : person) -> int of a persontour/person: V as briantour/brian: person.agetour/age: (person : person) -> int (which is of course just syntactic sugar for agetour/age: (person : person) -> int(briantour/brian: person)).

3.3.2. Copying

By default, all structs (and other data types) are immutable. Instead of directly mutating a field in a struct, we usually return a new struct where the fields are updated. For example, here is a birthdaytour/birthday: (p : person) -> person function that increments the agetour/age: (person : person) -> int field:

fun main() { println( brian.birthday.age ) }

struct person  
  age : int
  name : string
  realname : string = name 

val brian = Person( 29, "Brian" )

fun birthday( p : person ) : person
  p( age = p.age + 1 )
fun birthdaytour/birthday: (p : person) -> person( pp: person : persontour/person: V ) : persontour/person: V
  pp: person( age = pp: person.agetour/age: (person : person) -> int +std/core/(+): (int, int) -> int 1 )

Here, birthdaytour/birthday: (p : person) -> person returns a fresh persontour/person: V which is equal to p but with the agetour/age: (person : person) -> int incremented. The syntax p(...) is syntactic sugar for calling the copy constructor of a persontour/person: V. This constructor is also automatically generated for each data type, and is internally generated as:

fun main() { println( brian.copy().age ) }

struct person( age : int, name : string, realname : string = name )

val brian = Person( 29, "Brian" )

fun copy( p, age = p.age, name = p.name, realname = p.realname )
  return Person(age, name, realname)
fun copytour/copy: (p : person, age : ?int, name : ?string, realname : ?string) -> person( pp: person, ageage: ?int = pp: person.agetour/age: (person : person) -> int, namename: ?string = pp: person.nametour/name: (person : person) -> string, realnamerealname: ?string = pp: person.realnametour/realname: (person : person) -> string )
  returnreturn: person Persontour/Person: (age : int, name : string, realname : ?string) -> person(ageage: int, namename: string, realnamerealname: string)

When arguments follow a data value, as in p( age = age + 1), it is expanded to call this copy function, as in p.copytour/copy: (p : person, age : ?int, name : ?string, realname : ?string) -> person( agetour/age: (person : person) -> int = p.agetour/age: (person : person) -> int+1 ). In adherence with the min-gen principle, there are no special rules for record updates but using plain function calls with optional and named parameters.

3.3.3. Alternatives (or Unions)

Koka also supports algebraic data types where there are multiple alternatives. For example, here is an enumeration:

type color  
  Red
  Green
  Blue
type color  
  Red
  Green
  Blue

Special cases of these enumerated types are the voidstd/core/types/void: V type which has no alternatives (and therefore there exists no value with this type), the unit type () which has just one constructor, also written as () (and therefore, there exists only one value with the type (), namely ()), and finally the boolean type boolstd/core/types/bool: V with two constructors Truestd/core/types/True: bool and Falsestd/core/types/False: bool.

type void

type ()  
  ()

type bool  
  False
  True
type voidstd/core/types/void: V

type ()  
  ()

type boolstd/core/types/bool: V  
  Falsestd/core/types/False: bool
  Truestd/core/types/True: bool

Constructors can have parameters. For example, here is how to create a number type which is either an integer or the infinity value:

type number
  Infinity
  Integer( i : int )
type number
  Infinity
  Integer( i : intstd/core/types/int: V )

We can create such number by writing Integer(1) or Infinity. Moreover, data types can be polymorphic and recursive. Here is the definition of the liststd/core/list: V -> V type which is either empty (Nilstd/core/Nil: forall<a> list<a>) or is a head element followed by a tail list (Consstd/core/Cons: forall<a> (head : a, tail : list<a>) -> list<a>):

type list<a>
  Nil
  Cons{ head : a; tail : list<a> }
type liststd/core/list: V -> V<a>
  Nilstd/core/Nil: forall<a> list<a>
  Consstd/core/Cons: forall<a> (head : a, tail : list<a>) -> list<a>{ head : a; tail : liststd/core/list: V -> V<a> }

Koka automatically generates accessor functions for each named parameter. For lists for example, we can access the head of a list as Consstd/core/Cons: forall<a> (head : a, tail : list<a>) -> list<a>(1,Nilstd/core/Nil: forall<a> list<a>).head.

We can now also see that struct types are just syntactic sugar for regular a type with a single constructor of the same name as the type:

translation

struct tp { <fields> }
struct tp { <fields> }

$\mathpre{\rightsquigarrow}$

type tp { 
  con Tp { <fields> }
}
type tp { 
  con Tp { <fields> }
}

For example, our earlier persontour/person: V struct, defined as

struct person{ age : int; name : string; realname : string = name }
struct persontour/person: V{ agetour/age: (person : person) -> int : intstd/core/types/int: V; nametour/name: (person : person) -> string : stringstd/core/types/string: V; realnametour/realname: (person : person) -> string : stringstd/core/types/string: V = nametour/name: (person : person) -> string }

desugars to:

type person
  Person{ age : int; name : string; realname : string = name }
type persontour/person: V
  Persontour/Person: (age : int, name : string, realname : string) -> person{ agetour/age: (person : person) -> int : intstd/core/types/int: V; nametour/name: (person : person) -> string : stringstd/core/types/string: V; realnametour/realname: (person : person) -> string : stringstd/core/types/string: V = nametour/name: (person : person) -> string }

3.3.4. Matching

Todo

3.3.5. Extensible Data Types

Todo

3.3.6. Inductive, Co-inductive, and Recursive Types

For the purposes of equational reasoning and termination checking, a type declaration is limited to finite inductive types. There are two more declarations, namely co type and rec type that allow for co-inductive types, and arbitrary recursive types respectively.

3.3.7. Value Types

Value types are (non-recursive) data types that are not heap allocated but passed on the stack as a value. Since data types are immutable, semantically these types are equivalent but value types can be more efficient as they avoid heap allocation and reference counting (or more expensive as they need copying instead of sharing a reference).

By default, any non-recursive inductive datatype of a size upto 3 machine words (= 24 bytes on a 64-bit platform) is treated as a value type. For example, tuples and 3-tuples are passed and returned by value. Usually, that means that such tuples are for example returned in registers when compiling with optimization.

We can also force a type to be compiled as a value type by using the value keyword in front of a type or struct declaration:

value struct argb{ alpha: int; color-red: int; color-green: int; color-blue: int }
value struct argbtour/argb: V{ alphaalpha: int: intstd/core/types/int: V; color-redcolor-red: int: intstd/core/types/int: V; color-greencolor-green: int: intstd/core/types/int: V; color-bluecolor-blue: int: intstd/core/types/int: V }

advanced

Boxing

To support generic polymorphism, sometimes value types are boxed. For example, a list is polymorpic in its elements. That means that if we construct a list of tuples, like [(1,Truestd/core/types/True: bool)], that the element (1,2) will be boxed and heap allocated – essentially the compiler transforms this expression into [Boxstd/core/types/Box: forall<a> (unbox : a) -> box<a>((1,Truestd/core/types/True: bool)] internally.

Note that for regular data types and intstd/core/types/int: V's boxing is free (as in isomorphic). Moreover, value types up to 63 bits (on a 64-bit platform) are boxed in-place and do not require heap allocation (like int32std/core/types/int32: V). The doublestd/core/types/double: V type is also specialized; by default the Koka compiler only heap allocates doubles when their absolute value is outside the range 2-511 up to 2512 (excluding infinity and NaN)).

For performance sensitive code we may specialize certain polymorphic datatypes to reduce allocations due to boxing. For example:

type mylist 
  MyCons{ head1: int; head2: bool; mytail: mylist }
  MyNil
type mylisttour/mylist: V 
  MyConstour/MyCons: (head1 : int, head2 : bool, mytail : mylist) -> mylist{ head1head1: int: intstd/core/types/int: V; head2head2: bool: boolstd/core/types/bool: V; mytailmytail: mylist: mylisttour/mylist: V }
  MyNiltour/MyNil: mylist

Our previous example becomes MyConstour/MyCons: (head1 : int, head2 : bool, mytail : mylist) -> mylist(1,Truestd/core/types/True: bool,MyNiltour/MyNil: mylist) now and is more efficient as it only needs one allocation for the MyConstour/MyCons: (head1 : int, head2 : bool, mytail : mylist) -> mylist without an indirection to a tuple. In the future we hope to extend Koka to perform specialization automatically or by using special directives.

3.4. Effect Handlers

Effect handlers [8, 14] are a novel way to define control-flow abstractions and dynamic binding as user defined handlers – no need anymore to add special compiler extensions for exceptions, iterators, async-await, probabilistic programming, etc. Moreover, these handlers can be composed freely so the interaction between, say, async-await and exceptions as well-defined.

3.4.1. Handling

Let's start with defining an exception effect of our own. The effect declaration defines a new type together with operations, for now we use a control (ctl) operation:

effect raise
  ctl raise( msg : string ) : a
effect raisetour/raise: HX
  ctl raisetour/raise: forall<a> (msg : string) -> raise a( msgmsg: string : stringstd/core/types/string: V ) : aa: V

This defines an effect type raisetour/raise: HX together with an operation raise of type (msg : stringstd/core/types/string: V) -> raisetour/raise: HX a. With the effect signature declared, we can already use the operations:

fun safe-divide( x : int, y : int ) : raise int 
  if y==0 then raise("div-by-zero") else x / y
fun safe-dividetour/safe-divide: (x : int, y : int) -> raise int( xx: int : intstd/core/types/int: V, yy: int : intstd/core/types/int: V ) : raisetour/raise: HX intstd/core/types/int: V 
  if yy: int==std/core/(==).1: (x : int, y : int) -> bool0 then raisetour/raise: forall<a> (msg : string) -> raise a("div-by-zero") else xx: int /std/core/(/): (x : int, y : int) -> int yy: int

where we see that the safe-dividetour/safe-divide: (x : int, y : int) -> raise int function gets the raisetour/raise: HX effect (since we use the raise operation in the body). Such an effect type means that we can only evaluate the function in a context where raisetour/raise: HX is handled (in other words, where it is “dynamically bound”, or where we “have the raisetour/raise: HX capability”).

We can handle the effect by giving a concrete definition for the raise operation. For example, we may always return a default value:

fun raise-const() : int
  with handler
    ctl raise(msg){ 42 }
  8 + safe-divide(1,0)
fun raise-consttour/raise-const: () -> int() : intstd/core/types/int: V
  with handlerhandler: (() -> raise int) -> int
    ctl raiseraise: (msg : string, resume : (_6790) -> _6789 int) -> _6789 int(msgmsg: string){ 42 }
  8 +std/core/(+): (int, int) -> int safe-dividetour/safe-divide: (x : int, y : int) -> raise int(1,0)

The call raise-consttour/raise-const: () -> int() evaluates to 42 (not 50). When a raise is called (in safe-dividetour/safe-divide: (x : int, y : int) -> raise int), it will yield to its innermost handler, unwind the stack, and only then evaluate the operation definition – in this case just directly returning 42 from the point where the handler is defined. Now we can see why it is called a control operation as raise changes the regular linear control-flow and yields right back to its innermost handler from the original call site. Also note that raise-consttour/raise-const: () -> int is totalstd/core/total: E again and the handler discharged the raisetour/raise: HX effect.

The handler{ <ops> } expression is a function that itself expects a function argument over which the handler is scoped, as in (handler{ <ops> })(action). This works well in combination with the with statement of course. As a syntactic convenience, for single operations we can leave out the handler keyword which is translated as:

translation

with ctl op(<args>){ <body> }
with ctl op(<args>){ <body> }

$\mathpre{\rightsquigarrow}$

with handler 
  ctl op(<args>){ <body> }
with handler 
  ctl op(<args>){ <body> }

With this translation, we can write the previous example more concisely as:

fun raise-const1() : int 
  with ctl raise(msg){ 42 }
  8 + safe-divide(1,0)
fun raise-const1tour/raise-const1: () -> int() : intstd/core/types/int: V 
  withhandler: (() -> raise int) -> int ctl raiseraise: (msg : string, resume : (_6850) -> _6849 int) -> _6849 int(msgmsg: string){ 42 }
  8 +std/core/(+): (int, int) -> int safe-dividetour/safe-divide: (x : int, y : int) -> raise int(1,0)

which eventually expands to (handler{ ctl raise(msg){ 42 } })(fn(){ 8 + safe-dividetour/safe-divide: (x : int, y : int) -> raise int(1,0) }).

We have a similar syntactic convenience for effects with one operation where the name of the effect and operation are the same. We can define such an effect by just declaring its operation which implicitly declares an effect type of the same name:

translation

effect ctl op(<parameters>) : <result-type>
effect ctl op(<parameters>) : <result-type>

$\mathpre{\rightsquigarrow}$

effect op {
  ctl op(<parameters>) : <result-type>
}
effect op {
  ctl op(<parameters>) : <result-type>
}

That means we can declare our raisetour/raise: HX effect signature also more concisely as:

effect ctl raise( msg : string ) : a
effect ctl raise( msg : stringstd/core/types/string: V ) : a

Read more about the with statement

3.4.2. Resuming

The power of effect handlers is not just that we can yield to the innermost handler, but that we can also resume back to the call site with a result.

Let's define a asktour/ask: V -> HX<a> effect that allows us to get a contextual value of type a:

effect ask<a>                   // or: effect<a> ctl ask() : a
  ctl ask() : a

fun add-twice() : ask<int> int 
  ask() + ask()
effect asktour/ask: V -> HX<aa: V>                   // or: effect<a> ctl ask() : a
  ctl asktour/ask: forall<a> () -> (ask<a>) a() : aa: V

fun add-twicetour/add-twice: () -> (ask<int>) int() : asktour/ask: V -> HX<intstd/core/types/int: V> intstd/core/types/int: V 
  asktour/ask: forall<a> () -> (ask<a>) a() +std/core/(+): (int, int) -> int asktour/ask: forall<a> () -> (ask<a>) a()

The add-twicetour/add-twice: () -> (ask<int>) int function can ask for numbers but it is unaware of how these are provided – the effect signature just specifies an contextual API. We can handle it by always resuming with a constant for example:

fun ask-const() : int
  with ctl ask(){ resume(21) }
  add-twice()
fun ask-consttour/ask-const: () -> int() : intstd/core/types/int: V
  withhandler: (() -> (ask<int>) int) -> int ctl askask: (resume : (int) -> int) -> int(){ resumeresume: (int) -> int(21) }
  add-twicetour/add-twice: () -> (ask<int>) int()

where ask-consttour/ask-const: () -> int() evaluates to 42. Or by returning random values, like:

fun ask-random() : random int 
  with ctl ask(){ resume(random-int()) }
  add-twice()
fun ask-randomtour/ask-random: () -> random int() : randomstd/num/random/random: HX intstd/core/types/int: V 
  withhandler: (() -> <ask<int>,random> int) -> random int ctl askask: (resume : (int) -> random int) -> random int(){ resumeresume: (int) -> random int(random-intstd/num/random/random-int: () -> random int()) }
  add-twicetour/add-twice: () -> (ask<int>) int()

where ask-randomtour/ask-random: () -> random int() now handled the asktour/ask: V -> HX<intstd/core/types/int: V> effect, but itself now has randomstd/num/random/random: HX effect (see std/num/random). The resumestd/core/hnd/resume: forall<a,e,e1,b> (r : resume-context<a,e,e1,b>, x : a) -> e b function is implicitly bound by a ctl operation and resumes back to the call-site with the given result.

As we saw in the exception example, we do not need to call resumestd/core/hnd/resume: forall<a,e,e1,b> (r : resume-context<a,e,e1,b>, x : a) -> e b and can also directly return into our handler scope. For example, we may only want to handle a ask once, but after that give up:

fun ask-once() : int
  var count := 0
  with ctl ask()
    count := count + 1
    if count <= 1 then resume(42) else 0   
  add-twice()
fun ask-oncetour/ask-once: () -> int() : intstd/core/types/int: V
  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 countstd/core/types/local-scope: forall<a,e> (action : forall<h> () -> <local<h>|e> a) -> e a := 0
  withhandler: (() -> <ask<int>,local<$3432>> int) -> (local<$3432>) int ctl askask: (resume : (int) -> (local<$3432>) int) -> (local<$3432>) int()
    countcount: local-var<$3432,int> :=std/core/types/local-set: forall<a,e,h> (v : local-var<h,a>, assigned : a) -> <local<h>|e> () countcount: int +std/core/(+): (int, int) -> int 1
    if countcount: int <=std/core/(<=).1: (x : int, y : int) -> bool 1 then resumeresume: (int) -> (local<$3432>) int(42) else 0   
  add-twicetour/add-twice: () -> (ask<int>) int()

Here ask-oncetour/ask-once: () -> int() evaluates to 0 since the second call to ask does not resume, (and returns directly 0 in the ask-oncetour/ask-once: () -> int context). This pattern can for example be used to implement the concept of fuel in a setting where a computation is only allowed to take a limited amount of steps.

Read more about var mutable variables

3.4.3. Tail-Resumptive Operations

A ctl operation is one of the most general ways to define operations since we get a first-class resumestd/core/hnd/resume: forall<a,e,e1,b> (r : resume-context<a,e,e1,b>, x : a) -> e b function. However, almost all operations in practice turn out to be tail-resumptive: that is, they resume exactly once with their final result value. To make this more convenient, we can declare fun operations that do this by construction, i.e.

translation

with fun op(<args>){ <body> }
with fun op(<args>){ <body> }

$\mathpre{\rightsquigarrow}$

with ctl op(<args>){ val f = fn(){ <body> }; resume( f() ) }
with ctl op(<args>){ val f = fn(){ <body> }; resumestd/core/hnd/resume: forall<a,e,e1,b> (r : resume-context<a,e,e1,b>, x : a) -> e b( f() ) }

(The translation is defined via an intermediate function f so return works as expected).

With this syntactic sugar, we can write our earlier ask-consttour/ask-const: () -> int example using a fun operation instead:

fun ask-const2() : int 
  with fun ask(){ 21 }
  add-twice()
fun ask-const2tour/ask-const2: () -> int() : intstd/core/types/int: V 
  withhandler: (() -> (ask<int>) int) -> int fun askask: () -> int(){ 21 }
  add-twicetour/add-twice: () -> (ask<int>) int()

This also conveys better that even though ask is dynamically bound, it behaves just like a regular function without changing the control-flow.

Moreover, operations declared as fun are much more efficient than general ctl operations. The Koka compiler uses (generalized) evidence passing [16, 17] to pass down handler information to each call-site. At the call to ask in add-twicetour/add-twice: () -> (ask<int>) int, it selects the handler from the evidence vector and when the operation is a tail-resumptive fun, it calls it directly as a regular function (except with an adjusted evidence vector for its context). Unlike a general ctl operation, there is no need to yield upward to the handler, capture the stack, and eventually resume again. This gives fun (and val) operations a performance cost very similar to virtual method calls which can be quite efficient.

For even a bit more performance, you can also declare upfront that any operation definition must be tail-resumptive, as:

effect ask<a>
  fun ask() : a
effect asktour/ask: V -> HX<a>
  fun ask() : a

This restricts all handler definitions for the asktour/ask: V -> HX effect to use fun definitions for the ask operation. However, it increases the ability to reason about the code, and the compiler can optimize such calls a bit more as it no longer needs to check at run-time if the handler happens to define the operation as tail-resumptive.

advancedFor even better performance, one can mark the effect as linear (Section 3.4.12). Such effects are statically guaranteed to never use a general control operation and never need to capture a resumption. This removes the need for the monadic transformation and improves performance of any effect polymorphic function that uses such effects as well (like map or foldrstd/core/foldr: forall<a,b,e> (xs : list<a>, z : b, f : (a, b) -> e b) -> e b). Examples of linear effects are state (st) and builtin effects (like io or console).

Value Operations

A common subset of operations always tail-resume with a single value; these are essentially dynamically bound variables (but statically typed!). Such operations can be declared as a val with the following translation:

translation

with val v = <expr>
with val v = <expr>

$\mathpre{\rightsquigarrow}$

val x = <expr>
with fun v(){ x }
val x = <expr>
with fun v(){ x }

$\mathpre{\rightsquigarrow}$

val x = <expr>
with ctl v(){ resume(x) }
val x = <expr>
with ctl v(){ resumestd/core/hnd/resume: forall<a,e,e1,b> (r : resume-context<a,e,e1,b>, x : a) -> e b(x) }

For an example of the use of value operations, consider a pretty printer that produces pretty strings from documents:

fun pretty( d : doc ) : string
fun prettytour/pretty: (d : doc) -> width string( d : doctour/doc: V ) : stringstd/core/types/string: V

Unfortunately, it has a hard-coded maximum display width of 40 deep down in the code of prettytour/pretty: (d : doc) -> width string:

fun pretty-internal( line : string ) : string
  line.truncate(40)
fun pretty-internaltour/pretty-internal: (line : string) -> width string( line : stringstd/core/types/string: V ) : stringstd/core/types/string: V
  line.truncatestd/core/truncate: (s : string, count : int) -> string(40)

To abstract over the width we have a couple of choices: we could make the width a regular parameter but now we need to explicitly add the parameter to all functions in the library and manually thread them around. Another option is a global mutable variable but that leaks side-effects and is non-modular.

Or, we can define it as a value operation instead:

effect val width : int
effect val widthtour/width: value<int> : intstd/core/types/int: V

This also allows us to refer to the width operation as if is a regular value (even though internally it invokes the operation). So, the check for the width in the pretty printer can be written as:

fun pretty-internal( line : string ) : width string
  line.truncate(width)
fun pretty-internaltour/pretty-internal: (line : string) -> width string( lineline: string : stringstd/core/types/string: V ) : widthtour/width: HX1 stringstd/core/types/string: V
  lineline: string.truncatestd/core/truncate: (s : string, count : int) -> string(widthtour/width: value<int>)

When using the pretty printer we can bind the width as a regular effect handler:

fun pretty-thin(d : doc) : string
  with val width = 40
  pretty(d)
fun pretty-thintour/pretty-thin: (d : doc) -> string(dd: doc : doctour/doc: V) : stringstd/core/types/string: V
  withhandler: (() -> width string) -> string val widthwidth: () -> int = 40
  prettytour/pretty: (d : doc) -> width string(dd: doc)

Note that we did not need to change the structure of the original library functions. However the types of the functions still change to include the widthtour/width: HX1 effect as these now require the width value to be handled at some point. For example, the type of prettytour/pretty: (d : doc) -> width string becomes:

fun pretty( d : doc ) : width string
fun prettytour/pretty: (d : doc) -> width string( d : doctour/doc: V ) : widthtour/width: HX1 stringstd/core/types/string: V

as is requires the widthtour/width: HX1 effect to be handled (aka, the "dynamic binding for width : intstd/core/types/int: V to be defined“, aka, the ”widthtour/width: HX1 capability").

3.4.4. Abstracting Handlers

As another example, a writer effect is quite common where values are collected by a handler. For example, we can define an emittour/emit: HX effect to emit messages:

effect fun emit( msg : string ) : ()
effect fun emit( msg : stringstd/core/types/string: V ) : ()
fun ehello() : emit ()
  emit("hello")
  emit("world")
fun ehellotour/ehello: () -> emit ()() : emittour/emit: HX (std/core/types/(): V)std/core/types/(): V
  emittour/emit: (msg : string) -> emit ()("hello")
  emittour/emit: (msg : string) -> emit ()("world")

We can define for example a handler that prints the emitted messages directly to the console:

fun ehello-console() : console ()
  with fun emit(msg){ println(msg) }
  ehello()
fun ehello-consoletour/ehello-console: () -> console ()() : consolestd/core/console: X (std/core/types/(): V)std/core/types/(): V
  withhandler: (() -> <emit,console> ()) -> console () fun emitemit: (msg : string) -> console ()(msgmsg: string){ printlnstd/core/println: (s : string) -> console ()(msgmsg: string) }
  ehellotour/ehello: () -> emit ()()

Here the handler is defined directly, but we can also abstract the handler for emitting to the console into a separate function:

fun emit-console( action )
  with fun emit(msg){ println(msg) }
  action()
fun emit-consoletour/emit-console: forall<a,e> (action : () -> <console,emit|e> a) -> <console|e> a( actionaction: () -> <console,emit|_5112> _5075 )
  withhandler: (() -> <emit,console|_5112> _5075) -> <console|_5112> _5075 fun emitemit: (msg : string) -> <console|_5112> ()(msgmsg: string){ printlnstd/core/println: (s : string) -> console ()(msgmsg: string) }
  actionaction: () -> <console,emit|_5112> _5075()

where emit-consoletour/emit-console: forall<a,e> (action : () -> <console,emit|e> a) -> <console|e> a has the inferred type (action : () -> <emittour/emit: HX,consolestd/core/console: X|e> a) -> <consolestd/core/console: X|e> a (hover over the source to see the inferred types) where the action can have use the effects emittour/emit: HX, consolestd/core/console: X, and any other effects e, and where the final effect is just <consolestd/core/console: X|e> as the emittour/emit: HX effect is discharged by the handler.

Note, we could have written the above too as:

val emit-console2 = handler
  fun emit(msg){ println(msg) }
val emit-console2tour/emit-console2.1: forall<a,e> (() -> <console,emit|e> a) -> <console|e> a = handlerhandler: forall<a,e> (() -> <console,emit|e> a) -> <console|e> a
  fun emitemit: (msg : string) -> <console|_5325> ()(msgmsg: string){ printlnstd/core/println: (s : string) -> console ()(msgmsg: string) }

since a handler{ ... } expression is a function itself (and thus a value). Generally we prefer the earlier definition though as it allows further parameters like an initial state.

Since with works generally, we can use the abstracted handlers just like regular handlers, and our earlier example can be written as:

fun ehello-console2() : console ()
  with emit-console
  ehello()
fun ehello-console2tour/ehello-console2: () -> console ()() : consolestd/core/console: X (std/core/types/(): V)std/core/types/(): V
  with emit-consoletour/emit-console: forall<a,e> (action : () -> <console,emit|e> a) -> <console|e> a
  ehellotour/ehello: () -> emit ()()

(which expands to emit-consoletour/emit-console: forall<a,e> (action : () -> <console,emit|e> a) -> <console|e> a( fn(){ ehellotour/ehello: () -> emit ()() } )). Another useful handler may collect all emitted messages as a list of lines:

fun emit-collect( action : () -> <emit|e> () ) : e string
  var lines := []
  with handler
    return(x)    { lines.reverse.join("\n") }
    fun emit(msg){ lines := Cons(msg,lines) }  
  action()

fun ehello-commit() : string
  with emit-collect
  ehello()
fun emit-collecttour/emit-collect: forall<e> (action : () -> <emit|e> ()) -> e string( actionaction: () -> <emit|$4754> () : () -> <emittour/emit: HX|std/core/types/(<|>): (X, E) -> Eee: E> (std/core/types/(): V)std/core/types/(): V ) : ee: E stringstd/core/types/string: V
  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 linesstd/core/types/local-scope: forall<a,e> (action : forall<h> () -> <local<h>|e> a) -> e a := [std/core/Nil: forall<a> list<a>]std/core/Nil: forall<a> list<a>
  with handlerhandler: (() -> <emit,local<$4758>|$4754> ()) -> <local<$4758>|$4754> string
    return(xx: _4767)    { lineslines: list<string>.reversestd/core/reverse: forall<a> (xs : list<a>) -> list<a>.joinstd/core/join.3: (xs : list<string>, sep : string) -> string("\n") }
    fun emitemit: (msg : string) -> <local<$4758>|$4754> ()(msgmsg: string){ lineslines: local-var<$4758,list<string>> :=std/core/types/local-set: forall<a,e,h> (v : local-var<h,a>, assigned : a) -> <local<h>|e> () Consstd/core/Cons: forall<a> (head : a, tail : list<a>) -> list<a>(msgmsg: string,lineslines: list<string>) }  
  actionaction: () -> <emit|$4754> ()()

fun ehello-committour/ehello-commit: () -> string() : stringstd/core/types/string: V
  with emit-collecttour/emit-collect: forall<e> (action : () -> <emit|e> ()) -> e string
  ehellotour/ehello: () -> emit ()()

This is a total handler and only discharges the emittour/emit: HX effect.

Read more about the with statement

Read more about var mutable variables

As another example, consider a generic catch handler that applies an handling function when raisetour/raise: HX is called on our exception example:

fun catch( hnd : (string) -> e a, action : () -> <raise|e> a ) : e a 
  with ctl raise(msg){ hnd(msg) }
  action()
fun catchtour/catch: forall<a,e> (hnd : (string) -> e a, action : () -> <raise|e> a) -> e a( hndhnd: (string) -> $3772 $3771 : (stringstd/core/types/string: V) -> ee: E aa: V, actionaction: () -> <raise|$3772> $3771 : () -> <raisetour/raise: HX|std/core/types/(<|>): (X, E) -> Eee: E> aa: V ) : ee: E aa: V 
  withhandler: (() -> <raise|$3772> $3771) -> $3772 $3771 ctl raiseraise: (msg : string, resume : (_3777) -> $3772 $3771) -> $3772 $3771(msgmsg: string){ hndhnd: (string) -> $3772 $3771(msgmsg: string) }
  actionaction: () -> <raise|$3772> $3771()

We can use it now conveniently with a with statement to handle exceptional situations:

fun catch-example()
  with catch fn(msg){ println("error: " ++ msg); 42 }
  safe-divide(1,0)
fun catch-exampletour/catch-example: () -> console int()
  with catchtour/catch: forall<a,e> (hnd : (string) -> e a, action : () -> <raise|e> a) -> e a fn(msgmsg: string){ printlnstd/core/println: (s : string) -> console ()("error: " ++std/core/(++).1: (x : string, y : string) -> string msgmsg: string); 42 }
  safe-dividetour/safe-divide: (x : int, y : int) -> raise int(1,0)

advancedThe catch handler has an interesting type where the action can have a raisetour/raise: HX effect (() -> <raisetour/raise: HX|e> a) and maybe further effects e, while the handling function hnd only has effect e. Now consider supplying a handing function that itself calls raise: in that case, the type of catch would be instantiated to: (hnd: (stringstd/core/types/string: V) -> <raisetour/raise: HX> a, action : () -> <raisetour/raise: HX, raisetour/raise: HX> a ) : <raisetour/raise: HX> a. This is correct: the (outer) raisetour/raise: HX effect of action is handled and discharged, but since the handling function hnd can still cause raise to be called, the final effect still contains raisetour/raise: HX.

Here we see that Koka allows duplicate effect labels [7] where action has an instantiated <raisetour/raise: HX,raisetour/raise: HX> effect type. These kind of types occur naturally in the presence of polymorphic effects, and there is a natural correspondence to the structure of the evidence vectors at runtime (with entries for each nested effect handler). Intuitively, the action effect expresses that its outer (left-most) raisetour/raise: HX is handled, but that there may be other exceptions that are not handled – in this case from the handling function hnd, but they can also be masked exceptions (as described in Section 3.4.7).

3.4.5. Return Operations

In the previous emit-collecttour/emit-collect: forall<e> (action : () -> <emit|e> ()) -> e string example we saw the use of a return operation. Such operation changes the final result of the action of a handler. For example, consider our earlier used-defined exception effect raisetour/raise: HX. We can define a general handler that transforms any exceptional action into one that returns a maybestd/core/types/maybe: V -> V type:

fun raise-maybe( action : () -> <raise|e> a ) : e maybe<a>
  with handler
    return(x){ Just(x) }       // normal return: wrap in Just
    ctl raise(msg){ Nothing }  // exception: return Nothing directly  
  action()


fun div42()
  (raise-maybe{ safe-divide(1,0) }).default(42)
fun raise-maybetour/raise-maybe: forall<a,e> (action : () -> <raise|e> a) -> e maybe<a>( actionaction: () -> <raise|$4611> $4610 : () -> <raisetour/raise: HX|std/core/types/(<|>): (X, E) -> Eee: E> aa: V ) : ee: E maybestd/core/types/maybe: V -> V<aa: V>
  with handlerhandler: (() -> <raise|$4611> $4610) -> $4611 maybe<$4610>
    return(xx: _4614){ Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>(xx: _4614) }       // normal return: wrap in Just
    ctl raiseraise: (msg : string, resume : (_4623) -> _4622 maybe<_4614>) -> _4622 maybe<_4614>(msgmsg: string){ Nothingstd/core/types/Nothing: forall<a> maybe<a> }  // exception: return Nothing directly  
  actionaction: () -> <raise|$4611> $4610()


fun div42tour/div42: () -> int()
  (raise-maybetour/raise-maybe: forall<a,e> (action : () -> <raise|e> a) -> e maybe<a>{ safe-dividetour/safe-divide: (x : int, y : int) -> raise int(1,0) }).defaultstd/core/default: forall<a> (m : maybe<a>, nothing : a) -> a(42)

(where the body of div42tour/div42: () -> int desugars to default( raise-maybetour/raise-maybe: forall<a,e> (action : () -> <raise|e> a) -> e maybe<a>(fn(){ safe-dividetour/safe-divide: (x : int, y : int) -> raise int(1,0) }), 42 )).

Read more about function block expressions

Read more about dot expressions

A State Effect

For more examples of the use of return operations, we look at a the state effect. In its most general form it has just a set and gettour/get: forall<a> () -> (state<a>) a operation:

effect state<a>
  fun get() : a
  fun set( x : a ) : ()

fun sumdown( sum : int = 0 ) : <state<int>,div> int
  val i = get()
  if i <= 0 then sum else 
    set( i - 1 )
    sumdown( sum + i )
effect statetour/state: V -> HX<aa: V>
  fun gettour/get: forall<a> () -> (state<a>) a() : aa: V
  fun settour/set: forall<a> (x : a) -> (state<a>) ()( xx: $4159 : aa: V ) : (std/core/types/(): V)std/core/types/(): V

fun sumdowntour/sumdown: (sum : ?int) -> <div,state<int>> int( sumsum: ?int : intstd/core/types/optional: V -> V = 0 ) : <std/core/types/(<>): Estatetour/state: V -> HX<intstd/core/types/int: V>,divstd/core/types/div: X> intstd/core/types/int: V
  val ii: int = gettour/get: forall<a> () -> (state<a>) a()
  if ii: int <=std/core/(<=).1: (x : int, y : int) -> bool 0 then sumsum: int else 
    settour/set: forall<a> (x : a) -> (state<a>) ()( ii: int -std/core/(-): (int, int) -> int 1 )
    sumdowntour/sumdown: (sum : ?int) -> <state<int>,div> int( sumsum: int +std/core/(+): (int, int) -> int ii: int )

We can define a generic state handler most easily by using var declarations:

fun state( init : a, action : () -> <state<a>,div|e> b ) : <div|e> b 
  var st := init
  with handler
    fun get() { st }
    fun set(i){ st := i }
  action()
fun statetour/state: forall<a,b,e> (init : a, action : () -> <state<a>,div|e> b) -> <div|e> b( initinit: $6983 : aa: V, actionaction: () -> <state<$6983>,div|$6985> $6984 : () -> <statetour/state: V -> HX<aa: V>,divstd/core/types/div: X|std/core/types/(<|>): (X, E) -> Eee: E> bb: V ) : <divstd/core/types/div: X|std/core/types/(<|>): (X, E) -> Eee: E> bb: V 
  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 ststd/core/types/local-scope: forall<a,e> (action : forall<h> () -> <local<h>|e> a) -> e a := initinit: $6983
  with handlerhandler: (() -> <state<$6983>,local<$6989>,div|$6985> $6984) -> <local<$6989>,div|$6985> $6984
    fun getget: () -> <local<$6989>,div|$6985> $6983() { stst: $6983 }
    fun setset: (i : $6983) -> <local<$6989>,div|$6985> ()(ii: $6983){ stst: local-var<$6989,$6983> :=std/core/types/local-set: forall<a,e,h> (v : local-var<h,a>, assigned : a) -> <local<h>|e> () ii: $6983 }
  actionaction: () -> <state<$6983>,div|$6985> $6984()

where state(10){ sumdowntour/sumdown: (sum : ?int) -> <div,state<int>> int() } evaluates to 55.

Read more about default parameters

Read more about trailing lambdas

Read more about var mutable variables

Building on the previous state example, suppose we also like to return the final state. A nice way to do this is to use a return operation again to pair the final result with the final state:

fun pstate( init : a, action : () -> <state<a>,div|e> b ) : <div|e> (b,a)
  var st := init
  with handler     
    return(x) { (x,st) }      // pair with the final state
    fun get() { st }
    fun set(i){ st := i }
  action()
fun pstatetour/pstate: forall<a,b,e> (init : a, action : () -> <state<a>,div|e> b) -> <div|e> (b, a)( initinit: $4187 : aa: V, actionaction: () -> <state<$4187>,div|$4189> $4188 : () -> <statetour/state: V -> HX<aa: V>,divstd/core/types/div: X|std/core/types/(<|>): (X, E) -> Eee: E> bb: V ) : <divstd/core/types/div: X|std/core/types/(<|>): (X, E) -> Eee: E> (std/core/types/(,): (V, V) -> Vbb: V,aa: V)std/core/types/(,): (V, V) -> V
  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 ststd/core/types/local-scope: forall<a,e> (action : forall<h> () -> <local<h>|e> a) -> e a := initinit: $4187
  with handlerhandler: (() -> <state<$4187>,local<$4193>,div|$4189> $4188) -> <local<$4193>,div|$4189> ($4188, $4187)     
    return(xx: _4202) { (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)xx: _4202,stst: $4187)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b) }      // pair with the final state
    fun getget: () -> <local<$4193>,div|$4189> $4187() { stst: $4187 }
    fun setset: (i : $4187) -> <local<$4193>,div|$4189> ()(ii: $4187){ stst: local-var<$4193,$4187> :=std/core/types/local-set: forall<a,e,h> (v : local-var<h,a>, assigned : a) -> <local<h>|e> () ii: $4187 }
  actionaction: () -> <state<$4187>,div|$4189> $4188()

where pstatetour/pstate: forall<a,b,e> (init : a, action : () -> <state<a>,div|e> b) -> <div|e> (b, a)(10){ sumdowntour/sumdown: (sum : ?int) -> <div,state<int>> int() } evaluates to (55,0).

advancedIt is even possible to have a handler that only contains a single return operation: such handler handles no effect at all but only transforms the final result of a function. For example, we can define the previous example also with a separate return handler as:

fun pstate2( init : a, action : () -> <state<a>,div|e> b ) : <div|e> (b,a) 
  var st := init
  with return(x){ (x,st) }
  with handler 
    fun get() { st }
    fun set(i){ st := i }
  action()
fun pstate2tour/pstate2: forall<a,b,e> (init : a, action : () -> <state<a>,div|e> b) -> <div|e> (b, a)( initinit: $6580 : aa: V, actionaction: () -> <state<$6580>,div|$6582> $6581 : () -> <statetour/state: V -> HX<aa: V>,divstd/core/types/div: X|std/core/types/(<|>): (X, E) -> Eee: E> bb: V ) : <divstd/core/types/div: X|std/core/types/(<|>): (X, E) -> Eee: E> (std/core/types/(,): (V, V) -> Vbb: V,aa: V)std/core/types/(,): (V, V) -> V 
  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 ststd/core/types/local-scope: forall<a,e> (action : forall<h> () -> <local<h>|e> a) -> e a := initinit: $6580
  with return(xx: $6581){ (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)xx: $6581,stst: $6580)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b) }
  with handlerhandler: (() -> <state<$6580>,local<$6586>,div|$6582> $6581) -> <local<$6586>,div|$6582> $6581 
    fun getget: () -> <local<$6586>,div|$6582> $6580() { stst: $6580 }
    fun setset: (i : $6580) -> <local<$6586>,div|$6582> ()(ii: $6580){ stst: local-var<$6586,$6580> :=std/core/types/local-set: forall<a,e,h> (v : local-var<h,a>, assigned : a) -> <local<h>|e> () ii: $6580 }
  actionaction: () -> <state<$6580>,div|$6582> $6581()

Here it as a bit contrived but it can make certain programs more concise in their definition, see for example [4].

3.4.6. Combining Handlers

advancedWhat makes effect handlers a good control-flow abstraction? There are three fundamental advantages with regard to other approaches:

  1. Effect handlers can have simple (Hindley-Milner) types. This unlike shift/reset for example as that needs type rules with answer types (as the type of shift depends on the context of its matching reset).
  2. The scope of an effect handler is delimited by the handler definition. This is just like shift/reset but unlike call/cc. Delimiting the scope of a resumption has various good properties, like efficient implementation strategies, but also that it allows for modular composition (see also Oleg Kiselyov's “against call/cc”).
  3. Effect handlers can be composed freely. This is unlike general monads which need monad transformers to compose in particular ways. Essentially effect handlers can compose freely because every effect handler can be expressed eventually as an instance of a free monad which do compose. This also means that some monads cannot be expressed as an effect handler (namely the non-algebraic ones). A particular example of this is the continuation monad (which can express call/cc).

The Koka compiler internally uses monads and shift/reset to compile effect handlers though, and it compiles handlers into to an internal free monad based on multi-prompt delimited control [3, 17]. By inlining the monadic bind we are able to generate efficient C code that only allocates continuations in the case one is actually yielding up to a general ctl operation.

A great property of effect handlers is that they can be freely composed together. For example, suppose we have a function that calls raise if the state is an odd number:

fun no-odds() : <raise,state<int>> int
  val i = get()
  if i.is-odd then raise("no odds") else
    set(i / 2)
    i
fun no-oddstour/no-odds: () -> <raise,state<int>> int() : <std/core/types/(<>): Eraisetour/raise: HX,statetour/state: V -> HX<intstd/core/types/int: V>> intstd/core/types/int: V
  val ii: int = gettour/get: forall<a> () -> (state<a>) a()
  if ii: int.is-oddstd/core/is-odd: (int) -> bool then raisetour/raise: forall<a> (msg : string) -> raise a("no odds") else
    settour/set: forall<a> (x : a) -> (state<a>) ()(ii: int /std/core/(/): (x : int, y : int) -> int 2)
    ii: int

then we can compose a pstatetour/pstate: forall<a,b,e> (init : a, action : () -> <state<a>,div|e> b) -> <div|e> (b, a) and raise-maybetour/raise-maybe: forall<a,e> (action : () -> <raise|e> a) -> e maybe<a> handler together to handle the effects:

fun state-raise(init) : div (maybe<int>,int)
  with pstate(init)  
  with raise-maybe  
  no-odds()
fun state-raisetour/state-raise: (init : int) -> div (maybe<int>, int)(initinit: int) : divstd/core/types/div: X (std/core/types/(,): (V, V) -> Vmaybestd/core/types/maybe: V -> V<intstd/core/types/int: V>,intstd/core/types/int: V)std/core/types/(,): (V, V) -> V
  with pstatetour/pstate: forall<a,b,e> (init : a, action : () -> <state<a>,div|e> b) -> <div|e> (b, a)(initinit: int)  
  with raise-maybetour/raise-maybe: forall<a,e> (action : () -> <raise|e> a) -> e maybe<a>  
  no-oddstour/no-odds: () -> <raise,state<int>> int()

where both the statetour/state: V -> HX<intstd/core/types/int: V> and raisetour/raise: HX effects are discharged by the respective handlers. Note the type reflects that we always return a pair with as a first element either Nothingstd/core/types/Nothing: forall<a> maybe<a> (if raise was called) or a Juststd/core/types/Just: forall<a> (value : a) -> maybe<a> with the final result, and as the second element the final state. This corresponds to how we usually combine state and exceptions where the state (or heap) has set to the state at the point the exception happened.

However, if we combine the handlers in the opposite order, we get a form of transactional state where we either get an exception (and no final state), or we get a pair of the result with the final state:

fun raise-state(init) : div maybe<(int,int)> 
  with raise-maybe  
  with pstate(init)  
  no-odds()
fun raise-statetour/raise-state: (init : int) -> div maybe<(int, int)>(initinit: int) : divstd/core/types/div: X maybestd/core/types/maybe: V -> V<(std/core/types/(,): (V, V) -> Vintstd/core/types/int: V,intstd/core/types/int: V)std/core/types/(,): (V, V) -> V> 
  with raise-maybetour/raise-maybe: forall<a,e> (action : () -> <raise|e> a) -> e maybe<a>  
  with pstatetour/pstate: forall<a,b,e> (init : a, action : () -> <state<a>,div|e> b) -> <div|e> (b, a)(initinit: int)  
  no-oddstour/no-odds: () -> <raise,state<int>> int()

3.4.7. Masking Effects

Similar to masking signals in Unix, we can mask effects to not be handled by their innermost effect handler. The expression mask<eff>(action) modularly masks any effect operations in eff inside the action. For example, consider two nested handlers for the emit operation:

fun mask-emit() 
  with fun emit(msg){ println("outer:" ++ msg) }
  with fun emit(msg){ println("inner:" ++ msg) }
  emit("hi")
  mask<emit>{ emit("there") }
fun mask-emittour/mask-emit: () -> console ()() 
  withhandler: (() -> <emit,console> ()) -> console () fun emitemit: (msg : string) -> console ()(msgmsg: string){ printlnstd/core/println: (s : string) -> console ()("outer:" ++std/core/(++).1: (x : string, y : string) -> string msgmsg: string) }
  withhandler: (() -> <emit,console,emit> ()) -> <console,emit> () fun emitemit: (msg : string) -> <console,emit> ()(msgmsg: string){ printlnstd/core/println: (s : string) -> console ()("inner:" ++std/core/(++).1: (x : string, y : string) -> string msgmsg: string) }
  emittour/emit: (msg : string) -> emit ()("hi")
  mask<emittour/emit: HX>{ emittour/emit: (msg : string) -> emit ()("there") }

If we call mask-emittour/mask-emit: () -> console ()() it prints:

inner: hi
outer: there

The second call to emit is masked and therefore it skips the innermost handler and is handled subsequently by the outer handler (i.e. mask only masks an operation once for its innermost handler).

The type of mask<l> for some effect label l is (action: () -> e a) -> <l|e> a where it injects the effect l into the final effect result <l|e> (even thought the mask itself never actually performs any operation in l – it only masks any operations of l in action).

This type usually leads to duplicate effect labels, for example, the effect of mask<emit>{ emit("there") } is <emittour/emit: HX,emittour/emit: HX> signifying that there need to be two handlers for emittour/emit: HX: in this case, one to skip over, and one to subsequently handle the masked operation.

Effect Abstraction

The previous example is not very useful, but generally we can use mask to hide internal effect handling from higher-order functions. For example, consider the following function that needs to handle internal exceptions:

fun mask-print( action : () -> e int ) : e int
  with ctl raise(msg){ 42 }
  val x = mask<raise>(action)
  if x.is-odd then raise("wrong")   // internal exception
  x
fun mask-printtour/mask-print: forall<e> (action : () -> e int) -> e int( actionaction: () -> $6204 int : () -> ee: E intstd/core/types/int: V ) : ee: E intstd/core/types/int: V
  withhandler: (() -> <raise|$6204> int) -> $6204 int ctl raiseraise: (msg : string, resume : (_6209) -> _6208 int) -> _6208 int(msgmsg: string){ 42 }
  val xx: int = mask<raisetour/raise: HX>(actionaction: () -> $6204 int)
  if xx: int.is-oddstd/core/is-odd: (int) -> bool then raisetour/raise: forall<a> (msg : string) -> raise a("wrong")std/core/types/(): ()   // internal exception
  xx: int

Here the type of mask-printtour/mask-print: forall<e> (action : () -> e int) -> e int does not expose at all that we handle the raisetour/raise: HX effect internally for specific code and it is fully abstract – even if the action itself would call raise, it would neatly skip the internal handler due to the mask<raise> expression.

If we would leave out the mask, and call action() directly, then the inferred type of action would be () -> <raisetour/raise: HX|e> intstd/core/types/int: V instead, showing that the raisetour/raise: HX effect would be handled. Note that this is usually the desired behaviour since in the majority of cases we want to handle the effects in a particular way when defining handler abstractions. The cases where mask is needed are much less common in our experience.

advanced

State as a Combined Effect

Another nice use-case for mask occurs when modeling state directly using effect handlers without using mutable local variables [1]. We can do this using two separate operations peek and poke:

effect<a> val peek : a             // get the state
effect<a> ctl poke( x : a ) : ()   // set the state to x
effect<aa: V> val peektour/peek: forall<a> value<a> : aa: V             // get the state
effect<aa: V> ctl poketour/poke: forall<a> (x : a) -> (poke<a>) ()( xx: $6330 : aa: V ) : (std/core/types/(): V)std/core/types/(): V   // set the state to x

We can now define a generic state handler as:

fun ppstate( init : a, action : () -> <peek<a>,poke<a>|e> b ) : e b
  with val peek = init
  with ctl poke(x)
    mask<peek>
      with val peek = x
      resume(())
  action()
fun ppstatetour/ppstate: forall<a,b,e> (init : a, action : () -> <peek<a>,poke<a>|e> b) -> e b( initinit: $6358 : aa: V, actionaction: () -> <peek<$6358>,poke<$6358>|$6360> $6359 : () -> <peektour/peek: V -> HX1<aa: V>,poketour/poke: V -> HX<aa: V>|std/core/types/(<|>): (X, E) -> Eee: E> bb: V ) : ee: E bb: V
  withhandler: (() -> <peek<$6358>|$6360> $6359) -> $6360 $6359 val peekpeek: () -> $6360 $6358 = initinit: $6358
  withhandler: (() -> <poke<$6358>,peek<$6358>|$6360> $6359) -> <peek<$6358>|$6360> $6359 ctl pokepoke: (x : $6358, resume : (()) -> <peek<$6358>|$6360> $6359) -> <peek<$6358>|$6360> $6359(xx: $6358)
    mask_1: V<peektour/peek: V -> HX1>
      withhandler: (() -> <peek<$6358>|$6360> $6359) -> $6360 $6359 val peekpeek: () -> $6360 $6358 = xx: $6358
      resumeresume: (()) -> <peek<$6358>|$6360> $6359((std/core/types/(): ())std/core/types/(): ())
  actionaction: () -> <peek<$6358>,poke<$6358>|$6360> $6359()

In the handler for poke we resume under a fresh handler for peek that is bound to the new state. This means though there will be an ever increasing “stack” of handlers for peek. To keep the type from growing infinitely, we need to mask out any potential operation to a previous handler of peek which is why the mask is needed. (Another way of looking at this is to just follow the typing: action has a peektour/peek: V -> HX1 effect, and unifies with the effect of the poke operation definition. Since it handles its own peektour/peek: V -> HX1 effect, it needs to be injected back in with a mask.)

(Note: since the handler stack grows indefinitely on every poke this example is mostly of theoretical interest. However, we are looking into a stack smashing technique where we detect at runtime that a mask can discard a handler frame from the stack.)

3.4.8. Overriding Handlers

A common use for masking is to override handlers. For example, consider overriding the behavour of emit:

fun emit-quoted1( action : () -> <emit,emit|e> a ) : <emit|e> a
  with fun emit(msg){ emit("\"" ++ msg ++ "\"" ) }
  action()
fun emit-quoted1tour/emit-quoted1: forall<a,e> (action : () -> <emit,emit|e> a) -> <emit|e> a( actionaction: () -> <emit,emit|$5354> $5353 : () -> <emittour/emit: HX,emittour/emit: HX|std/core/types/(<|>): (X, E) -> Eee: E> aa: V ) : <emittour/emit: HX|std/core/types/(<|>): (X, E) -> Eee: E> aa: V
  withhandler: (() -> <emit,emit|$5354> $5353) -> <emit|$5354> $5353 fun emitemit: (msg : string) -> <emit|$5354> ()(msgmsg: string){ emittour/emit: (msg : string) -> emit ()("\"" ++std/core/(++).1: (x : string, y : string) -> string msgmsg: string ++std/core/(++).1: (x : string, y : string) -> string "\"" ) }
  actionaction: () -> <emit,emit|$5354> $5353()

Here, the handler for emit calls itself emit to actually emit the newly quoted string. The effect type inferred for emit-quoted1tour/emit-quoted1: forall<a,e> (action : () -> <emit,emit|e> a) -> <emit|e> a is (action : () -> <emittour/emit: HX,emittour/emit: HX|e> a) -> <emittour/emit: HX|e> a. This is not the nicest type as it exposes that action is evaluated under (at least) two emittour/emit: HX handlers (and someone could use mask inside action to use the outer emittour/emit: HX handler).

The override keyword keeps the type nice and fully overrides the previous handler which is no longer accessible from action:

fun emit-quoted2( action : () -> <emit|e> a ) : <emit|e> a
  with override fun emit(msg){ emit("\"" ++ msg ++ "\"" ) }
  action()
fun emit-quoted2tour/emit-quoted2: forall<a,e> (action : () -> <emit|e> a) -> <emit|e> a( actionaction: () -> <emit|$5460> $5459 : () -> <emittour/emit: HX|std/core/types/(<|>): (X, E) -> Eee: E> aa: V ) : <emittour/emit: HX|std/core/types/(<|>): (X, E) -> Eee: E> aa: V
  withhandler: (() -> <emit,emit|$5460> $5459) -> <emit|$5460> $5459 override fun emitemit: (msg : string) -> <emit|$5460> ()(msgmsg: string){ emittour/emit: (msg : string) -> emit ()("\"" ++std/core/(++).1: (x : string, y : string) -> string msgmsg: string ++std/core/(++).1: (x : string, y : string) -> string "\"" ) }
  actionaction: () -> <emit|$5460> $5459()

This of course applies to any handler or value, for example, to temporarily increase the width while pretty printing, we can override the width as:

fun extra-wide( action )
  with override val width = 2*width
  action()
fun extra-widetour/extra-wide: forall<a,e> (action : () -> <width|e> a) -> <width|e> a( actionaction: () -> <width|_5593> _5578 )
  withhandler: (() -> <width,width|_5593> _5578) -> <width|_5593> _5578 override val widthwidth: () -> <width|_5593> int = 2*std/core/(*): (int, int) -> intwidthtour/width: value<int>
  actionaction: () -> <width|_5593> _5578()

advanced

Mask Behind

Unfortunately, we cannot modularly define overriding with just mask; if we add mask outside of the emit handler, the emit call inside the operation definition would get masked and skip our intended handler. On the other hand, if we add mask just over action all its emit calls would be masked for our intended handler!

For this situation, there is another primitive that only “masks the masks”. The expression mask behind<eff> has type (() -> <eff|e> a) -> <eff,eff|e> a and only masks any masked operations but not the direct ones. The override keyword is defined in terms of this primitive:

translation

with override handler<eff> { <ops> }
<body>
with override handler<eff> { <ops> }
<body>

$\mathpre{\rightsquigarrow}$

(handler<eff> { <ops> })(mask behind<eff>{ <body> })
(handler<eff> { <ops> })(mask behind<eff>{ <body> })

This ensures any operation calls in <body> go the newly defined handler while any masked operations are masked one more level and skip both of the two innermost handlers.

3.4.9. Side-effect Isolation

3.4.10. Resuming more than once

Since resumestd/core/hnd/resume: forall<a,e,e1,b> (r : resume-context<a,e,e1,b>, x : a) -> e b is a first-class function (well, almost, see raw control), it is possible to store it in a list for example to implement a scheduler, but it is also possible to invoke it more than once. This can be used to implement backtracking or probabilistic programming models.

A common example of multiple resumptions is the choicetour/choice: HX effect:

effect ctl choice() : bool

fun xor() : choice bool
  val p = choice()
  val q = choice()
  if p then !q else q
effect ctl choicetour/choice: () -> choice bool() : boolstd/core/types/bool: V

fun xortour/xor: () -> choice bool() : choicetour/choice: HX boolstd/core/types/bool: V
  val pp: bool = choicetour/choice: () -> choice bool()
  val qq: bool = choicetour/choice: () -> choice bool()
  if pp: bool then !std/core/types/(!).1: (b : bool) -> boolqq: bool else qq: bool

One possible implementation just uses random numbers:

fun choice-random(action : () -> <choice,random|e> a) : <random|e> a
  with fun choice(){ random-bool() }
  action()
fun choice-randomtour/choice-random: forall<a,e> (action : () -> <choice,random|e> a) -> <random|e> a(actionaction: () -> <choice,random|$4078> $4077 : () -> <choicetour/choice: HX,randomstd/num/random/random: HX|std/core/types/(<|>): (X, E) -> Eee: E> aa: V) : <randomstd/num/random/random: HX|std/core/types/(<|>): (X, E) -> Eee: E> aa: V
  withhandler: (() -> <choice,random|$4078> $4077) -> <random|$4078> $4077 fun choicechoice: () -> <random|$4078> bool(){ random-boolstd/num/random/random-bool: () -> random bool() }
  actionaction: () -> <choice,random|$4078> $4077()

Where choice-randomtour/choice-random: forall<a,e> (action : () -> <choice,random|e> a) -> <random|e> a(xortour/xor: () -> choice bool) returns Truestd/core/types/True: bool and Falsestd/core/types/False: bool at random.

However, we can also resume multiple times, once with Falsestd/core/types/False: bool and once with Truestd/core/types/True: bool, to return all possible outcomes. This also changes the handler type to return a list of all results of the action, and we need a return clause to wrap the result of the action in a singleton list:

fun choice-all(action : () -> <choice|e> a) : e list<a>
  with handler
    return(x){ [x] }
    ctl choice(){ resume(False) ++ resume(True) }
  action()
fun choice-alltour/choice-all: forall<a,e> (action : () -> <choice|e> a) -> e list<a>(actionaction: () -> <choice|$4001> $4000 : () -> <choicetour/choice: HX|std/core/types/(<|>): (X, E) -> Eee: E> aa: V) : ee: E liststd/core/list: V -> V<aa: V>
  with handlerhandler: (() -> <choice|$4001> $4000) -> $4001 list<$4000>
    return(xx: $4000){ [std/core/Cons: forall<a> (head : a, tail : list<a>) -> list<a>xx: $4000]std/core/Nil: forall<a> list<a> }
    ctl choicechoice: (resume : (bool) -> $4001 list<$4000>) -> $4001 list<$4000>(){ resumeresume: (bool) -> $4001 list<$4000>(Falsestd/core/types/False: bool) ++std/core/(++): forall<a> (xs : list<a>, ys : list<a>) -> list<a> resumeresume: (bool) -> $4001 list<$4000>(Truestd/core/types/True: bool) }
  actionaction: () -> <choice|$4001> $4000()

where choice-alltour/choice-all: forall<a,e> (action : () -> <choice|e> a) -> e list<a>(xortour/xor: () -> choice bool) returns [Falsestd/core/types/False: bool,Truestd/core/types/True: bool,Truestd/core/types/True: bool,Falsestd/core/types/False: bool].

Resuming more than once interacts in interesting ways with the state effect. Consider the following example that uses both choicetour/choice: HX and statetour/state: V -> HX:

fun surprising() : <choice,state<int>> bool 
  val p = choice()
  val i = get()
  set(i+1)
  if i>0 && p then xor() else False
fun surprisingtour/surprising: () -> <choice,state<int>> bool() : <std/core/types/(<>): Echoicetour/choice: HX,statetour/state: V -> HX<intstd/core/types/int: V>> boolstd/core/types/bool: V 
  val pp: bool = choicetour/choice: () -> choice bool()
  val ii: int = gettour/get: forall<a> () -> (state<a>) a()
  settour/set: forall<a> (x : a) -> (state<a>) ()(ii: int+std/core/(+): (int, int) -> int1)
  if ii: int>std/core/(>).1: (x : int, y : int) -> bool0 &&std/core/types/(&&): (x : bool, y : bool) -> bool pp: bool then xortour/xor: () -> choice bool() else Falsestd/core/types/False: bool

We can combine the handlers in two interesting ways:

fun state-choice() : div (list<bool>,int) 
  pstate(0){ choice-all(surprising) }

fun choice-state() : div list<(bool,int)>
  choice-all{ pstate(0,surprising) }
fun state-choicetour/state-choice: () -> div (list<bool>, int)() : divstd/core/types/div: X (std/core/types/(,): (V, V) -> Vliststd/core/list: V -> V<boolstd/core/types/bool: V>,intstd/core/types/int: V)std/core/types/(,): (V, V) -> V 
  pstatetour/pstate: forall<a,b,e> (init : a, action : () -> <state<a>,div|e> b) -> <div|e> (b, a)(0){ choice-alltour/choice-all: forall<a,e> (action : () -> <choice|e> a) -> e list<a>(surprisingtour/surprising: () -> <choice,state<int>> bool) }

fun choice-statetour/choice-state: () -> div list<(bool, int)>() : divstd/core/types/div: X liststd/core/list: V -> V<(std/core/types/(,): (V, V) -> Vboolstd/core/types/bool: V,intstd/core/types/int: V)std/core/types/(,): (V, V) -> V>
  choice-alltour/choice-all: forall<a,e> (action : () -> <choice|e> a) -> e list<a>{ pstatetour/pstate: forall<a,b,e> (init : a, action : () -> <state<a>,div|e> b) -> <div|e> (b, a)(0,surprisingtour/surprising: () -> <choice,state<int>> bool) }

In state-choicetour/state-choice: () -> div (list<bool>, int)() the pstatetour/pstate: forall<a,b,e> (init : a, action : () -> <state<a>,div|e> b) -> <div|e> (b, a) is the outer handler and becomes like a global state over all resumption strands in choice-alltour/choice-all: forall<a,e> (action : () -> <choice|e> a) -> e list<a>, and thus after the first resume the i>0 (&&)std/core/types/(&&): (x : bool, y : bool) -> bool p condition in surprisingtour/surprising: () -> <choice,state<int>> bool is Truestd/core/types/True: bool, and we get ([Falsestd/core/types/False: bool,Falsestd/core/types/False: bool,Truestd/core/types/True: bool,Truestd/core/types/True: bool,Falsestd/core/types/False: bool],2).

In choice-statetour/choice-state: () -> div list<(bool, int)>() the pstatetour/pstate: forall<a,b,e> (init : a, action : () -> <state<a>,div|e> b) -> <div|e> (b, a) is the inner handler and becomes like transactional state, where the state becomes local to each resumption strand in choice-alltour/choice-all: forall<a,e> (action : () -> <choice|e> a) -> e list<a>. Now i is always 0 at first and thus we get [(Falsestd/core/types/False: bool,1),(Falsestd/core/types/False: bool,1)].

advancedThis example also shows how var state is correctly saved and restored on resumptions (as part of the stack) and this is essential to the correct composition of effect handlers. If var declarations were instead heap allocated or captured by reference, they would no longer be local to their scope and side effects could “leak” across different resumptions.

3.4.11. Initially and Finally

With arbitrary effect handlers we need to be careful when interacting with external resources like files. Generally, operations can never resume (like exceptions), resume exactly once (giving the usual linear control flow), or resume more than once. To robustly handle these different cases, Koka provides the finallystd/core/hnd/finally: forall<a,e> (fin : () -> e (), action : () -> e a) -> e a and initiallystd/core/hnd/initially: forall<a,e> (init : (int) -> e (), action : () -> e a) -> e a functions. Suppose we have the following low-level file operations on file handles:

type fhandle
fun fopen( path : string )   : <exn,filesys> fhandle
fun hreadline( h : fhandle ) : <exn,filesys> string
fun hclose( h : fhandle )    : <exn,filesys> ()
type fhandle
fun fopen( path : stringstd/core/types/string: V )   : <exnstd/core/exn: HX,filesys> fhandle
fun hreadline( h : fhandle ) : <exnstd/core/exn: HX,filesys> stringstd/core/types/string: V
fun hclose( h : fhandle )    : <exnstd/core/exn: HX,filesys> ()

Using these primitives, we can declare a fread effect to read from a file:

effect fun fread() : string

fun with-file( path : string, action : () -> <fread,exn,filesys|e> a ) : <exn,filesys|e> a
  val h = fopen(path)
  with handler
    return(x)  { hclose(h); x }
    fun fread(){ hreadline(h) }  
  action()
effect fun fread() : stringstd/core/types/string: V

fun with-file( path : stringstd/core/types/string: V, action : () -> <fread,exnstd/core/exn: HX,filesys|e> a ) : <exnstd/core/exn: HX,filesys|e> a
  val h = fopen(path)
  with handler
    return(x)  { hclose(h); x }
    fun fread(){ hreadline(h) }  
  action()

However, as it stands it would fail to close the file handle if an exceptional effect inside action is used (i.e. or any operation that never resumes). The finallystd/core/hnd/finally: forall<a,e> (fin : () -> e (), action : () -> e a) -> e a function handles these situations, and takes as its first argument a function that is always executed when either returning normally, or when unwinding for a non-resuming operation. So, a more robust way to write with-file is:

fun with-file( path : string, action : () -> <fread,exn,filesys|e> a ) : <exn,filesys|e> a
  val h = fopen(path)
  with finally{ hclose(h) }
  with fun fread(){ hreadline(h) }
  action()
fun with-file( path : stringstd/core/types/string: V, action : () -> <fread,exnstd/core/exn: HX,filesys|e> a ) : <exnstd/core/exn: HX,filesys|e> a
  val h = fopen(path)
  with finallystd/core/hnd/finally: forall<a,e> (fin : () -> e (), action : () -> e a) -> e a{ hclose(h) }
  with fun fread(){ hreadline(h) }
  action()

The current definition is robust for operations that never resume, or operations that resume once – but there is still trouble when resuming more than once. If someone calls choice inside the action, the second time it resumes the file handle will be closed again which is probably not intended. There is active research into using the type system to statically prevent this from happening.

Another way to work with multiple resumptions is to use the initiallystd/core/hnd/initially: forall<a,e> (init : (int) -> e (), action : () -> e a) -> e a function. This function takes 2 arguments: the first argument is a function that is called the first time initiallystd/core/hnd/initially: forall<a,e> (init : (int) -> e (), action : () -> e a) -> e a is evaluated, and subsequently every time a particular resumption is resumed more than once. We can use this to implement various strategies to handle linear resources even for multiple resumptions. For files, it is not clear what is the best way to handle this, but one way would be to not close the file until all strands have finished:

fun with-file( path : string, action : () -> <fread,exn,filesys|e> a ) : <exn,filesys|e> a
  var count := 0
  val h = fopen(path)
  with initially fn(rcount){ count := count+1 }
  with finally{ if count==1 then hclose(h) else count := count - 1 }
  with fun fread(){ hreadline(h) }
  action()
fun with-file( path : stringstd/core/types/string: V, action : () -> <fread,exnstd/core/exn: HX,filesys|e> a ) : <exnstd/core/exn: HX,filesys|e> a
  var count := 0
  val h = fopen(path)
  with initiallystd/core/hnd/initially: forall<a,e> (init : (int) -> e (), action : () -> e a) -> e a fn(rcount){ count := count+1 }
  with finallystd/core/hnd/finally: forall<a,e> (fin : () -> e (), action : () -> e a) -> e a{ if count==1 then hclose(h) else count := count - 1 }
  with fun fread(){ hreadline(h) }
  action()

advancedThe rcount parameter is the resume count; it is 0 on the first evaluation of initiallystd/core/hnd/initially: forall<a,e> (init : (int) -> e (), action : () -> e a) -> e a, and >1 for every resume (for any operation) after the first one.

Raw Control

Todo. Use rctl for raw control operations which do not automatically finalize; this gives true first-class resumption contexts (as rcontext) but need to be used with care. With rctl one can use the implicitly bound resumption context rcontext to either resume (as rcontext.resumestd/core/hnd/resume: forall<a,e,e1,b> (r : resume-context<a,e,e1,b>, x : a) -> e b(x)), or to finalize a resumption (as rcontext.finalizestd/core/hnd/finalize: forall<a,e,e1,b> (r