Koka language

[bearophile]

Through Reddit I have found this new little language, that 
probably is meant to be just an experiment:

Reddit thread:
http://www.reddit.com/r/programming/comments/ycz6a/koka_a_function_oriented_language_with_effect/

LtU thread:
http://lambda-the-ultimate.org/node/4589

Slides:
http://research.microsoft.com/en-us/projects/koka/2012-overviewkoka.pdf

Little tutorial:
http://www.rise4fun.com/koka/tutorial

To see a bit larger examples:
http://www.rise4fun.com/Koka/


Koka is a function-oriented language, this means it's almost a 
functional language, with a syntax a bit similar to JavaScript, 
probably because today lot of programmers are used to JS syntax. 
Kika has kind of module-level type inference.

But the most important characteristic of Koka is its "effect 
inference". The effects are like the side effects prevented by 
the "pure" or "nothrow" of D. Koka is able to infer not just the 
plain types like int, list<int> or generic types like list<a>, 
but it's also able to infer the various effects of functions, 
avoiding the need to write them manually, see below.

Each Koka experession has associated its type, plus something 
like <div,exn,ndet>, this is a set of the effects of that 
expression. In D we do the opposite, we annote what effects a 
function doesn't have, and they are not organized in a set (the 
use of such sets offers significant advantages explained below).

Below there are some quotations from the slides, tutorial and the 
LtU thread. Fisrt I show some simple features , and later there 
are notes about its type system.

-----------------------

Dot notation, nice for chaining (this is the same as in D):

s.map(f)  ==  map(s, f)
s.caesar.map(to-upper).print

-----------------------

Optional parameters have a default value:

function 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)
   }
}

-----------------------

Named parameters can be used in any order:

function world() {
   "hi world".substring(len=5, start=3)
}

-----------------------

Structs are immutable by default: changing a field usually copies 
a struct:

function birthday(p : person) {
    p(age = p.age + 1)
}


Where structs are nested you use something like:

p(address = p.address(street = "Madison Sq"))

-----------------------

A mutable example (uses immutable references to the values, so 
it's similar to OcaML):

fun fib2(n)
{
   var x := 0
   var y := 1
   repeat(n) {
     y0 = y
     y := x+y
     x := y0
   }
   return x
}

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.

-----------------------

When we look at the types inferred for references, we see that x 
and y have type ref<h,int> which stands for a reference to a 
mutable value of type int in some heap h. The effects on heaps 
are allocation as heap<h>, reading from a heap as read<h> and 
writing to a heap as write<h>. The combination of these effects 
is called stateful and denoted with the alias st<h>.

-----------------------

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 "total" (or <>) and 
corresponds to pure mathematical functions.
- If a function can raise an exception the effect is "exn";
- if a function may not terminate the effect is "div" (for 
divergence);
- The combination of "exn" and "div" is "pure" and corresponds 
directly to Haskell's notion of purity;
- Non-deterministic functions get the "ndet" effect.
- The 'worst' effect is "io" 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:

function square1(x : int) : total int
{
   return x * x
}

function square2(x : int) : io int
{
   print( "a not so secret side-effect" )
   return x * x
}

function square3(x : int) : div int
{
   square3(x)
   return x * x
}

function square4(x : int) : exn int
{
   error("oops")
   return x * x
}

-----------------------

Often, a function contains multiple effects, for example:

function combine-effects()
{
   i = random-int()  // non-deterministic
   error("hi")       // exception raising
   combine-effects() // and non-terminating
}

The effect assigned to combine-effects are ndet, div, and exn. We 
can write such combination as a row of effects as <div,exn,ndet>. 
When you hover over the combine-effects identifiers, you will see 
that the type inferred is really <pure,ndet> where pure is a type 
alias defined as

alias pure = <div,exn>

-----------------------

(*)   : (int,int)    -> total int
(/)   : (int,int)    -> exn int
exec  : (turingMach) -> div bool
(!)   : (ref<h,a>)   -> read<h> a
print : (string)     -> io ()


Our approach: row-polymorphism, we use a set of effect labels:
- The empty effect is <> (total)
- An effect can be extended as <div|e>
- Sugar: <div,exn> == <div|<exn|<>>>
- Duplicates are ok: <div|<div|e>> == <div|e>

type ndet: !
type exn : !
type div : !
type rd  : !
type wr  : !
type heap<h> : H -> !

alias pure     = <div,exn>
alias read<h>  = <rd,heap<h>>
alias write<h> = <wr,heap<h>>
alias st<h>    = <rd,wr,heap<h>>
alias io       = <st<global>,div,exn,ndet>

-----------------------

When the effect is total we usually leave it out in the type 
annotation. [...] 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:

function square6( x : int ) : _e int
{
   print("I did not want to write down the io effect")
   return x*x
}

-----------------------

In D there is nothing like the "div" (or @nodiverge, to keep the 
style of the negative D annotations) annotation. Maybe it's hard 
to enforce this effect in a mostly imperative language like D, I 
don't know.

On LtU he/they explains why the "div" (divergence) annotation 
type is useful:

>The presence of divergence complicates reasoning about the 
>program. For example, a piece of code on which no other code has 
>data dependencies upon can be discarded without affecting 
>referential transparency, under some restrictions on its side 
>effects. Of course, diverging code should not be discarded. 
>Keeping track of an upper-bound on divergence allows such 
>reasoning, e.g. in an optimizing compiler. While not being a 
>tight upper bound (which is undecidable anyway), such inference 
>is an easy bound. I conjecture a lot of basic pattern matching 
>code fits this criteria (and is probably the code we want to 
>optimise away too). However, I have no hard evidence supporting 
>this conjecture, nor know of studies examining this question. 
>Another reason for tracking divergence is suitability to run on 
>different architectures. The application I refer to is database 
>queries, where recursive code cannot be run directly on the DB 
>engine, even if it does terminate. (The system I saw this in was 
>Wadler&co.'s Links web programming language.) 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.<

-----------------------

The effects analysis works with polymorphic functions too:

Polymorphic effects

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 : list<a>, f : (a) -> e b) -> e list<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 while function which 
has type:

load in editorwhile : ( pred : () -> <div|e> bool, action : () -> 
<div|e> () ) -> <div|e> ()

The while function takes a predicate function and an action to 
perform, both with effect <div|e>. The final effect of the while 
function is of course also <div|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 while forces the 
predicate and action to have exactly the same effect <div|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 looptest()
{
   while { odd(random-int()) }
   {
     error("<b>")
   }
}

In the above program, Koka infers that the predicate 
odd(random-int()) has effect <ndet|e1> while the action has 
effect <exn|e2> for some e1 and e2. When applying while, those 
effects are unified to the type <exn|ndet|div|e3> for some e3 
(which can be seen by hovering over the looptest identifier)

Bye,
bearophile