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