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:
For Linux and macOS on x86 64-bit, you can install Koka using:
> curl -sSL https://github.com/koka-lang/koka/releases/latest/download/install.sh | sh
This also installs syntax highlighting for the VS Code and Atom editors. After installation, verify if Koka installed correctly:
> koka
_ _ ____
| | | | |__ \
| | __ ___ | | __ __ _ __) |
| |/ // _ \| |/ // _' || ___/ welcome to the koka interpreter
| <| (_) | <| (_| ||____| version 2.0.10, Nov 28 2020, libc 64-bit (gcc)
|_|\_\\___/|_|\_\\__,_| type :? for help
loading: std/core
loading: std/core/types
loading: std/core/hnd
>
Type :q
to exit the interpreter.
For detailed instructions and other platforms (including Windows) see the releases page. It is also straightforward to build the compiler from source.
You can compile a Koka source using -c
(note that all samples
are pre-installed):
> koka -c samples/basic/caesar.kk
compile: samples/basic/caesar.kk
loading: std/core
loading: std/core/types
loading: std/core/hnd
loading: std/num/double
loading: std/text/parse
loading: std/num/int32
check : samples/basic/caesar
linking: samples_basic_caesar
created: out/v2.0.9/gcc-debug/samples_basic_caesar
and run the resulting executable:
> out/v2.0.9/gcc-debug/samples_basic_caesar
plain : Koka is a well-typed language
encoded: Krnd lv d zhoo-wbshg odqjxdjh
cracked: Koka is a well-typed language
The -O2
flag builds an optimized program. Let's try it on a purely functional implementation
of balanced insertion in a red-black tree (rbtree.kk
):
> koka -O2 -c samples/basic/rbtree.kk
...
linking: samples_basic_rbtree
created: out/v2.0.10/gcc-drelease/samples_basic_rbtree
> time out/v2.0.10/gcc-drelease/samples_basic_rbtree
420000
real 0m0.750s
...
We can compare this against an in-place updating C++ implementation using stl::map
(rbtree.cpp
) (which also uses a
red-black tree internally):
> clang++ --std=c++17 -o cpp-rbtree -O3 /usr/local/share/koka/v2.0.12/samples/basic/rbtree.cpp
> time ./cpp-rbtree
420000
real 0m0.864s
...
The excellent performance relative to C++ here (on an AMD 3600XT) is the result of Perceus automatically transforming the fast path of the pure functional rebalancing to use mostly in-place updates, closely mimicking the imperative rebalancing code of the hand optimized C++ library.
Without giving any input files, the interactive environment runs by default:
> koka
_ _ ____
| | | | |__ \
| | __ ___ | | __ __ _ __) |
| |/ // _ \| |/ // _' || ___/ welcome to the koka interpreter
| <| (_) | <| (_| ||____| version 2.0.9, Nov 27 2020, libc 64-bit (gcc)
|_|\_\\___/|_|\_\\__,_| type :? for help
loading: std/core
loading: std/core/types
loading: std/core/hnd
>
Now you can test some expressions:
> println("hi koka")
check : interactive
check : interactive
linking: interactive
created: out\v2.0.9\mingw-debug\interactive
hi koka
> :t "hi"
string
> :t println("hi")
console ()
Or load a demo (use tab
completion to avoid typing too much):
> :l samples/basic/fibonacci
compile: samples/basic/fibonacci.kk
loading: std/core
loading: std/core/types
loading: std/core/hnd
check : samples/basic/fibonacci
modules:
samples/basic/fibonacci
> main()
check : interactive
check : interactive
linking: interactive
created: out\v2.0.9\mingw-debug\interactive
The 10000th fibonacci number is 33644764876431783266621612005107543310302148460680063906564769974680081442166662368155595513633734025582065332680836159373734790483865268263040892463056431887354544369559827491606602099884183933864652731300088830269235673613135117579297437854413752130520504347701602264758318906527890855154366159582987279682987510631200575428783453215515103870818298969791613127856265033195487140214287532698187962046936097879900350962302291026368131493195275630227837628441540360584402572114334961180023091208287046088923962328835461505776583271252546093591128203925285393434620904245248929403901706233888991085841065183173360437470737908552631764325733993712871937587746897479926305837065742830161637408969178426378624212835258112820516370298089332099905707920064367426202389783111470054074998459250360633560933883831923386783056136435351892133279732908133732642652633989763922723407882928177953580570993691049175470808931841056146322338217465637321248226383092103297701648054726243842374862411453093812206564914032751086643394517512161526545361333111314042436854805106765843493523836959653428071768775328348234345557366719731392746273629108210679280784718035329131176778924659089938635459327894523777674406192240337638674004021330343297496902028328145933418826817683893072003634795623117103101291953169794607632737589253530772552375943788434504067715555779056450443016640119462580972216729758615026968443146952034614932291105970676243268515992834709891284706740862008587135016260312071903172086094081298321581077282076353186624611278245537208532365305775956430072517744315051539600905168603220349163222640885248852433158051534849622434848299380905070483482449327453732624567755879089187190803662058009594743150052402532709746995318770724376825907419939632265984147498193609285223945039707165443156421328157688908058783183404917434556270520223564846495196112460268313970975069382648706613264507665074611512677522748621598642530711298441182622661057163515069260029861704945425047491378115154139941550671256271197133252763631939606902895650288268608362241082050562430701794976171121233066073310059947366875
And quit the interpreter:
> :q
I think of my body as a side effect of my mind.
-- Carrie Fisher (1956)
The samples/syntax
and samples/basic
directories contain various basic Koka examples to start with. If you type:
> :l samples/
in the interpreter, you can tab
twice to see the available sample files and directories.
Use :s
to see the source of a loaded module.
If you use VS Code or Atom, or if you set the koka_editor
environment variable,
you can type :e
in the interactive prompt to edit your program further. For example,
> :l samples/basic/caesar
...
check : samples/basic/caesar
modules:
samples/basic/caesar
> :e
<edit the source and reload>
> :r
...
check : samples/basic/caesar
modules:
samples/basic/caesar
> main()
What next?
Basic Koka syntax Browse the Library documentation
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:
Koka has a small core set of orthogonal, well-studied language features – but each of these is as general and composable as possible, such that we do not need further “special” extensions. Core features include first-class functions, a higher-rank impredicative polymorphic type- and effect system, algebraic data types, and effect handlers.
fun hello-ten() { var i := 0 while { i < 10 } { println("hello") i := i + 1 } } fun hello-ten() { var i := 0 while { i < 10 } { println("hello") i := i + 1 } }
As an example of the min-gen design principle, Koka implements most
control-flow primitives as regular functions. An anonymous function can
be written as fn(){ <body> }
; but as a syntactic convenience, any
function without arguments can be shortened further to use just braces,
as { <body> }
.
We can write a whilestd/core/while: forall<e> (predicate : () -> <div|e> bool, action : () -> <div|e> ()) -> <div|e> ()
loop now using regular
function calls as shown in the example,
where the call to whilestd/core/while: forall<e> (predicate : () -> <div|e> bool, action : () -> <div|e> ()) -> <div|e> ()
is desugared to
whilestd/core/while: forall<e> (predicate : () -> <div|e> bool, action : () -> <div|e> ()) -> <div|e> ()( fn(){ i < 10 }, fn(){ ... } )
.
This also naturally leads to
consistency: an expression between parenthesis is always evaluated
before a function call, whereas an expression between braces (ah,
suspenders!) is suspended and may be never evaluated or more than once
(as in our example). This is inconsistent in most other languages where
often the predicate of a whilestd/core/while: forall<e> (predicate : () -> <div|e> bool, action : () -> <div|e> ()) -> <div|e> ()
loop is written in parenthesis but may
be evaluated multiple times.
Koka infers and tracks the effect of every function in its type – and a function type has 3 parts: the argument types, the effect type, and the type of the result. For example:
fun sqr : (int) -> total int // mathematical total function fun divide : (int,int) -> exn int // may raise an exception (partial) fun turing : (tape) -> div int // may not terminate (diverge) fun print : (string) -> console () // may write to the console fun rand : () -> ndet int // non-deterministic fun sqr : (intstd/core/types/int: V) -> totalstd/core/total: E intstd/core/types/int: V // mathematical total function fun divide : (intstd/core/types/int: V,intstd/core/types/int: V) -> exnstd/core/exn: HX intstd/core/types/int: V // may raise an exception (partial) fun turing : (tape) -> divstd/core/types/div: X intstd/core/types/int: V // may not terminate (diverge) fun print : (stringstd/core/types/string: V) -> consolestd/core/console: X () // may write to the console fun rand : () -> ndetstd/core/types/ndet: X intstd/core/types/int: V // non-deterministic
The precise effect typing gives Koka rock-solid semantics and deep safety guarantees backed by well-studied category theory, which makes Koka particularly easy to reason about for both humans and compilers. (Given the importance of effect typing, the name Koka was derived from the Japanese word for effective (効果, こうか, Kōka)).
A function without any effect is called totalstd/core/total: E
and corresponds to
mathematically total functions – a good place to be. Then we have
effects for partial functions that can raise exceptions (exnstd/core/exn: HX
), and
potentially non-terminating functions as divstd/core/types/div: X
(divergent). The
combination of exnstd/core/exn: HX
and divstd/core/types/div: X
is called purestd/core/pure: E
as that corresponds to
Haskell's notion of purity. On top of that we find mutability (as ststd/core/types/st: H -> E
)
up to full non-deterministic side effects in iostd/core/io: E
.
Effects can be polymorphic as well. Consider mapping a function over a list:
fun map( xs : list<a>, f : a -> e b ) : e list<b> { match(xs) { Cons(x,xx) -> Cons( f(x), map(xx,f) ) Nil -> Nil } } fun map( xs : liststd/core/list: V -> V<a>, f : a -> e b ) : e liststd/core/list: V -> V<b> { match(xs) { Consstd/core/Cons: forall<a> (head : a, tail : list<a>) -> list<a>(x,xx) -> Consstd/core/Cons: forall<a> (head : a, tail : list<a>) -> list<a>( f(x), map(xx,f) ) Nilstd/core/Nil: forall<a> list<a> -> Nilstd/core/Nil: forall<a> list<a> } }
Single letter types are polymorphic (aka, generic), and Koka infers
that you map from a list of elements a
to a list of elements of
type b
. Since map
itself has no intrinsic effect, the effect
of applying map
is exactly the effect of the function f
that
is applied, namely e
.
Another example of the min-gen design principle: instead of various special language and compiler extensions to support exceptions, generators, async/await etc., Koka has full support for algebraic effect handlers – these lets you define advanced control abstractions like async/await as a user library in a typed and composable way.
Here is an example of an effect definition with
one operation to yield intstd/core/types/int: V
values:
effect yield { control yield( i : int ) : bool } effect yieldwhy/yield: HX { control yieldwhy/yield: (i : int) -> yield bool( ii: int : intstd/core/types/int: V ) : boolstd/core/types/bool: V }
Once the effect is declared, we can use it for example to yield the elements of a list:
fun traverse( xs : list<int> ) : yield () { match(xs) { Cons(x,xx) -> if (yield(x)) then traverse(xx) else () Nil -> () } } fun traversewhy/traverse: (xs : list<int>) -> yield ()( xsxs: list<int> : liststd/core/list: V -> V<intstd/core/types/int: V> ) : yieldwhy/yield: HX (std/core/types/(): V)std/core/types/(): V { match(xsxs: list<int>) { Consstd/core/Cons: forall<a> (head : a, tail : list<a>) -> list<a>(xx: int,xxxx: list<int>) -> if (std/core/types/True: boolyieldwhy/yield: (i : int) -> yield bool(xx: int)) then traversewhy/traverse: (xs : list<int>) -> yield ()(xxxx: list<int>) else (std/core/types/(): ())std/core/types/(): () Nilstd/core/Nil: forall<a> list<a> -> (std/core/types/(): ())std/core/types/(): () } }
The traversewhy/traverse: (xs : list<int>) -> yield ()
function calls yield
and therefore gets the yieldwhy/yield: HX
effect in its type,
and if we want to use traversewhy/traverse: (xs : list<int>) -> yield ()
, we need to handle the yieldwhy/yield: HX
effect.
This is much like defining an exception handler, except we can receive values (here an intstd/core/types/int: V
),
and we can resume with a result (which determines if we keep traversing):
fun print-elems() : console () { with control yield(i){ println("yielded " ++ i.show) resume(i<=2) } traverse([1,2,3,4]) } fun print-elemswhy/print-elems: () -> console ()() : consolestd/core/console: X (std/core/types/(): V)std/core/types/(): V { withhandler: (() -> <yield,console> ()) -> console () control yieldyield: (i : int, resume : (bool) -> console ()) -> console ()(ii: int){ printlnstd/core/println: (s : string) -> console ()("yielded " ++std/core/(++).1: (x : string, y : string) -> string ii: int.showstd/core/show: (i : int) -> string) resumeresume: (bool) -> console ()(ii: int<=std/core/(<=).1: (int, int) -> bool2) } traversewhy/traverse: (xs : list<int>) -> yield ()([std/core/Cons: forall<a> (head : a, tail : list<a>) -> list<a>1,2,3,4]std/core/Nil: forall<a> list<a>) }
The with
statement binds the handler for yieldwhy/yield: HX
over the
rest of the scope, in this case traversewhy/traverse: (xs : list<int>) -> yield ()([1,2,3,4])
.
Note how the handler discharges the yieldwhy/yield: HX
effect – and replaces
it with a consolestd/core/console: X
effect. When we run the example, we get:
yielded: 1
yielded: 2
yielded: 3
Perceus is the compiler optimized reference counting technique that Koka uses for automatic memory management [15]. This (together with evidence translation [16]) enables Koka to compile directly to plain C code without needing a garbage collector or runtime system.
Perceus uses extensive static analysis to aggressively optimize the reference counts. Here the strong semantic foundation of Koka helps a lot: inductive data types cannot form cycles, and potential sharing across threads can be reliably determined.
Normally we need to make a fundamental choice when managing memory:
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.
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.
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.
As usual, we start with the familiar Hello world program:
fun main() { println("Hello world!") // println output } fun maintour/main: () -> console ()() { printlnstd/core/println: (s : string) -> console ()("Hello world!") // println output }
Koka uses familiar curly-braces syntax where starts a line
comment. Functions are declared using the
fun
keyword (and anonymous functions with fn
).
Here is another short example program that encodes a string using the Caesar cipher, where each lower-case letter in a string is replaced by the letter three places up in the alphabet:
fun main() { println(caesar("koka is fun")) } fun encode( s : string, shift : int ) { fun encode-char(c) { if (c < 'a' || c > 'z') return c val base = (c - 'a').int val rot = (base + shift) % 26 (rot.char + 'a') } s.map(encode-char) } fun caesar( s : string ) : string { s.encode( 3 ) } fun encodetour/encode: (s : string, shift : int) -> string( ss: string : stringstd/core/types/string: V, shiftshift: int : intstd/core/types/int: V ) { fun encode-charencode-char: (c : char) -> char(cc: char) { if (std/core/types/True: boolcc: char <std/core/(<): (char, char) -> bool 'a' ||std/core/types/(||): (x : bool, y : bool) -> bool cc: char >std/core/(>): (char, char) -> bool 'z') returnreturn: char cc: char val basebase: int = (cc: char -std/core/(-).4: (c : char, d : char) -> total char 'a').intstd/core/int: (char) -> int val rotrot: int = (basebase: int +std/core/(+): (int, int) -> int shiftshift: int) %std/core/(%): (int, int) -> int 26 (rotrot: int.charstd/core/char: (int) -> char +std/core/(+).4: (c : char, d : char) -> total char 'a') } ss: string.mapstd/core/map.6: forall<e> (s : string, f : (char) -> e char) -> e string(encode-charencode-char: (c : char) -> char) } fun caesartour/caesar: (s : string) -> string( ss: string : stringstd/core/types/string: V ) : stringstd/core/types/string: V { ss: string.encodetour/encode: (s : string, shift : int) -> string( 3 ) }
In this example, we declare a local function encode-char
which encodes a
single character c
. The final statement s.map(encode-char)
applies the
encode-char
function to each character in the string s
, returning a
new string where each character is Caesar encoded. The result of the final
statement in a function is also the return value of that function, and you can
generally leave out an explicit return
keyword.
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.
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.
Koka also allows for anonymous function expressions using the fn
keyword.
For example, instead of
declaring the encode-char
function, we can also pass it directly to
the map
function as a function expression:
fun encode2( s : string, shift : int ) { s.map( fn(c) { if (c < 'a' || c > 'z') return c val base = (c - 'a').int val rot = (base + shift) % 26 (rot.char + 'a') }); } fun encode2tour/encode2: (s : string, shift : int) -> string( ss: string : stringstd/core/types/string: V, shiftshift: int : intstd/core/types/int: V ) { ss: string.mapstd/core/map.6: forall<e> (s : string, f : (char) -> e char) -> e string( fn(cc: char) { if (std/core/types/True: boolcc: char <std/core/(<): (char, char) -> bool 'a' ||std/core/types/(||): (x : bool, y : bool) -> bool cc: char >std/core/(>): (char, char) -> bool 'z') returnreturn: char cc: char val basebase: int = (cc: char -std/core/(-).4: (c : char, d : char) -> total char 'a').intstd/core/int: (char) -> int val rotrot: int = (basebase: int +std/core/(+): (int, int) -> int shiftshift: int) %std/core/(%): (int, int) -> int 26 (rotrot: int.charstd/core/char: (int) -> char +std/core/(+).4: (c : char, d : char) -> total char 'a') }); }
It is a bit annoying we had to put the final right-parenthesis after the last
brace in the previous example. As a convenience, Koka allows anonymous functions to follow
the function call instead – this is also known as trailing lambdas.
For example, here is how we can print the numbers
1
to 10
:
fun main() { print10() } fun print10() { for(1,10) fn(i) { println(i) } } fun print10tour/print10: () -> console ()() { forstd/core/for: forall<e> (start : int, end : int, action : (int) -> e ()) -> e ()(1,10) fn(ii: int) { printlnstd/core/println.1: (i : int) -> console ()(ii: int) } }
which is desugared to forstd/core/for: forall<e> (start : int, end : int, action : (int) -> e ()) -> e ()( 1, 10, fn(i){ println(i) } )
. (In fact, since we
pass the i
argument directly to println
, we could have also passed the function itself
directly, and write forstd/core/for: forall<e> (start : int, end : int, action : (int) -> e ()) -> e ()(1,10,println)
.)
Anonymous functions without any arguments can be shortened further by leaving
out the fn
keyword as well and just use braces directly. Here is an example using
the repeat
function:
fun main() { printhi10() } fun printhi10() { repeat(10) { println("hi") } } fun printhi10tour/printhi10: () -> console ()() { repeatstd/core/repeat.1: forall<e> (n : int, action : () -> e ()) -> e ()(10) { printlnstd/core/println: (s : string) -> console ()("hi") } }
where the body desugars to repeat( 10, fn(){println(
hi
)} )
. The is
especially convenient for the whilestd/core/while: forall<e> (predicate : () -> <div|e> bool, action : () -> <div|e> ()) -> <div|e> ()
loop since this is not a built-in
control flow construct but just a regular function:
fun main() { print11() } fun print11() { var i := 10 while { i >= 0 } { println(i) i := i - 1 } } fun print11tour/print11: () -> <console,div> ()() { varstd/core/hnd/local-var: forall<a,b,e,h> (init : a, action : (l : local-var<h,a>) -> <local<h>|e> b) -> <local<h>|e> b istd/core/types/local-scope: forall<e,a> (action : forall<h> () -> <local<h>|e> a) -> e a := 10 whilestd/core/while: forall<e> (predicate : () -> <div|e> bool, action : () -> <div|e> ()) -> <div|e> () { ii: int >=std/core/(>=).1: (int, int) -> bool 0 } { printlnstd/core/println.1: (i : int) -> console ()(ii: int) ii: local-var<$3011,int> :=std/core/types/local-set: forall<a,e,h> (v : local-var<h,a>, assigned : a) -> <local<h>|e> () ii: int -std/core/(-): (int, int) -> int 1 } }
Note how the first argument to whilestd/core/while: forall<e> (predicate : () -> <div|e> bool, action : () -> <div|e> ()) -> <div|e> ()
is in braces instead of the usual
parenthesis. In Koka, an expression between parenthesis is always evaluated
before a function call, whereas an expression between braces (ah,
suspenders!) is suspended and may be never evaluated or more than once
(as in our example).
To the best of our knowledge, Koka was the first language to have
generalized dot notation and trailing lambdas. Another novel
syntactical feature is the with
statement.
With the ease of passing a function block as a parameter, these
often become nested. For example:
fun twice(f) { f() f() } fun test-twice() { twice( fn(){ twice( fn(){ println("hi") }) }) } fun twicetour/twice: forall<a,e> (f : () -> e a) -> e a(ff: () -> _3532 _3533) { ff: () -> _3532 _3533() ff: () -> _3532 _3533() } fun test-twicetour/test-twice: () -> console ()() { twicetour/twice: forall<a,e> (f : () -> e a) -> e a( fn(){ twicetour/twice: forall<a,e> (f : () -> e a) -> e a( fn(){ printlnstd/core/println: (s : string) -> console ()("hi") }) }) }
where "hi"
is printed four times. Using the with
statement
we can write this more concisely as:
public fun test-with1() { with twice with twice println("hi") } public fun test-with1tour/test-with1: () -> console ()() { with twicetour/twice: forall<a,e> (f : () -> e a) -> e a with twicetour/twice: forall<a,e> (f : () -> e a) -> e a printlnstd/core/println: (s : string) -> console ()("hi") }
The with
statement essentially puts all statements that follow it into
an anynomous function block and passes that as the last parameter. In general:
translation
with f(e1,...,eN) <body> with f(e1,...,eN) <body>
f(e1,...,eN, fn(){ <body> }) f(e1,...,eN, fn(){ <body> })
Moreover, a with
statement can also bind a variable parameter as:
translation
with x = f(e1,...,eN) <body> with x = f(e1,...,eN) <body>
f(e1,...,eN, fn(x){ <body> }) f(e1,...,eN, fn(x){ <body> })
Here is an examply using foreach
to span over the rest of the function body:
public fun test-with2() { with x = list(1,10).foreach println(x) } public fun test-with2tour/test-with2: () -> console ()() { with xx: int = liststd/core/list: (lo : int, hi : int) -> total list<int>(1,10).foreachstd/core/foreach: forall<a,e> (xs : list<a>, action : (a) -> e ()) -> e () printlnstd/core/println.1: (i : int) -> console ()(xx: int) }
which desugars to list(1,10).foreach( fn(x){ println(x) } )
.
This is a bit reminiscent of Haskell do
notation.
Using the with
statement this way may look a bit strange at first
but is very convenient in practice – it helps thinking of with
as
a closure over the rest of the lexical scope.
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
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 except op(x){ <body> } with control op(x){ <body> } with val op = <expr> with fun op(x){ <body> } with except op(x){ <body> } with control op(x){ <body> }
with handler{ val op = <expr> } with handler{ fun op(x){ <body> } } with handler{ except op(x){ <body> } } with handler{ control op(x){ <body> } } with handler{ val op = <expr> } with handler{ fun op(x){ <body> } } with handler{ except op(x){ <body> } } with handler{ control op(x){ <body> } }
Using this, we can write the previous example in a more concise and natural way as:
public fun emit-console2() { with fun emit(msg){ println(msg) } hello() } public fun emit-console2tour/emit-console2: () -> console ()() { withhandler: (() -> <emit,console> ()) -> console () fun emitemit: (msg : string) -> console ()(msgmsg: string){ printlnstd/core/println: (s : string) -> console ()(msgmsg: string) } hellotour/hello: () -> emit ()() }
Intuitively, we can view the handler with fun emit
as a dynamic binding of the function emit
over the rest of the scope.
Being a function-oriented language, Koka has powerful support for function
calls where it supports both optional and named parameters. For example, the
function replace-allstd/core/replace-all: (s : string, pattern : string, repl : string) -> string
takes a string, a pattern (named pattern
), and
a replacement string (named repl
):
fun main() { println(world()) } fun world() { replace-all("hi there", "there", "world") // returns "hi world" } fun worldtour/world: () -> string() { replace-allstd/core/replace-all: (s : string, pattern : string, repl : string) -> string("hi there", "there", "world") // returns "hi world" }
Using named parameters, we can also write the function call as:
fun main() { println(world2()) } fun world2() { "hi there".replace-all( repl="world", pattern="there" ) } fun world2tour/world2: () -> string() { "hi there".replace-allstd/core/replace-all: (s : string, pattern : string, repl : string) -> string( repl="world", pattern="there" ) }
Optional parameters let you specify default values for parameters that do not
need to be provided at a call-site. As an example, let's define a function
sublisttour/sublist: forall<a> (xs : list<a>, start : int, len : ?int) -> list<a>
that takes a list, a start
position, and the length len
of the desired
sublist. We can make the len
parameter optional and by default return all
elements following the start
position by picking the length of the input list by
default:
fun main() { println( ['a','b','c'].sublist(1).string ) } fun sublist( xs : list<a>, start : int, len : int = xs.length ) : list<a> { if (start <= 0) return xs.take(len) match(xs) { Nil -> Nil Cons(_,xx) -> xx.sublist(start - 1, len) } } fun sublisttour/sublist: forall<a> (xs : list<a>, start : int, len : ?int) -> list<a>( xsxs: list<$8136> : liststd/core/list: V -> V<aa: V>, startstart: int : intstd/core/types/int: V, lenlen: ?int : intstd/core/types/optional: V -> V = xsxs: list<$8136>.lengthstd/core/length.1: forall<a> (xs : list<a>) -> int ) : liststd/core/list: V -> V<aa: V> { if (std/core/types/True: boolstartstart: int <=std/core/(<=).1: (int, int) -> bool 0) returnreturn: list<$8136> xsxs: list<$8136>.takestd/core/take: forall<a> (xs : list<a>, n : int) -> list<a>(lenlen: int)std/core/types/(): () match(xsxs: list<$8136>) { Nilstd/core/Nil: forall<a> list<a> -> Nilstd/core/Nil: forall<a> list<a> Consstd/core/Cons: forall<a> (head : a, tail : list<a>) -> list<a>(_,xxxx: list<$8136>) -> xxxx: list<$8136>.sublisttour/sublist: forall<a> (xs : list<a>, start : int, len : ?int) -> list<a>(startstart: int -std/core/(-): (int, int) -> int 1, lenlen: int) } }
Hover over the sublisttour/sublist: forall<a> (xs : list<a>, start : int, len : ?int) -> list<a>
identifier to see its full type, where the len
parameter has gotten an optional intstd/core/types/int: V
type signified by the question mark:
:?int
.
fun main() { test-uncaesar() } fun encode( s : string, shift : int ) { function encode-char(c) { if (c < 'a' || c > 'z') return c val base = (c - 'a').int val rot = (base + shift) % 26 (rot.char + 'a') } s.map(encode-char) } // The letter frequency table for English val english = [8.2,1.5,2.8,4.3,12.7,2.2, 2.0,6.1,7.0,0.2,0.8,4.0,2.4, 6.7,7.5,1.9,0.1, 6.0,6.3,9.1, 2.8,1.0,2.4,0.2,2.0,0.1] // Small helper functions fun percent( n : int, m : int ) { 100.0 * (n.double / m.double) } fun rotate( xs, n ) { xs.drop(n) ++ xs.take(n) } // Calculate a frequency table for a string fun freqs( s : string ) : list<double> { val lowers = list('a','z') val occurs = lowers.map( fn(c){ s.count(c.string) }) val total = occurs.sum occurs.map( fn(i){ percent(i,total) } ) } // Calculate how well two frequency tables match according // to the _chi-square_ statistic. fun chisqr( xs : list<double>, ys : list<double> ) : double { zipwith(xs,ys, fn(x,y){ ((x - y)^2.0)/y } ).foldr(0.0,(+)) } // Crack a Caesar encoded string fun uncaesar( s : string ) : string { val table = freqs(s) // build a frequency table for `s` val chitab = list(0,25).map( fn(n) { // build a list of chisqr numbers for each shift between 0 and 25 chisqr( table.rotate(n), english ) }) val min = chitab.minimum() // find the mininal element val shift = chitab.index-of( fn(f){ f == min } ).negate // and use its position as our shift s.encode( shift ) } fun test-uncaesar() { println( uncaesar( "nrnd lv d ixq odqjxdjh" ) ) } // The letter frequency table for English val englishtour/english: list<double> = [std/core/Cons: forall<a> (head : a, tail : list<a>) -> list<a>8.2,1.5,2.8,4.3,12.7,2.2, 2.0,6.1,7.0,0.2,0.8,4.0,2.4, 6.7,7.5,1.9,0.1, 6.0,6.3,9.1, 2.8,1.0,2.4,0.2,2.0,0.1]std/core/Nil: forall<a> list<a> // Small helper functions fun percenttour/percent: (n : int, m : int) -> double( nn: int : intstd/core/types/int: V, mm: int : intstd/core/types/int: V ) { 100.0 *std/core/(*).1: (double, double) -> double (nn: int.doublestd/core/double: (int) -> double /std/core/(/).1: (double, double) -> double mm: int.doublestd/core/double: (int) -> double) } fun rotatetour/rotate: forall<a> (xs : list<a>, n : int) -> list<a>( xsxs: list<_3219>, nn: int ) { xsxs: list<_3219>.dropstd/core/drop: forall<a> (xs : list<a>, n : int) -> list<a>(nn: int) ++std/core/(++): forall<a> (xs : list<a>, ys : list<a>) -> list<a> xsxs: list<_3219>.takestd/core/take: forall<a> (xs : list<a>, n : int) -> list<a>(nn: int) } // Calculate a frequency table for a string fun freqstour/freqs: (s : string) -> list<double>( ss: string : stringstd/core/types/string: V ) : liststd/core/list: V -> V<doublestd/core/types/double: V> { val lowerslowers: list<char> = liststd/core/list.2: (lo : char, hi : char) -> total list<char>('a','z') val occursoccurs: list<int> = lowerslowers: list<char>.mapstd/core/map.5: forall<a,b,e> (xs : list<a>, f : (a) -> e b) -> e list<b>( fn(cc: char){ ss: string.countstd/core/count: (s : string, pattern : string) -> int(cc: char.stringstd/core/string: (c : char) -> string) }) val totaltotal: int = occursoccurs: list<int>.sumstd/core/sum: (xs : list<int>) -> int occursoccurs: list<int>.mapstd/core/map.5: forall<a,b,e> (xs : list<a>, f : (a) -> e b) -> e list<b>( fn(ii: int){ percenttour/percent: (n : int, m : int) -> double(ii: int,totaltotal: int) } ) } // Calculate how well two frequency tables match according // to the _chi-square_ statistic. fun chisqrtour/chisqr: (xs : list<double>, ys : list<double>) -> double( xsxs: list<double> : liststd/core/list: V -> V<doublestd/core/types/double: V>, ysys: list<double> : liststd/core/list: V -> V<doublestd/core/types/double: V> ) : doublestd/core/types/double: V { zipwithstd/core/zipwith: forall<a,b,c,e> (xs : list<a>, ys : list<b>, f : (a, b) -> e c) -> e list<c>(xsxs: list<double>,ysys: list<double>, fn(xx: double,yy: double){ ((xx: double -std/core/(-).3: (double, double) -> double yy: double)^std/core/(^): (d : double, p : double) -> double2.0)/std/core/(/).1: (double, double) -> doubleyy: double } ).foldrstd/core/foldr: forall<a,b,e> (xs : list<a>, z : b, f : (a, b) -> e b) -> e b(0.0,(+)std/core/(+).3: (double, double) -> double) } // Crack a Caesar encoded string fun uncaesartour/uncaesar: (s : string) -> string( ss: string : stringstd/core/types/string: V ) : stringstd/core/types/string: V { val tabletable: list<double> = freqstour/freqs: (s : string) -> list<double>(ss: string) // build a frequency table for `s` val chitabchitab: list<double> = liststd/core/list: (lo : int, hi : int) -> total list<int>(0,25).mapstd/core/map.5: forall<a,b,e> (xs : list<a>, f : (a) -> e b) -> e list<b>( fn(nn: int) { // build a list of chisqr numbers for each shift between 0 and 25 chisqrtour/chisqr: (xs : list<double>, ys : list<double>) -> double( tabletable: list<double>.rotatetour/rotate: forall<a> (xs : list<a>, n : int) -> list<a>(nn: int), englishtour/english: list<double> ) }) val minmin: double = chitabchitab: list<double>.minimumstd/core/minimum.1: (xs : list<double>) -> double() // find the mininal element val shiftshift: int = chitabchitab: list<double>.index-ofstd/core/index-of: forall<a> (xs : list<a>, pred : (a) -> bool) -> int( fn(ff: double){ ff: double ==std/core/(==).2: (double, double) -> bool minmin: double } ).negatestd/core/negate: (i : int) -> int // and use its position as our shift ss: string.encodetour/encode: (s : string, shift : int) -> string( shiftshift: int ) } fun test-uncaesartour/test-uncaesar: () -> console ()() { printlnstd/core/println: (s : string) -> console ()( uncaesartour/uncaesar: (s : string) -> string( "nrnd lv d ixq odqjxdjh" ) ) }
The val
keyword declares a static value. In the example, the value englishtour/english: list<double>
is a list of floating point numbers (of type doublestd/core/types/double: V
) denoting the average
frequency for each letter. The function freqstour/freqs: (s : string) -> list<double>
builds a frequency table for a
specific string, while the function chisqrtour/chisqr: (xs : list<double>, ys : list<double>) -> double
calculates how well two frequency
tables match. In the function crack
these functions are used to find a
shift
value that results in a string whose frequency table matches the
englishtour/english: list<double>
one the closest – and we use that to decode the string.
You can try out this example directly in the interactive environment:
> :l samples/basic/caesar.kk
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
The inferred effects are not just considered as some extra type information on
functions. On the contrary, through the inference of effects, Koka has a very
strong connection to its denotational semantics. In particular, the full type
of a Koka functions corresponds directly to the type signature of the
mathematical function that describes its denotational semantics. For example,
using 〚t
〛 to translate a type t
into its corresponding
mathematical type signature, we have:
In the above translation, we use as a sum
where we have either a unit (i.e. exception) or a type , and we use
for a product consisting of a pair of a
heap and a type . From the above correspondence, we can immediately see that
a totalstd/core/total: E
function is truly total in the mathematical sense, while a stateful
function (ststd/core/types/st: H -> E<h>
) that can raise exceptions or not terminate (purestd/core/pure: E
)
takes an implicit heap parameter, and either does not terminate () or
returns an updated heap together with either a value or an exception ().
We believe that this semantic correspondence is the true power of full effect types and it enables effective equational reasoning about the code by a programmer. For almost all other existing programming languages, even the most basic semantics immediately include complex effects like heap manipulation and divergence. In contrast, Koka allows a layered semantics where we can easily separate out nicely behaved parts, which is essential for many domains, like safe LINQ queries, parallel tasks, tier-splitting, sand-boxed mobile code, etc.
Often, a function contains multiple effects, for example:
fun combine-effects() { val i = srandom-int() // non-deterministic throw("oops") // exception raising combine-effects() // and non-terminating } fun combine-effectstour/combine-effects: forall<a> () -> <pure,ndet> a() { val ii: int = srandom-intstd/num/random/srandom-int: () -> ndet int() // non-deterministic throwstd/core/throw: forall<a> (message : string, info : ?exception-info) -> exn a("oops") // exception raising combine-effectstour/combine-effects: () -> <exn,ndet,div> _5155() // and non-terminating }
The effect assigned to combine-effectstour/combine-effects: forall<a> () -> <pure,ndet> a
are ndetstd/core/types/ndet: X
, divstd/core/types/div: X
, and exnstd/core/exn: HX
. We
can write such combination as a row of effects as <divstd/core/types/div: X,exnstd/core/exn: HX,ndetstd/core/types/ndet: X>
. When
you hover over the combine-effectstour/combine-effects: forall<a> () -> <pure,ndet> a
identifiers, you will see that the type
inferred is really <purestd/core/pure: E,ndetstd/core/types/ndet: X>
where purestd/core/pure: E
is a type alias defined as
alias pure = <div,exn> alias purestd/core/pure: E = <divstd/core/types/div: X,exnstd/core/exn: HX>
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
.
The Fibonacci numbers are a sequence where each subsequent Fibonacci number is
the sum of the previous two, where fibtour/fib: (n : int) -> div int(0) == 0
and fibtour/fib: (n : int) -> div int(1) == 1
. We can
easily calculate Fibonacci numbers using a recursive function:
fun main() { println(fib(10)) } fun fib(n : int) : div int { if (n <= 0) then 0 elif (n == 1) then 1 else fib(n - 1) + fib(n - 2) } fun fibtour/fib: (n : int) -> div int(nn: int : intstd/core/types/int: V) : divstd/core/types/div: X intstd/core/types/int: V { if (std/core/types/True: boolnn: int <=std/core/(<=).1: (int, int) -> bool 0) then 0 elif (std/core/types/True: boolnn: int ==std/core/(==).1: (int, int) -> bool 1) then 1 else fibtour/fib: (n : int) -> div int(nn: int -std/core/(-): (int, int) -> int 1) +std/core/(+): (int, int) -> int fibtour/fib: (n : int) -> div int(nn: int -std/core/(-): (int, int) -> int 2) }
Note that the type inference engine is currently not powerful enough to
prove that this recursive function always terminates, which leads to
inclusion of the divergence effect divstd/core/types/div: X
in the result type.
Here is another version of the Fibonacci function but this time
implemented using local mutable variables.
We use the repeat
function to iterate n
times:
fun main() { println(fib2(10)) } fun fib2(n) { var x := 0 var y := 1 repeat(n) { val y0 = y y := x+y x := y0 } x } fun fib2tour/fib2: (n : int) -> int(nn: int) { varstd/core/hnd/local-var: forall<a,b,e,h> (init : a, action : (l : local-var<h,a>) -> <local<h>|e> b) -> <local<h>|e> b xstd/core/types/local-scope: forall<e,a> (action : forall<h> () -> <local<h>|e> a) -> e a := 0 varstd/core/hnd/local-var: forall<a,b,e,h> (init : a, action : (l : local-var<h,a>) -> <local<h>|e> b) -> <local<h>|e> b yy: local-var<$2244,int> := 1 repeatstd/core/repeat.1: forall<e> (n : int, action : () -> e ()) -> e ()(nn: int) { val y0y0: int = yy: int yy: local-var<$2244,int> :=std/core/types/local-set: forall<a,e,h> (v : local-var<h,a>, assigned : a) -> <local<h>|e> () xx: int+std/core/(+): (int, int) -> intyy: int xx: local-var<$2244,int> :=std/core/types/local-set: forall<a,e,h> (v : local-var<h,a>, assigned : a) -> <local<h>|e> () y0y0: int } xx: int }
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.
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<h,a> (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 } return !x } fun fib3tour/fib3: (n : int) -> int(nn: int) { val xx: ref<_2414,int> = refstd/core/types/ref: forall<h,a> (value : a) -> (alloc<h>) ref<h,a>(0) val yy: ref<_2414,int> = refstd/core/types/ref: forall<h,a> (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/(!).1: forall<h,a,e> (ref : ref<h,a>) -> <read<h>|e> a with hdiv<h,a,e>yy: ref<_2414,int> yy: ref<_2414,int> :=std/core/types/set: forall<h,a> (ref : ref<h,a>, assigned : a) -> (write<h>) () !std/core/types/(!).1: forall<h,a,e> (ref : ref<h,a>) -> <read<h>|e> a with hdiv<h,a,e>xx: ref<_2414,int> +std/core/(+): (int, int) -> int !std/core/types/(!).1: forall<h,a,e> (ref : ref<h,a>) -> <read<h>|e> a with hdiv<h,a,e>yy: ref<_2414,int> xx: ref<_2414,int> :=std/core/types/set: forall<h,a> (ref : ref<h,a>, assigned : a) -> (write<h>) () y0y0: int } returnreturn: int !std/core/types/(!).1: forall<h,a,e> (ref : ref<h,a>) -> <read<h>|e> a with hdiv<h,a,e>xx: ref<_2414,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
.
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)
).
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.
Koka also supports algebraic data types where there are multiple alternatives. For example, here is an enumeration:
type colors { Red Green Blue } type colors { redtour/red: (argb : argb) -> int greentour/green: (argb : argb) -> int bluetour/blue: (argb : argb) -> int }
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> }
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 } }
Todo
Todo
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.
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; red: int; green: int; blue: int } value struct argbtour/argb: V{ alphaalpha: int: intstd/core/types/int: V; redred: int: intstd/core/types/int: V; greengreen: int: intstd/core/types/int: V; blueblue: int: intstd/core/types/int: V }
advanced
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 negative doubles for boxing while positive doubles are boxed in-place.
(this can be configured though to only heap allocate doubles for boxing when their absolute value is
outside of the range 2-511 up to 2512).
For performance sensitive code we may specialize certain polymorphic datatypes to reduce allocations due to boxing. For example:
type mylist{ con MyCons{ head1: int; head2: bool; mytail: mylist } con MyNil } type mylisttour/mylist: V{ con MyConsmylist: mylist{ head1head1: int: intstd/core/types/int: V; head2head2: bool: boolstd/core/types/bool: V; mytailmytail: mylist: mylisttour/mylist: V } con MyNilmylist: 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.
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.
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
operation:
effect raise { control raise( msg : string ) : a } effect raisetour/raise: HX { control 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 (std/core/types/True: boolyy: int==std/core/(==).1: (int, 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 { control raise(msg){ 42 } } 8 + safe-divide(1,0) } fun raise-consttour/raise-const: () -> int() : intstd/core/types/int: V { with handlerhandler: (() -> raise int) -> int { control raiseraise: (msg : string, resume : (_7686) -> _7685 int) -> _7685 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 control op(<args>){ <body> } with control op(<args>){ <body> }
with handler { control op(<args>){ <body> } } with handler { control op(<args>){ <body> } }
With this translation, we can write the previous example more concisely as:
fun raise-const1() : int { with control raise(msg){ 42 } 8 + safe-divide(1,0) } fun raise-const1tour/raise-const1: () -> int() : intstd/core/types/int: V { withhandler: (() -> raise int) -> int control raiseraise: (msg : string, resume : (_7752) -> _7751 int) -> _7751 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{ control 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 control op(<parameters>) : <result-type> effect control op(<parameters>) : <result-type>
effect op { control op(<parameters>) : <result-type> } effect op { control op(<parameters>) : <result-type> }
That means we can declare our raisetour/raise: HX
effect signature also more concisely as:
effect control raise( msg : string ) : a effect control raise( msg : stringstd/core/types/string: V ) : a
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> control ask() : a control ask() : a } fun add-twice() : ask<int> int { ask() + ask() } effect asktour/ask: V -> HX<aa: V> { // or: effect<a> control ask() : a control 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 control ask(){ resume(21) } add-twice() } fun ask-consttour/ask-const: () -> int() : intstd/core/types/int: V { withhandler: (() -> (ask<int>) int) -> int control 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 control 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 control 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,b> (r : resume-context<a,e,b>, x : a) -> e b
function is implicitly bound by a control
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,b> (r : resume-context<a,e,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 control 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<e,a> (action : forall<h> () -> <local<h>|e> a) -> e a := 0 withhandler: (() -> <ask<int>,local<$3923>> int) -> (local<$3923>) int control askask: (resume : (int) -> (local<$3923>) int) -> (local<$3923>) int() { countcount: local-var<$3923,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 (std/core/types/True: boolcountcount: int <=std/core/(<=).1: (int, int) -> bool 1) then resumeresume: (int) -> (local<$3923>) 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.
A control
operation is one of the most general ways to define operations since
we get a first-class resumestd/core/hnd/resume: forall<a,e,b> (r : resume-context<a,e,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> }
with control op(<args>){ val f = fn(){ <body> }; resume( f() ) } with control op(<args>){ val f = fn(){ <body> }; resumestd/core/hnd/resume: forall<a,e,b> (r : resume-context<a,e,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
control
operations. The Koka compiler uses (generalized) evidence translation [16]
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 adjucted evidence
vector for its context). Unlike a general control
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 very 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.
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>
val x = <expr> with fun v(){ x } val x = <expr> with fun v(){ x }
val x = <expr> with control v(){ resume(x) } val x = <expr> with control v(){ resumestd/core/hnd/resume: forall<a,e,b> (r : resume-context<a,e,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").
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 define 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|_5792> _5743 ) { withhandler: (() -> <emit,console|_5792> _5743) -> <console|_5792> _5743 fun emitemit: (msg : string) -> <console|_5792> ()(msgmsg: string){ printlnstd/core/println: (s : string) -> console ()(msgmsg: string) } actionaction: () -> <console,emit|_5792> _5743() }
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|_6043> ()(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|$5386> () : () -> <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<e,a> (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<$5390>|$5386> ()) -> <local<$5390>|$5386> string { return(xx: _5399){ 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<$5390>|$5386> ()(msgmsg: string){ lineslines: local-var<$5390,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|$5386> ()() } 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.
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 control raise(msg){ hnd(msg) } action() } fun catchtour/catch: forall<a,e> (hnd : (string) -> e a, action : () -> <raise|e> a) -> e a( hndhnd: (string) -> $4299 $4298 : (stringstd/core/types/string: V) -> ee: E aa: V, actionaction: () -> <raise|$4299> $4298 : () -> <raisetour/raise: HX|std/core/types/(<|>): (X, E) -> Eee: E> aa: V ) : ee: E aa: V { withhandler: (() -> <raise|$4299> $4298) -> $4299 $4298 control raiseraise: (msg : string, resume : (_4304) -> $4299 $4298) -> $4299 $4298(msgmsg: string){ hndhnd: (string) -> $4299 $4298(msgmsg: string) } actionaction: () -> <raise|$4299> $4298() }
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).
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 control 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|$5235> $5234 : () -> <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|$5235> $5234) -> $5235 maybe<$5234> { return(xx: _5238){ Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>(xx: _5238) } // normal return: wrap in Just control raiseraise: (msg : string, resume : (_5247) -> _5246 maybe<_5238>) -> _5246 maybe<_5238>(msgmsg: string){ Nothingstd/core/types/Nothing: forall<a> maybe<a> } // exception: return Nothing directly } actionaction: () -> <raise|$5235> $5234() } 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 )
).
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: $4748 : 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 (std/core/types/True: boolii: int <=std/core/(<=).1: (int, 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: $7923 : aa: V, actionaction: () -> <state<$7923>,div|$7925> $7924 : () -> <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<e,a> (action : forall<h> () -> <local<h>|e> a) -> e a := initinit: $7923 with handlerhandler: (() -> <state<$7923>,local<$7929>,div|$7925> $7924) -> <local<$7929>,div|$7925> $7924 { fun getget: () -> <local<$7929>,div|$7925> $7923(){ stst: $7923 } fun setset: (i : $7923) -> <local<$7929>,div|$7925> ()(ii: $7923){ stst: local-var<$7929,$7923> :=std/core/types/local-set: forall<a,e,h> (v : local-var<h,a>, assigned : a) -> <local<h>|e> () ii: $7923 } } actionaction: () -> <state<$7923>,div|$7925> $7924() }
where state(10){ sumdowntour/sumdown: (sum : ?int) -> <div,state<int>> int() }
evaluates to 55
.
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: $4776 : aa: V, actionaction: () -> <state<$4776>,div|$4778> $4777 : () -> <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<e,a> (action : forall<h> () -> <local<h>|e> a) -> e a := initinit: $4776 with handlerhandler: (() -> <state<$4776>,local<$4782>,div|$4778> $4777) -> <local<$4782>,div|$4778> ($4777, $4776) { return(xx: _4791){ (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)xx: _4791,stst: $4776)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b) } // pair with the final state fun getget: () -> <local<$4782>,div|$4778> $4776(){ stst: $4776 } fun setset: (i : $4776) -> <local<$4782>,div|$4778> ()(ii: $4776){ stst: local-var<$4782,$4776> :=std/core/types/local-set: forall<a,e,h> (v : local-var<h,a>, assigned : a) -> <local<h>|e> () ii: $4776 } } actionaction: () -> <state<$4776>,div|$4778> $4777() }
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: $7476 : aa: V, actionaction: () -> <state<$7476>,div|$7478> $7477 : () -> <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<e,a> (action : forall<h> () -> <local<h>|e> a) -> e a := initinit: $7476 with return(xx: $7477){ (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)xx: $7477,stst: $7476)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b) } with handlerhandler: (() -> <state<$7476>,local<$7482>,div|$7478> $7477) -> <local<$7482>,div|$7478> $7477 { fun getget: () -> <local<$7482>,div|$7478> $7476(){ stst: $7476 } fun setset: (i : $7476) -> <local<$7482>,div|$7478> ()(ii: $7476){ stst: local-var<$7482,$7476> :=std/core/types/local-set: forall<a,e,h> (v : local-var<h,a>, assigned : a) -> <local<h>|e> () ii: $7476 } } actionaction: () -> <state<$7476>,div|$7478> $7477() }
Here it as a bit contrived but it can make certain programs more concise in their definition, see for example [4].
advancedWhat makes effect handlers a good control-flow abstraction? There are three fundamental advantages with regard to other approaches:
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
).
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”).
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].
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 control
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 (std/core/types/True: boolii: 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() }
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.
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 control 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: () -> $7090 int : () -> ee: E intstd/core/types/int: V ) : ee: E intstd/core/types/int: V { withhandler: (() -> <raise|$7090> int) -> $7090 int control raiseraise: (msg : string, resume : (_7095) -> _7094 int) -> _7094 int(msgmsg: string){ 42 } val xx: int = mask<raisetour/raise: HX>(actionaction: () -> $7090 int) if (std/core/types/True: boolxx: 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 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
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> control 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> control poketour/poke: forall<a> (x : a) -> (poke<a>) ()( xx: $7226 : 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 control 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: $7254 : aa: V, actionaction: () -> <peek<$7254>,poke<$7254>|$7256> $7255 : () -> <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<$7254>|$7256> $7255) -> $7256 $7255 val peekpeek: () -> $7256 $7254 = initinit: $7254 withhandler: (() -> <poke<$7254>,peek<$7254>|$7256> $7255) -> <peek<$7254>|$7256> $7255 control pokepoke: (x : $7254, resume : (()) -> <peek<$7254>|$7256> $7255) -> <peek<$7254>|$7256> $7255( xx: $7254 ) { mask_1: V<peektour/peek: V -> HX1> { withhandler: (() -> <peek<$7254>|$7256> $7255) -> $7256 $7255 val peekpeek: () -> $7256 $7254 = xx: $7254 resumeresume: (()) -> <peek<$7254>|$7256> $7255((std/core/types/(): ())std/core/types/(): ()) } } actionaction: () -> <peek<$7254>,poke<$7254>|$7256> $7255() }
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.)
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|$6073> $6072 : () -> <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|$6073> $6072) -> <emit|$6073> $6072 fun emitemit: (msg : string) -> <emit|$6073> ()(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|$6073> $6072() }
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|$6197> $6196 : () -> <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|$6197> $6196) -> <emit|$6197> $6196 override fun emitemit: (msg : string) -> <emit|$6197> ()(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|$6197> $6196() }
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|_6352> _6333 ) { withhandler: (() -> <width,width|_6352> _6333) -> <width|_6352> _6333 override val widthwidth: () -> <width|_6352> int = 2*std/core/(*): (int, int) -> intwidthtour/width: value<int> actionaction: () -> <width|_6352> _6333() }
advanced
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<l>
has type (() -> <l|e> a) -> <l,l|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<l> { <ops> } <body> with override handler<l> { <ops> } <body>
(handler<l> { <ops> })(mask behind<l>{ <body> }) (handler<l> { <ops> })(mask behind<l>{ <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.
Since resumestd/core/hnd/resume: forall<a,e,b> (r : resume-context<a,e,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 control choice() : bool fun xor() : choice bool { val p = choice() val q = choice() if (p) then !q else q } effect control 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 (std/core/types/True: boolpp: bool) then !std/core/types/(!): (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|$4667> $4666 : () -> <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|$4667> $4666) -> <random|$4667> $4666 fun choicechoice: () -> <random|$4667> bool(){ random-boolstd/num/random/random-bool: () -> random bool() } actionaction: () -> <choice,random|$4667> $4666() }
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] } control choice(){ resume(False) ++ resume(True) } } action() } fun choice-alltour/choice-all: forall<a,e> (action : () -> <choice|e> a) -> e list<a>(actionaction: () -> <choice|$4586> $4585 : () -> <choicetour/choice: HX|std/core/types/(<|>): (X, E) -> Eee: E> aa: V) : ee: E liststd/core/list: V -> V<aa: V> { with handlerhandler: (() -> <choice|$4586> $4585) -> $4586 list<$4585> { return(xx: $4585){ [std/core/Cons: forall<a> (head : a, tail : list<a>) -> list<a>xx: $4585]std/core/Nil: forall<a> list<a> } control choicechoice: (resume : (bool) -> $4586 list<$4585>) -> $4586 list<$4585>(){ resumeresume: (bool) -> $4586 list<$4585>(Falsestd/core/types/False: bool) ++std/core/(++): forall<a> (xs : list<a>, ys : list<a>) -> list<a> resumeresume: (bool) -> $4586 list<$4585>(Truestd/core/types/True: bool) } } actionaction: () -> <choice|$4586> $4585() }
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 (std/core/types/True: boolii: int>std/core/(>).1: (int, 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.
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.
Todo.
Use rcontrol
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 rcontrol
one can use the implicitly bound
resumption context rcontext
to either resume (as rcontext.resumestd/core/hnd/resume: forall<a,e,b> (r : resume-context<a,e,b>, x : a) -> e b(x)
),
or to finalize a resumption (as rcontext.finalizestd/core/hnd/finalize: forall<a,b,e,c> (r : resume-context<b,e,c>, x : a) -> e a
) which runs all
finallystd/core/hnd/finally: forall<a,e> (fin : () -> e (), action : () -> e a) -> e a
handlers to clean up resources.
Todo.
Use linear effect
to declare effects whose operations are always tail-resumptive
and use only linear effects themselves
(and thus resume exactly once). This removes monadic translation for such effects and
can make code that uses only linear effects more compact and efficient.
Todo.
See samples/named-handlers
.
With Perceus reuse analysis we can
write algorithms that dynamically adapt to use in-place mutation when
possible (and use copying when used persistently). Importantly,
you can rely on this optimization happening, e.g. see
the match
patterns and pair them to same-sized constructors in each branch.
This style of programming leads to a new paradigm that we call FBIP: “functional but in place”. Just like tail-call optimization lets us describe loops in terms of regular function calls, reuse analysis lets us describe in-place mutating imperative algorithms in a purely functional way (and get persistence as well).
Note. FBIP is still active research. In particular we'd like to add ways to add annotations to ensure reuse is taking place.
As an example, we consider
insertion into a red-black tree [2].
A polymorphic version of this example is part of the samples
directory when you have
installed Koka and can be loaded as :l
samples/basic/rbtree
.
We define red-black trees as:
type color { Red Black } type tree { Leaf Node(color: color, left: tree, key: int, value: bool, right: tree) } type color { redtour/red: (argb : argb) -> int Black } type treetour/tree: V { Leaf Node(color: color, left: treetour/tree: V, key: intstd/core/types/int: V, value: boolstd/core/types/bool: V, right: treetour/tree: V) }
The red-black tree has the invariant that the number of black nodes from the root to any of the leaves is the same, and that a red node is never a parent of red node. Together this ensures that the trees are always balanced. When inserting nodes, the invariants need to be maintained by rebalancing the nodes when needed. Okasaki's algorithm [12] implements this elegantly and functionally:
fun balance-left( l : tree, k : int, v : bool, r : tree ): tree { match(l) { Node(_, Node(Red, lx, kx, vx, rx), ky, vy, ry) -> Node(Red, Node(Black, lx, kx, vx, rx), ky, vy, Node(Black, ry, k, v, r)) ... } fun ins( t : tree, k : int, v : bool ): tree { match(t) { Leaf -> Node(Red, Leaf, k, v, Leaf) Node(Red, l, kx, vx, r) -> if (k < kx) then Node(Red, ins(l, k, v), kx, vx, r) ... Node(Black, l, kx, vx, r) -> if (k < kx && is-red(l)) then balance-left(ins(l,k,v), kx, vx, r) ... } fun balance-left( l : treetour/tree: V, k : intstd/core/types/int: V, v : boolstd/core/types/bool: V, r : treetour/tree: V ): treetour/tree: V { match(l) { Node(_, Node(redtour/red: (argb : argb) -> int, lx, kx, vx, rx), ky, vy, ry) -> Node(redtour/red: (argb : argb) -> int, Node(Black, lx, kx, vx, rx), ky, vy, Node(Black, ry, k, v, r)) ... } fun ins( t : treetour/tree: V, k : intstd/core/types/int: V, v : boolstd/core/types/bool: V ): treetour/tree: V { match(t) { Leaf -> Node(redtour/red: (argb : argb) -> int, Leaf, k, v, Leaf) Node(redtour/red: (argb : argb) -> int, l, kx, vx, r) -> if (k < kx) then Node(redtour/red: (argb : argb)