This is a short introduction to the Koka programming language meant for programmers familiar with languages like C++, C#, or JavaScript.

Koka is a *function-oriented* language that separates pure values from side-effecting computations (The word 'koka' (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 JavaScript like syntax.

For more background information, see the Koka research page and the slides of a talk presented Lang.Next (April 2012)

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

load in editorfunction mainguide/main: () -> console ()() { printlnstd/core/println: (s : string) -> console ()("Hello world!") // println output }

Functions are declared using the function or fun keyword. It is customary to use function for top-level functions, and fun for anonymous function expressions.

Now click on the load in editor button in the upper right corner of the hello world example to load it into the editor on the right-hand side and run the program to see its output.

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:

load in editorfunction encodeguide/encode: (s : string, shift : int) -> string( ss: string : stringstd/core/string: V, shiftshift: int : intstd/core/int: V ) { fun encodeCharencodeChar: (c : char) -> char(cc: char) { if (cc: char <std/core/(<): (char, char) -> bool 'a' ||std/core/(||): (bool, bool) -> bool cc: char >std/core/(>): (char, char) -> bool 'z') returnreturn: char cc: char basebase: int = (cc: char -std/core/(-).2: (c : char, d : char) -> total char 'a').intstd/core/int: (char) -> int rotrot: int = (basebase: int +std/core/(+): (int, int) -> int shiftshift: int) %std/core/(%).1: (x : int, y : int) -> int 26 returnreturn: char (rotrot: int.charstd/core/char: (int) -> char +std/core/(+).3: (c : char, d : char) -> total char 'a') } ss: string.mapstd/core/map.3: forall<e> (s : string, f : (char) -> e char) -> e string(encodeCharencodeChar: (c : char) -> char) } function caesarguide/caesar: (s : string) -> string( ss: string : stringstd/core/string: V ) : stringstd/core/string: V { ss: string.encodeguide/encode: (s : string, shift : int) -> string( 3 ) }

In this example, we declare a local function encodeChar which encodes a single character c. The final statement s.map(encodeChar) applies the encodeChar function to each character in the 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.

As we can see in the example, we can leave out semi-colons at the end of each statement or declaration. Koka uses a simple layout rule where semi-colons are automatically inserted for any statements and declarations that are aligned between braces ({ and }). Long statements can be continued on the next line simply by using more indentation. Of course, if required, you can always use explicit semi-colons as well, for example to put multiple statements on a single line.

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.encode(3) does *not* select the encodeguide/encode: (s : string, shift : int) -> string method from the stringstd/core/string: V object, but it is simply syntactic sugar for the function call encode(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:

load in editorfun showitguide/showit: (s : string) -> console ()( ss: string : stringstd/core/string: V ) = ss: string.encodeguide/encode: (s : string, shift : int) -> string(3).lengthstd/core/length.3: (s : string) -> int.printlnstd/core/println.1: (i : int) -> console ()

for example (where the body desugars as println(length(encode(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. You can hover with your mouse over base and rot in the example to see the types that were inferred by Koka. Generally, we do 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 encodeguide/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/string: V types, 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. For example, instead of declaring the encodeChar function, we could just have passed it directly to the map function as a function expression:

load in editorfunction encode2guide/encode2: (s : string, shift : int) -> string( ss: string : stringstd/core/string: V, shiftshift: int : intstd/core/int: V ) { ss: string.mapstd/core/map.3: forall<e> (s : string, f : (char) -> e char) -> e string( fun(cc: char) { if (cc: char <std/core/(<): (char, char) -> bool 'a' ||std/core/(||): (bool, bool) -> bool cc: char >std/core/(>): (char, char) -> bool 'z') returnreturn: char cc: char basebase: int = (cc: char -std/core/(-).2: (c : char, d : char) -> total char 'a').intstd/core/int: (char) -> int rotrot: int = (basebase: int +std/core/(+): (int, int) -> int shiftshift: int) %std/core/(%).1: (x : int, y : int) -> int 26 returnreturn: char (rotrot: int.charstd/core/char: (int) -> char +std/core/(+).3: (c : char, d : char) -> total char 'a') }); }

It is a bit annoying we had to put the final right-parenthesis after the last brace. As a convenience, Koka allows anonymous functions to *follow* the function call instead. For example, here is how we can print the numbers 1 to 10:

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

which is desugared to for( 1, 10, fun(i){ println(i) } ). In fact, since we pass the i argument directly to println, we can also the function itself directly, and write for(1,10,println).

Anonymous functions without any arguments can be shortened further by leaving out the fun keyword and just using braces directly. Here is an example using the repeatstd/core/repeat: forall<e> (n : int, action : () -> e ()) -> e () function:

load in editorfunction printhi10guide/printhi10: () -> console ()() { repeatstd/core/repeat: forall<e> (n : int, action : () -> e ()) -> e ()(10) { printlnstd/core/println: (s : string) -> console ()("hi") } }

where the body desugars to repeat( 10, fun(){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 operator in Koka but just a regular function:

load in editorfunction print11guide/print11: () -> <div,console> ()() { var ii: ref<_h,int> := 10 whilestd/core/while: forall<e> (predicate : () -> <div|e> bool, action : () -> <div|e> ()) -> <div|e> () { ii: ref<_h,int> >=std/core/(>=).1: (int, int) -> bool 0 } { printlnstd/core/println.1: (i : int) -> console ()(ii: ref<_h,int>) ii: ref<_h,int> :=std/core/set: forall<h,a> (ref : ref<h,a>, assigned : a) -> (write<h>) () ii: ref<_h,int>-std/core/(-): (int, int) -> int1 } }

In particular, Koka makes it always explicit when code is evaluated before a function is called (in between parenthesis), or evaluated (potentially multiple times) by the called function (in between braces).

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: X, and if a function may not terminate the effect is divstd/core/div: X (for divergence). The combination of exnstd/core/exn: X and divstd/core/div: X is purestd/core/pure: E and corresponds directly to Haskell's notion of purity. Non-deterministic functions get the ndetstd/core/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:

load in editorfunction square1guide/square1: (x : int) -> total int( xx: int : intstd/core/int: V ) : totalstd/core/total: E intstd/core/int: V { returnreturn: int xx: int*std/core/(*): (int, int) -> intxx: int } function square2guide/square2: (x : int) -> io int( xx: int : intstd/core/int: V ) : iostd/core/io: E intstd/core/int: V { printlnstd/core/println: (s : string) -> console ()( "a not so secret side-effect" ) returnreturn: int xx: int*std/core/(*): (int, int) -> intxx: int } function square3guide/square3: (x : int) -> div int( xx: int : intstd/core/int: V ) : divstd/core/div: X intstd/core/int: V { square3guide/square3: (x : int) -> div int( xx: int ) returnreturn: int xx: int*std/core/(*): (int, int) -> intxx: int } function square4guide/square4: (x : int) -> exn int( xx: int : intstd/core/int: V ) : exnstd/core/exn: X intstd/core/int: V { errorstd/core/error: forall<a> (string) -> exn a( "oops" ) returnreturn: int 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:

load in editorfunction square5guide/square5: (x : int) -> int( xx: int : intstd/core/int: V ) : intstd/core/int: V = xx: int*std/core/(*): (int, int) -> intxx: int

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

load in editorfunction square6guide/square6: (x : int) -> console int( xx: int : intstd/core/int: V ) : _e_e: E intstd/core/int: V { printlnstd/core/println: (s : string) -> console ()("I did not want to write down the io effect") returnreturn: int xx: int*std/core/(*): (int, int) -> intxx: int }

Hover over square6guide/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:

〚intstd/core/int: V -> totalstd/core/total: E intstd/core/int: V〛 | = | ℤ_{32} → ℤ_{32} |

〚intstd/core/int: V -> exnstd/core/exn: X intstd/core/int: V〛 | = | ℤ_{32} → (1 + ℤ_{32}) |

〚intstd/core/int: V -> purestd/core/pure: E intstd/core/int: V〛 | = | ℤ_{32} → (1 + ℤ_{32})_{⊥} |

〚intstd/core/int: V -> <ststd/core/st: H -> E<h>,purestd/core/pure: E> intstd/core/int: V〛 | = | (Heap × ℤ_{32}) → (Heap × (1 + ℤ_{32}))_{⊥} |

In the above translation, we use 1 + t as a sum where we have either a unit 1 (i.e. exception) or a type t, and we use Heap × t for a product consisting of a pair of a heap and a type t. 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/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 (1).

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

Often, a function contains multiple effects, for example:

load in editorfunction combineEffectsguide/combineEffects: forall<a> () -> <pure,ndet> a() { ii: int = randomIntstd/core/randomInt: () -> ndet int() // non-deterministic errorstd/core/error: forall<a> (string) -> exn a("hi") // exception raising combineEffectsguide/combineEffects: () -> <exn,ndet,div|_e> _a() // and non-terminating }

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

load in editoralias purestd/core/pure: E = <divstd/core/div: X,exnstd/core/exn: X>

Many functions are polymorphic in their effect. For example, the map 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:

load in editormap : (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:

load in editorwhile : ( pred : () -> <divstd/core/div: X|e> boolstd/core/bool: V, action : () -> <divstd/core/div: X|e> () ) -> <divstd/core/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/div: X|e>. The final effect of the whilestd/core/while: forall<e> (predicate : () -> <div|e> bool, action : () -> <div|e> ()) -> <div|e> () function is of course also <divstd/core/div: X|e>. Indeed, since while may diverge depending on the predicate its effect must include possible 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/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

load in editorfunction looptestguide/looptest: () -> <pure,ndet> ()() { whilestd/core/while: forall<e> (predicate : () -> <div|e> bool, action : () -> <div|e> ()) -> <div|e> () { oddstd/core/odd: (i : int) -> bool(randomIntstd/core/randomInt: () -> ndet int()) } { errorstd/core/error: forall<a> (string) -> exn a("<b>") } }

In the above program, Koka infers that the predicate odd(random-int()) has effect <ndetstd/core/ndet: X|e1> while the action has effect <exnstd/core/exn: X|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: X|ndetstd/core/ndet: X|divstd/core/div: X|e3> for some e3 (which can be seen by hovering over the looptestguide/looptest: () -> <pure,ndet> () identifier)

The fibonacci numbers are a sequence where each subsequent fibonacci number is the sum of the previous two, where fib(0) == 0 and fib(1) == 1. We can easily calculate fibonacci numbers using a recursive function:

load in editorfunction fibguide/fib: (n : int) -> div int(nn: int : intstd/core/int: V) : divstd/core/div: X intstd/core/int: V { if (nn: int <=std/core/(<=).1: (int, int) -> bool 0) then 0 elif (nn: int ==std/core/(==).1: (int, int) -> bool 1) then 1 else fibguide/fib: (n : int) -> div int(nn: int-std/core/(-): (int, int) -> int1) +std/core/(+): (int, int) -> int fibguide/fib: (n : int) -> div int(nn: int-std/core/(-): (int, int) -> int2) }

Note that the type inference engine is currently not poweful enough to prove that this recursive function always terminates, which leads to inclusion of the divergence effect divstd/core/div: X in the result type. We can avoid this by using the repeatstd/core/repeat: forall<e> (n : int, action : () -> e ()) -> e () function and some imperative updates, and increase the efficiency too:

load in editorfun fib2guide/fib2: (n : int) -> int(nn: int) { var xx: ref<_h,int> := 0 var yy: ref<_h,int> := 1 repeatstd/core/repeat: forall<e> (n : int, action : () -> e ()) -> e ()(nn: int) { y0y0: int = yy: ref<_h,int> yy: ref<_h,int> :=std/core/set: forall<h,a> (ref : ref<h,a>, assigned : a) -> (write<h>) () xx: ref<_h,int>+std/core/(+): (int, int) -> intyy: ref<_h,int> xx: ref<_h,int> :=std/core/set: forall<h,a> (ref : ref<h,a>, assigned : a) -> (write<h>) () y0y0: int } returnreturn: int xx: ref<_h,int> }

The var declaration declares a variable that can be assigned too using the (:=) operator. In contrast, a regular equality sign, as in y0 = y introduces an immutable value y0. For clarity, one can actually write val y0 = y for such declaration too but we usually leave out the val keyword.

Local variables declared using var are actually syntactic sugar for allocating explicit references to mutable cells. A reference to a mutable integer is allocated using r = ref(0) (since the reference itself is actually a value!), and can be derefenced using the bang operator, as !r. The desugared version of our previously fibonacci function can be written using explicit references as

load in editorfun fib3guide/fib3: (n : int) -> int(nn: int) { val xx: ref<_h,int> = refstd/core/ref: forall<h,a> (value : a) -> (alloc<h>) ref<h,a>(0) val yy: ref<_h,int> = refstd/core/ref: forall<h,a> (value : a) -> (alloc<h>) ref<h,a>(1) repeatstd/core/repeat: forall<e> (n : int, action : () -> e ()) -> e ()(nn: int) { y0y0: int = !std/core/(!).1: forall<h,a,e> (ref : ref<h,a>) -> <read<h>|e> a with hdiv<h,a,e>yy: ref<_h,int> yy: ref<_h,int> :=std/core/set: forall<h,a> (ref : ref<h,a>, assigned : a) -> (write<h>) () !std/core/(!).1: forall<h,a,e> (ref : ref<h,a>) -> <read<h>|e> a with hdiv<h,a,e>xx: ref<_h,int> +std/core/(+): (int, int) -> int !std/core/(!).1: forall<h,a,e> (ref : ref<h,a>) -> <read<h>|e> a with hdiv<h,a,e>yy: ref<_h,int> xx: ref<_h,int> :=std/core/set: forall<h,a> (ref : ref<h,a>, assigned : a) -> (write<h>) () y0y0: int } returnreturn: int !std/core/(!).1: forall<h,a,e> (ref : ref<h,a>) -> <read<h>|e> a with hdiv<h,a,e>xx: ref<_h,int> }

As we can see, using var declarations is quite convenient since such declaration automatically adds a dereferencing operator to all occurrences except on the left-hand side of an assignment.

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

Clearly, the effect of the body of fib3guide/fib3: (n : int) -> int is ststd/core/st: H -> E<h>; but when we hover over fib3guide/fib3: (n : int) -> int, we see the type inferred is actually the totalstd/core/total: E effect: (n:intstd/core/int: V) -> intstd/core/int: V. Indeed, even though fib3guide/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/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/run: forall<e,a> (action : forall<h> () -> <st<h>|e> a) -> e a function (corresponding to runST in Haskell) to discard the ststd/core/st: H -> E<h> effect.

The Garsia-Wachs algorithm is nice example where side-effects are used internally but where the algorithm itself behaves like a pure function, see the garsiaWachs sample online.

Enough about effects and imperative updates. Let's look at some more functional examples :-) For example, cracking Caesar encoded strings:

load in editor// The letter frequency table for English val englishguide/english: list<double> = [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 function percentguide/percent: (n : int, m : int) -> double( nn: int : intstd/core/int: V, mm: int : intstd/core/int: V ) { 100.0 *std/core/(*).1: (double, double) -> double (nn: int.doublestd/core/double: (int) -> double /std/core/(/): (double, double) -> double mm: int.doublestd/core/double: (int) -> double) } function rotateguide/rotate: forall<a> (xs : list<a>, n : int) -> list<a>( xsxs: list<_a>, nn: int ) { xsxs: list<_a>.dropstd/core/drop: forall<a> (xs : list<a>, n : int) -> list<a>(nn: int) +std/core/(+).2: forall<a> (xs : list<a>, ys : list<a>) -> list<a> xsxs: list<_a>.takestd/core/take: forall<a> (xs : list<a>, n : int) -> list<a>(nn: int) } // Calculate a frequency table for a string function freqsguide/freqs: (s : string) -> list<double>( ss: string : stringstd/core/string: V ) : liststd/core/list: V -> V<doublestd/core/double: V> { nn: int = ss: string.countstd/core/count.1: (s : string, pred : (char) -> bool) -> int( isLowerstd/core/isLower: (c : char) -> bool ) // count of lowercase letters in "s" lowerslowers: list<char> = liststd/core/list.1: (lo : char, hi : char) -> total list<char>('a','z') // list of the lower-case letters returnreturn: list<double> lowerslowers: list<char>.mapstd/core/map: forall<a,b,e> (xs : list<a>, f : (a) -> e b) -> e list<b>( fun(cc: char) { percentguide/percent: (n : int, m : int) -> double( ss: string.countstd/core/count: (s : string, c : char) -> int(cc: char), nn: int ) } ) } // Calculate how well two frequency tables match according // to the ''chi-square'' statistic. function chisqrguide/chisqr: (xs : list<double>, ys : list<double>) -> double( xsxs: list<double> : liststd/core/list: V -> V<doublestd/core/double: V>, ysys: list<double> : liststd/core/list: V -> V<doublestd/core/double: V> ) : doublestd/core/double: V { returnreturn: double 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>, fun(xx: double,yy: double){ ((xx: double -std/core/(-).1: (double, double) -> double yy: double)^std/core/(^).1: (d : double, p : double) -> double2.0)/std/core/(/): (double, double) -> doubleyy: double } ).sumstd/core/sum.1: (xs : list<double>) -> double() } // Crack a Caesar encoded string function crackguide/crack: (s : string) -> string( ss: string : stringstd/core/string: V ) : stringstd/core/string: V { tabletable: list<double> = freqsguide/freqs: (s : string) -> list<double>(ss: string) // build a frequency table for "s" chitabchitab: list<double> = liststd/core/list: (lo : int, hi : int) -> total list<int>(0,25).mapstd/core/map: forall<a,b,e> (xs : list<a>, f : (a) -> e b) -> e list<b>( fun(nn: int) { // build a list of chisqr numbers for each shift between 0 and 25 chisqrguide/chisqr: (xs : list<double>, ys : list<double>) -> double( tabletable: list<double>.rotateguide/rotate: forall<a> (xs : list<a>, n : int) -> list<a>(nn: int), englishguide/english: list<double> ) }) minmin: double = chitabchitab: list<double>.minimumstd/core/minimum.1: (xs : list<double>) -> double() // find the mininal element shiftshift: int = chitabchitab: list<double>.indexOfstd/core/indexOf: forall<a> (xs : list<a>, pred : (a) -> bool) -> int( fun(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 returnreturn: string ss: string.encodeguide/encode: (s : string, shift : int) -> string( shiftshift: int ) }

The val keyword declares a static value. In the example, the value englishguide/english: list<double> is a list of floating point numbers (of type doublestd/core/double: V) denoting the average frequency for each letter. The function freqsguide/freqs: (s : string) -> list<double> builds a frequency table for a specific string, while the function chisqrguide/chisqr: (xs : list<double>, ys : list<double>) -> double calculates how well two frequency tables match. In the function crackguide/crack: (s : string) -> string these functions are used to find a shift value that results in a string whose frequency table matches the englishguide/english: list<double> one the closest -- and we use that to decode the string. Let's try it out in the editor!

Being a function-oriented languague, Koka has powerful support for function calls where it supports both optional and named parameters. For example, the function substringstd/core/substring: (s : string, start : int, len : ?int) -> string takes a string, a start position, and the length len of the desired substring:

load in editorfunction worldguide/world: () -> string() { returnreturn: string substringstd/core/substring: (s : string, start : int, len : ?int) -> string("hi world", 3, 5) // returns "world" }

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

load in editorfunction world2guide/world2: () -> string() { returnreturn: string "hi world".substringstd/core/substring: (s : string, start : int, len : ?int) -> string( len=5, start=3 ) }

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 sublistguide/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:

load in editorfunction sublistguide/sublist: forall<a> (xs : list<a>, start : int, len : ?int) -> list<a>( xsxs: list<_a> : liststd/core/list: V -> V<aa: V>, startstart: int : intstd/core/int: V, lenlen: ?int : intstd/core/optional: V -> V = xsxs: list<_a>.lengthstd/core/length.2: forall<a> (xs : list<a>) -> int ) : liststd/core/list: V -> V<aa: V> { if (startstart: int <=std/core/(<=).1: (int, int) -> bool 0) returnreturn: list<_a> xsxs: list<_a>.takestd/core/take: forall<a> (xs : list<a>, n : int) -> list<a>(lenlen: int)std/core/(): () match(xsxs: list<_a>) { 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<_a>) -> xxxx: list<_a>.sublistguide/sublist: forall<a> (xs : list<a>, start : int, len : ?int) -> list<a>(startstart: int-std/core/(-): (int, int) -> int1, lenlen: int) } }

Hover over the sublistguide/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/int: V type signified by the question mark: ?intstd/core/int: V.

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:

load in editorstruct personguide/person: V( ageage: int : intstd/core/int: V, namename: string : stringstd/core/string: V, realnamerealname: string : stringstd/core/string: V = namename: string ) val gagaguide/gaga: person = Personguide/Person: (age : int, name : string, realname : ?string) -> person( 25, "Lady Gaga" )

Every struct (and other data types) come with constructor functions to create instances, as in Personguide/Person: (age : int, name : string, realname : string) -> person(25,"Gaga"). Moreover, these constructors can use named arguments so we can also call the constructor as Personguide/Person: (age : int, name : string, realname : string) -> person( name = "Lady Gaga", age = 25, realname = "Stefani Joanne Angelina Germanotta" ) which is quite close 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 ageguide/age: (person : person) -> int of a personguide/person: V as gaga.age (which is of course just syntactic sugar for age(gaga)).

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 birthdayguide/birthday: (p : person) -> person function that increments the ageguide/age: (person : person) -> int field:

load in editorfunction birthdayguide/birthday: (p : person) -> person( pp: person : personguide/person: V ) : personguide/person: V { returnreturn: person pp: person( age = pp: person.ageguide/age: (person : person) -> int +std/core/(+): (int, int) -> int 1 ) }

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

load in editorfunction copyguide/copy: (p : person, age : ?int, name : ?string, rname : ?string) -> person( pp: person, ageage: ?int = pp: person.ageguide/age: (person : person) -> int, namename: ?string = pp: person.nameguide/name: (person : person) -> string, rnamername: ?string = pp: person.realnameguide/realname: (person : person) -> string ) { returnreturn: person Personguide/Person: (age : int, name : string, realname : ?string) -> person(ageage: int, namename: string, rnamername: string) }

When arguments follow a data value, as in p( age = p.age+1 ), it is desugared to call this copy function, as in p.copy( age = p.age+1 ). Again, there are no special rules for record updates and everything is just function calls with optional and named parameters.

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

load in editortype colors { Red Green Blue }

Note that the layout rule seperates each *constructor* with a semi-colon, and we can also write this on one line as type colors { Red; Green; Blue }.

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

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

load in editortype number { Infinity Integer( i : intstd/core/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>):

load in editortype 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. For example, our earlier personguide/person: V struct, defined as

load in editorstruct personguide/person: V( age : intstd/core/int: V, name : stringstd/core/string: V, realname : stringstd/core/string: V = name )

desugars to:

load in editortype personguide/person: V { Personguide/Person: (age : int, name : string, realname : string) -> person( age : intstd/core/int: V, name : stringstd/core/string: V, realname : stringstd/core/string: V = name ) }

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 cotype and rectype that allow for co-inductive types, and arbitrary *recursive types* respectively.