I'm excited about Koka
It’s been a while since I’ve been excited about a new programming language.
I’ve learnt and used a number of languages, either because of necessity or curiosity, but there’s only been a few languages in the past 20+ years where I’ve thought “this could be my new favourite language”.
For a long time Python was my preferred language for its simplicity, and then StratifiedJS for its powerful approach to asynchrony (and JS interop). Since then most of my interest has been in statically typed languages, particularly OCaml and Rust.
I’ve used plenty of other languages for my day job, and I consider myself lucky to have a day job where I’m mostly writing Scala - a really good mix of “powerful language” and “something I can get paid to write”. But I’m a big believer that there should be a language which is great for nearly everything I want to do, and none of those are it.
Koka?
So when I came across Koka recently and realised how strongly it aligns with the kinds of things I like in a language, I got pretty excited! Of course, it’s far too early to know if it will stay that way as the language and ecosystem (hopefully!) grow and become production-ready, but for now I’m very optimistic.
Where I’m coming from
Above I mentioned a few languages which I’ve been impressed with over the years. To give you an idea of what I like (and dislike), here’s a quick overview of my favourite languages and their downsides:
OCaml
I have a soft spot for OCaml - it’s like a dramatically more approachable Haskell. It has a great type system, simple and efficient runtime, and I appreciate the fast startup compared to VM languages.
Downsides: The syntax is hard to love. Lack of typeclasses or implicits means you’re forever specifying which map
function to call (List, Array, Lwt, etc), so code tends to be verbose and hard to refactor. Composing the appropriate functions every time you want to log some arbitrary structure can be amazingly frustrating. Build tooling is pretty nice these days with dune
, but package management with opam
is still quite painful.
Rust
Rust is an absolutely brilliant language. If I were writing low-level OS code or performance-critical code, I’d use Rust, no question. The power-to-convenience ratio is amazing. Cargo is great.
Downsides: The convenience doesn’t necessarily extend to many FP idioms. Rust gives you the tools to do things right, but it can take a lot of work. Basically, Rust can do high-level things (like async) but it still forces a lot of low-level concerns to permeate your codebase, which you don’t want or need to care about if efficiency isn’t your number one priority.
Scala
Scala has a high quality, reliable and extensive FP ecosystem. You can do pretty much anything in Scala, and the language is powerful enough to implement all kinds of useful abstractions.
Downsides: it’s a broad, complex language which can be hard to teach and navigate. The JVM legacy makes it a poor fit for CLI applications - it’s fast to run, but slow to start. FP purity is a matter of diligence, it’s incredibly easy to violate expectations by invoking code that throws exceptions, uses mutation, blocks the thread etc. Also I hate dealing with sbt
, but it’s too entrenched to make me seriously consider alternatives.
Koka: Functional Programming with algebraic effects
Koka is a functional programming language. It’s eager like OCaml, not lazy like Haskell. It uses reference counting instead of a Garbage Collector.
And the big ticket item: it is built around algebraic effects - “koka” is Japanese for “effect”. Rust spent most of its innovation tokens on ownership, Koka spends it on effects.
(I’m aware that OCaml 5 has dynamically typed algebraic effects, which are interesting but much less so than statically typed ones, to me at least)
Algebraic effects: power
Algebraic effects is a bit of an obtuse name, they’re best understood from a mechanical perspective as “resumable exceptions”. With exceptions you can throw an exception and have it propagate up the stack to the nearest catch
statement. From there you can do some more code and then return or throw another exception.
Effects allow you to call some function that the effect defines, and have that propagate up the stack to the nearest handler. Like catch
you can perform some code and then return, but there’s another option: you can resume the code that threw the exception, as if the throw
were calling a function and receiving its result. But it’s not a function you have a (lexical) reference to, it’s a function which is resolved dynamically via the callstack.
Obviously for exceptions resuming is a terrible idea, but it’s extremely powerful for other types of control flow. The easiest to appreciate is async
. A number of languages support async/await
syntax which allows you to write synchronous-looking code with asynchronous runtime behaviour. Adding this to a compiler is a massive undertaking.
But adding async in Koka amounts to a few hundred lines of code, none of it in the compiler. Effects allow everyday library code to implement an async system which captures a continuation and hands that off to the underlying scheduler, while having the surface syntax unchanged from synchronous code. The only change is the addition of async
to the set of effects a function requires.
Many languages do support async/await but lack support for related concepts like cancellation. I love that in Koka this (and many other interesting execution concepts) is a library concern which lends itself to experimentation and evolution, rather than something that can only be implemented as a huge modification to both the language and compiler.
Algebraic effects: usage
Effect types never apply to values, only to functions. fun foo(): io ()
means that foo
returns unit, but requires the io
effect in order to evaluate. There is no such thing as an io ()
value. When you call a function, you can only do so if the effect is available, and the result you get back is the value type.
An effect can be “available” in two ways. The most common way is that the caller also requires that effect. Just like in monadic programming, if you’ve got an IO<()>
then you’ll also need to return an IO<_>
. With effects you will only call an io ()
function from another io
function.
An effect can also be available by handling it. io
can only be handled by the runtime, but other effects can be handled in user code. e.g the exn
effect represents the ability to throw exceptions:
fun inner(): exn ()
throw("oh no!")
fun outer(): error<()>
// handle `throw-exn` (fail) and `return` (succeed) for the `exn` effect
with handler <exn> {
final ctl throw-exn(e) { Error(e) }
return(value) { Ok(()) }
}
inner()
The outer
function does not need the exn
effect, because it’s handled that effect for inner
and turned it into an error
type with Ok
/ Error
variants. In practice you’d just use the try
function to handle errors rather than writing an exn
handler, this is just for illustration.
So far, that’s just monads with a different syntax. But the crucial part of effect types is how they compose - a function has a set of effects. So you might have foo(state: ref<global>): <exn,st<global>> ()
. That means foo can fail (exn), and it needs to read and write to the global heap (state
is a mutable reference cell, reading or writing to it requires the corresponding read
or write
effect, and st
is just an alias for read
, write
and alloc
, for reading writing and creating refs).
In monad-land, this is where we might enter monad transformer territory, with a StateT IO
maybe? Or an IOT State
? I don’t know. But in Koka, it’s just two effects that we need. And there’s no need to wrap / unwrap the various layers of a monad to get at the “right” effect level, you simply call functions that require effects, and the result is a function requiring all the effects you depend on.
To illustrate the difference, here’s an example which combines state and errors in Haskell. I borrowed it from this article, because I have done a bit of Haskell but I still couldn’t write this myself:
type StoreM = StateT (Map String Int) (Either String)
note :: a -> Maybe b -> Either a b
note msg = maybe (Left msg) Right
save :: String -> Int -> StoreM ()
save k v = modify (Map.insert k v)
load :: String -> StoreM Int
load k = do
store <- get
lift $ note ("the key " ++ k ++ " is missing") (Map.lookup k store)
operation :: StoreM Int
operation = do
save "x" 1
save "x" 2
save "y" 123
x <- load "x"
y <- load "y"
save "z" (x + y)
load "z"
operation
and save
are straightforward, but I wouldn’t be able to write load
and note
without reading a few docs first.
Here’s the equivalent Koka code which is pretty straightforward once you know Koka’s syntax:
alias stored = hash-map<string, int>
alias store = ref<global, hash-map<string, int>>
fun save(store: store, k: string, v: int): st<global> ()
store.modify fn(s)
s := s.insert(k, v)
fun load(store: store, k: string): <exn,read<global>> int
match (!store).get(k)
Just(v) -> v
Nothing -> throw("the key " ++ k ++ " is missing")
fun operation(store: store): <exn,st<global>> int
store.save("x", 1)
store.save("x", 2)
store.save("y", 123)
val x = store.load("x")
val y = store.load("y")
store.save("z", x + y)
store.load("z")
I think this is an absolutely wonderful improvement for readability and general understanding, as well as type inference. There’s simply so much less manual machinery to think about. And thinking of “the set of effects I require” feels quite natural.
There’s one odd thing here: it feels very OOP. This feels jarring because humans are pattern recognition machines, but it still is FP, and I believe it retains all the important benefits of FP. Speaking of…
Effects: no more referential transparency?
A quick refresher: referential transparency means you should be able to substitute an expression for a variable-holding-that-expression without changing semantics.
So in Scala, there’s no difference between these two pieces of code:
def foo(): IO[Unit] = ???
// foo happens twice
doItTwice(foo(), foo())
// foo still happens twice
val action: IO[Unit] = foo()
doItTwice(action, action)
In Koka, that’s not true (but it also wouldn’t type-check, so at least it’s not an accident waiting to happen). Calling foo()
evaluates its effects, and gives you the result. If you want to defer that you can pass the unevaluated function doItTwice(foo, foo)
, or have val action
be an anonymous lambda. You can use braces (suspenders!) to write a zero-argument lambda, so these two are equivalent:
val action1 = fn() foo()
val action2 = { foo() }
I’m not sure how this one sits with me. Some would say a language without referential transparency is not a “real” FP language. But I’m not sure how much it matters in practice. Maybe it is still referentially transparent, if you argue the difference between IO[T]
and T
is equivalent to the difference between () -> io T
and T
. If you alias IO<t> = () -> io T
, that would be awful for ergonomics but would it count as referential transparency? Not sure.
Either way, I’m fine with this in practice since it’s responsible for much of the readability gains in effect-using code.
Other features
Beyond algebraic effects, Koka has a handful of other distinguishing features:
No Garbage Collector
I flip-flop between this being a minor detail and a huge deal. Koka uses reference counting which is technically garbage collection, but it doesn’t have the overheads and unpredictability associated with a tracing GC. It’s also technically possible to create cycles, but thanks to its FP and lack of general mutation, this is much less likely to be a problem in practice compared to e.g. Swift.
Koka’s reference counting uses some clever techniques to be competitive (in select benchmarks) with the best garbage collectors, while requiring much less runtime code and fewer decades of cutting-edge engineering investment.
Ultimately I’ve enjoyed how lean and embeddable Rust is, and Koka gives me the same vibes in a much higher level language. For performance sensitive use cases you’re more likely to want to embed Rust than Koka, but using WASM for frontend code is an embedding use case where Koka should be much nicer than Rust.
Dot selection
obj.function(value)
is always syntactic sugar for function(obj, value)
. This gives a natural left-to-right flow of methods as in OOP, but without the complexity of juggling both instance methods functions. Some OOP languages have ways to add extension methods to classes they didn’t define, but in Koka that’s just writing a function which accepts the given type as its first argument.
This left-to-right ordering makes IDE support nicer, since writing the value first allows the suggestions to be narrowed down to functions that accept that type, similar to OOP methods.
It does mean that any functions which are generic in the first argument will always be a valid suggestion, which could be noisy. Scala has similar problems with extension methods you can call on any value, IDEs present these as low priority suggestions. Koka should be able to do the same (maybe it already does).
OCaml (and many others) have a similar chaining operator where you can write obj |> method(value)
as syntactic sugar for method(value, obj)
. But that feels like an afterthought in OCaml which is used (and useful) inconsistently, whereas dot syntax is idiomatic and universal in Koka.
Qualified names and overloading
In OOP, the namespace of “possible function names” is per-class - different classes can use the same name without colliding. In FP, there are a lot of functions in one big shared namespace. If you have a map
function, then either:
- You need to qualify it everywhere, like OCaml’s
List.map(...)
- You need some system whereby the one and only
map
function does the right thing for any structure which supports the concept of “mapping”, like Haskell’s typeclasses
Koka has a novel approach: functions and variables can all have qualified names, like list/map
and array/map
. Both can be referred to as map
, but you can explicitly use list/map
if you need to disambiguate. But Koka also has support for overloading, where it’ll automatically pick the correct map
function if there’s only one in scope which matches the argument types given. So if you call map(somelist, ...)
that’s going to select list/map
without you needing to disambiguate.
Modules can be used to disambiguate, so you often don’t need to define the function using a qualified name. If you write a function called map
in the list
module, it can be referred to as list/map
.
This felt weird at first, but after a short time feels like a nice way to balance “one big namespace” with “simple function names”, without the complexity of Haskell’s typeclasses. The one downside is that errors can be a little tougher since if the call doesn’t match any function, you get all the possibilities listed. But you can (temporarily) disambiguate with the full name to get a more specific error message.
Implicit arguments
Koka supports implicit arguments which are resolved by a combination of both name and type, unlike Scala which only considers the type of an implicit argument. Here’s an example of an implicit in Scala:
object Foo {
implicit val show: Show[Foo] = ???
}
def print[T](value: T)(implicit S: Show[T]) {
println(s"Here is a ${S.show(value)}")
}
The equivalent in Koka would be:
fun foo/show(value: foo) { ... }
fun print<a>(value: a, ?show: (a) -> string) {
println("Here is a " ++ show(value))
}
- Because Scala’s implicit requires exactly one instance of a given type to be found, it adds extra ceremony (marking values as
implicit
) to avoid polluting the search space - There’s also a complex resolution process (e.g. companion objects of the type in question will be searched, even if they’re not in scope)
With Koka, implicits have to match the name and type. And all that’s searched is the lexical scope, there are no extra rules. Because of qualified names, it’s possible to have many functions called show
. If there’s only one that accepts a foo
type, then that’s the one it uses! If there’s multiple (or none), you’ll need to specify one explicitly.
This does increase the chances of implicitly resolving a value which happens to be in scope, but not intended for that purpose. But given that the name also needs to match, it doesn’t seem too likely in practice.
It can also mean that you need additional imports. E.g. currently the hash
functions for various types are defined in std/data/hash
, so you need to import that in order for those symbols to be available for hash-map
functions. This is all part of the community stdlib right now, it’s likely these hash functions would be defined more centrally once they become part of the official stdlib.
Cohesion and simplicity
One of Koka’s principals is minimal-but-general. Many languages (especially those who are young and not burdened with decades of production use) claim similar things, so I was prepared to be underwhelmed. Lest we forget one of the most complex build tools ever created was originally called Simple Build Tool.
It probably didn’t help that the “language basics” section started by describing all the various syntactic sugars which make parts of the syntax optional in certain situations, giving many different ways to write the same thing. I think these are useful and important for the “general” part of koka’s goals, but it does stand in contrast to the “minimal” goal.
I hope things go well enough that we see how these goals pan out after decades of supporting production use cases, but right now I buy it.
The effects system is clearly more general than other languages which have bespoke support for async, exceptions, and other specialized control flow.
And the features it does have tend to work well together. a.map(...)
would not be that useful if there could only be one function in scope called map
, nor would it be useful to require an implicit show
parameter if there could only be one such function in scope.
Qualified names allows a much broader namespace because names can overlap, and the type level constraints provide a pragmatic way to extract the right thing out of those overlapping definitions. I don’t know how often in practice this will be better or worse than the explicitness of objects and instance methods, but it’s clearly much simpler and uniform, which I appreciate. It’s also the simplest approach I’ve seen to resolve the “one big namespace for functions” constraint that all FP languages have.
Performance
I like the fact that Rust is so efficient, but Rust makes a lot of tradeoffs to get there. This is probably not the right tradeoff for me most of the time. To be honest, for the kinds of things I do Haskell and OCaml are perfectly fine performance-wise without bogging down logic with memory management concerns. In some cases I’m comparing performance to languages like ruby and python, where being “fast” is a comically low bar.
So while I don’t often need a high performance language, it feels nice to have that option. Koka’s creator has devoted a fair bit of research and effort into specific optimisations which can make (some) idiomatic FP code compile to a form which is competitive with C, which feels like a pretty good balance of “the compiler cares about this” but “I don’t have to constantly care about this”.
Koka: the hard parts
So far I’ve mostly been playing around with the effects side of Koka, since that’s the novel part I want to understand better. These are some issues I’ve run into so far:
You can’t refer to generic type parameters in the function body
When the compiler says my types are incorrect, I often like to annotate parts of them in order to close the gap between what I think and what the compiler thinks types are. In Koka, there seem to be a lot of situations where you can’t actually write a type down, which makes this hard.
I think the main cause for this is that type parameters in the function type are not bound in the function body. So this annotation (of val result
) is incorrect:
fun singleton<a>(value: a): list<a>
val result: list<a> = [value]
result
The problem here is that a
in the function signature can’t be referenced in the function body. So ascribing a type list<a>
in the body of a function is syntactic sugar for forall<a> list<a>
, i.e “a list of any type you like”, which obviously won’t compile. There doesn’t seem to be any advantage in not making a
reference “the one from the function signature”, so I’m hoping this can change in the future.
Local variables interfere with dot selection
When there’s a bunch of functions called location
, Koka uses overloading to figure out which one you mean based on the arguments you pass. So in foo.location
which desugars to location(foo)
, that’ll pick the single location
function whose argument types match - or fail if there isn’t exactly one.
The one issue I’ve found with this is when you also use some field’s name as a variable, e.g. val location = "..."
. A local variable in scope will always be used rather than looking for other overloads. That’s a good rule, but in this case it makes foo.location
a type error - that desugars to location(foo)
but location
is a string!
In these cases you still can access the field by using a qualified name (e.g. foo.file/location
), but that’s a bit ugly - I typically find a different name for my variable. Working around this isn’t hard, it’s understanding the error message which is the hard part. Especially when you’re working through a bunch of other errors and the code in question has no obvious connection to your change.
I don’t think this is problematic enough to change the language, but the compiler error could definitely be improved when foo.bar
doesn’t typecheck to highlight that bar
refers to a local variable.
Matching up effect types can be hard
This may be simply a learning curve thing, but I stumbled a lot when trying to get my effect type declarations to compile.
Part of this is the way that effect types combine. They are unordered like a set, but they’re not deduplicated like a set is (they’re referred to as a row rather than a set in the documentation).
For example, I thought this would work:
fun withLogging(action: () -> e a): <console|e> a
println("Starting action!")
action()
You can read this as accepting an action
function of type e a
(generic effect, generic return type). The resulting function returns the same type, but with the effect of <console|e>
, read as “console plus whatever e
is”.
That doesn’t work, because if e
already included the console effect, you’d have an effect type <console,console,...>
, which would require two levels of console handlers to be available.
The correct way to write this is by requiring the action to have a console
effect:
fun withLogging(action: () -> <console|e> a): <console|e> a
println("Starting action!")
action()
This says that action
has the console effect. Which really means action
may have the console effect, since the compiler will allow effect widening (a function can always be evaluated with more handlers available than it needs, it just won’t use them).
This does make sense, but can be a bit tedious since you often end up repeating the set of effects for both the action and return type, if you’re annotating types explicitly.
I also really struggled making effect types align. Here’s an example:
val pending: ref<h, list<thunk>> = ref([])
Gave me the error:
inferred effect: <alloc<$h>|$e>
expected effect: <alloc<$h1>|_e1>
Understanding why $h
(the “heap” parameter of a ref) is not equal to $h1
and $e
not equal to _e1
is not an easy task when none of those names are present (or even valid?) in the code I wrote.
I think the h
difference is another instance of not being able to refer to generic type parameters. And I believe the $e
/ _e1
thing fell out of that too, in that if you have a ref<h>
then its corresponding allocation effect is alloc<h>
, and since there was a difference in h
it affected both the type and the effect. But it’s not obvious from the error message, and I have since started using ref<global>
over ref<h>
because it leads to fewer type errors. I haven’t yet figured out why it’s useful that refs can be associated with different “heaps”, since I believe there’s only one in an actual program.
Compiler bugs
It says “experimental” on the tin for good reason!
So far I’ve run into a few compiler bugs when using effects in nontrivial ways, where the compiler generates code that crashes. In some cases I can get code that works by changing my effect type annotations, so I suspect I’m just running into codegen bugs (rather than typechecking bugs).
In some other cases I’ve been unable to get code which both compiles and runs, which is a shame. But given the language has such solid roots in research, I’m hopeful these are just minor bugs rather than larger flaws.
Summary
So far there’s a lot to love, and not a lot to put me off. That’s already a pretty amazing feat - I’m a fussy guy.
Koka is explicitly not ready for mainstream use, it’s still an experimental language. I’m really impressed with that language, and I get the feeling the core isn’t likely to significantly change, but I wouldn’t be surprised if the stdlib went through a few overhauls, and there’s no package manager yet.
So I don’t expect I’ll be writing real code in Koka any time soon, but it’s been a long time since I’ve been this excited about a new language. I’m definitely going to keep playing with it, and I might start posting more content that goes into details of my experiments and what I’m learning.