Effects are the obvious feature of Koka. But, it actually also has a lot of interesting syntactic features. It has universal call syntax, which it calls dot selection (i.e. f(a, b) is equivalent to a.f(b)). It has trailing closure syntax, similar to Ruby and Swift. You can even drop braces for trailing closures with indentation. Similarly, it supports a with statement which cleans up passing trailing closures as well. The example they use in the docs for that is:
with x <- list(1,10).foreach
println(x)
which is equivalent to this in Ruby:
(1..10).each { |i| puts i }
I think these features are interesting, and it makes it a very complete language vs. just a research language based on effects.
Koka is a great research language, probably (with Idris?) the one closer to being ready for real-world usage that isn’t widely used yet. In my mind Koka’s greatest claim to fame is an effect system that is actually usable for everyday programming. (By effect system, I mean the fact that the type-checker knows which effects the various parts of the program may perform; this is orthogonal to whether the effects are presented using monads or effect handlers, in fact Koka switched to effect handlers at some later point in its design.) There were a lot of attempts to have a usable effect system before – the most successful in terms of actual usage is basically Haskell’s mtl library – but most prove too cumbersome to use in practice.
Recently, Daan Leijen grew interested in low-level optimization of programming language runtimes, in particular (but not only) those that benefit from having a purely-functional language. Mimalloc, Perceus, etc. It’s a lot of fun, and it’s great that Koka (and more generally the MSR group, Lean as well I guess) is also having an impact this way.
This has really come a long way over the past few years! I think I’ll try it out over the holiday break. I wonder how hard it would be to write a STM similar to Haskell’s popular one…
Effects are the obvious feature of Koka. But, it actually also has a lot of interesting syntactic features. It has universal call syntax, which it calls dot selection (i.e.
f(a, b)
is equivalent toa.f(b)
). It has trailing closure syntax, similar to Ruby and Swift. You can even drop braces for trailing closures with indentation. Similarly, it supports awith
statement which cleans up passing trailing closures as well. The example they use in the docs for that is:which is equivalent to this in Ruby:
I think these features are interesting, and it makes it a very complete language vs. just a research language based on effects.
Koka is a great research language, probably (with Idris?) the one closer to being ready for real-world usage that isn’t widely used yet. In my mind Koka’s greatest claim to fame is an effect system that is actually usable for everyday programming. (By effect system, I mean the fact that the type-checker knows which effects the various parts of the program may perform; this is orthogonal to whether the effects are presented using monads or effect handlers, in fact Koka switched to effect handlers at some later point in its design.) There were a lot of attempts to have a usable effect system before – the most successful in terms of actual usage is basically Haskell’s
mtl
library – but most prove too cumbersome to use in practice.Recently, Daan Leijen grew interested in low-level optimization of programming language runtimes, in particular (but not only) those that benefit from having a purely-functional language. Mimalloc, Perceus, etc. It’s a lot of fun, and it’s great that Koka (and more generally the MSR group, Lean as well I guess) is also having an impact this way.
Previously submitted a couple years ago, but I found it interesting with the discussion of effects in OCaml 5
This has really come a long way over the past few years! I think I’ll try it out over the holiday break. I wonder how hard it would be to write a STM similar to Haskell’s popular one…