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

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:

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

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

{
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
```