Koka: Strongly typed functional-style language with effect types and handlers
koka-lang.github.io
koka-lang.github.io
Koka: A fast functional programming language with algebraic effects - https://news.ycombinator.com/item?id=38421003 - Nov 2023 (2 comments)
The Koka Programming Language - https://news.ycombinator.com/item?id=28335043 - Aug 2021 (2 comments)
Koka: A Functional Language with Effects - https://news.ycombinator.com/item?id=27710267 - July 2021 (12 comments)
A Tour of Koka (an elegant programming language with Algebraic Effects) - https://news.ycombinator.com/item?id=26292411 - Feb 2021 (1 comment)
An Introduction to the Koka Programming Language - https://news.ycombinator.com/item?id=14647415 - June 2017 (1 comment)
Koka – A function-oriented programming language - https://news.ycombinator.com/item?id=10131071 - Aug 2015 (10 comments)
Koka a function oriented language with effect inference - https://news.ycombinator.com/item?id=4407415 - Aug 2012 (1 comment)
FP2: Fully In-Place Functional Programming [pdf] - https://news.ycombinator.com/item?id=36471591 - July 2023 (24 comments)
Perceus: Garbage Free Reference Counting with Reuse [pdf] - https://news.ycombinator.com/item?id=25464354 - Dec 2020 (44 comments)
Implementing Algebraic Effects in C - https://news.ycombinator.com/item?id=14887341 - July 2017 (21 comments)
> Perceus is an advanced compilation method for reference counting. This lets Koka compile directly to C code without needing a garbage collector or runtime system! This also gives Koka excellent performance in practice.
Effectful functional language that compiles to C? Sounds great.
While restarts can be visible or not, I believe there is no such mechanism for handlers. However, handlers can be effectively invisible/transparent by declining to handle a condition, which they can do simply by returning instead of perpetrating a non-local transfer.
Also, there doesn't seem to be an API in Common Lisp for calculating the handlers visible at a given point for a condition of a given type. So that means that the ability of a handler to decline a condition is pretty much as good as a visibility mechanism.
I particularly enjoyed this presentation, which is what sold it to me as a good idea worth spending some time on: https://youtu.be/6OFhD_mHtKA
OCaml 5.0 also interestingly includes an effect handler system: https://v2.ocaml.org/manual/effects.html
https://koka-lang.github.io/nodec/api/group__effect.html
On GitHub:
https://github.com/koka-lang/libhandler
I believe it grew out of this prior work:
The reason Koka's GC is interesting despite being based on reference counting is that its ownership system eliminates most of these reference checks at compile time - and additionally can tell whether to use atomic RC (slow but threadsafe for shared data) or non-atomic RC (fast but only threadsafe when data is moved across threads, not shared). This ownership analysis is very similar to what some other languages like Nim do (except Nim differs in not allowing atomic RC at all).
The other strange terminology that is occasionally tossed around in Koka documentation is "garbage free": Koka takes this to mean that at any given point in the program, there is no memory waiting to be freed. This is because the ownership analysis lets the compiler know exactly where the last use (or possible last use) is and insert destructors accordingly. All of that has made Koka's GC algorithm fast and low-overhead enough that it's competitive with state-of-the-art tracing GCs (specifically, OCaml's GC). I haven't seen benchmarks comparing it to manual memory management or strict ownership systems but that's not terribly the point - manual memory management is unsafe and strict ownership is complicated + inexpressive on occasion. Koka's system might just be the best you can get, with those tradeoffs in mind.
Anyway, this doesn't answer your question at all. Sorry. I hope it's interesting, though.
It's in the same category as Swift, yes, but much improved: Swift does not do ownership analysis to get rid of counts (though I've heard they're looking at alternative region-based approaches), and their counts across threads are always atomic (and thus slow).
Reference counting has traditionally led to worse performance than tracing. So even though I get the desire to think of it as separate because it's just transparently replacing your allocator / deallocator with one that does a little bit more instead of having a whole separate tracing collector program, I'd still probably refer to both tracing and reference counting as "garbage collection", and then refer to them + ownership systems (+ regions + everything else new) as "memory management techniques".
The overlap in implementation techniques between tracing and reference counting is interesting. You might enjoy this paper: https://dl.acm.org/doi/10.1145/1028976.1028982
This makes it possible for fold to free all the Cons cells as it is mapping over it. The reuse analysis is cool, too, with in-place updates of structures that won't be referenced again.
[1] https://koka-lang.github.io/koka/doc/book.html [2] https://www.microsoft.com/en-us/research/publication/perceus... (see section 2.2)
(Source: https://www.microsoft.com/en-us/research/project/koka/)
Pretty comical to hear the words "easy to reason about" and "category theory" in the same sentence.
With apologies to the Haskellers, any time "category theory" is mentioned I feel myself shying away, prior experience teaching me that those words mean "you will spend the majority of your time working around the type system "; and, "we have more data types than individual bits of data that those types describe".
A little type system goes a long way, and there's such a thing as too much in my opinion.
I was initially interested because of algebraic effects in the language because I'm told they're basically the same as common lisp conditions. I really liked learning about conditions and I wish they were in more languages. I must confess I am less interested now.
Its innovation (they claim) is that it deallocates objects immediately as soon as it can prove that the object is not referenced any more. Not at the end of a lexical scope, like C++ smart pointers and Rust, but immediately after the last use of the object.
One big concern was that there's a lot of pre-existing unsafe code that could rely on the drop being at the end of the scope, and not earlier. And you could imagine where, in a world with early drop, maybe you write some unsafe that's sound, but then the safe code changes, something gets dropped earlier, and now it's not sound anymore.
This doesn't mean that this affects Koka, I haven't spent any time with it yet and so I don't mean to imply this is the wrong decision, just showing some related work.
Granted Common Lisp is not statically typed and the type system support for effects is a major part of the utility of algebraic effects in Koka, but otherwise they do look remarkably similar to me, both offering a form of delimited continuation that allows you to write code that can call out to a non-local handler that is set up the call stack, and which can itself return control to the caller.
CL's condition system is one of the (possible) applications of an algebraic effect system (implemented using delimited continuations). Schemes have dynamically typed (delimited) continuations, for example.
Agreed.
The purpose of "types" is to make the program easier to understand, because the invariants expressed as type-declarations hold at all times of the program execution. That makes it EASIER to reason about the program, in other words makes it easier to understand your program and what it is doing, by understanding what it cannot be doing, meaning violating its type-constraints.
But now IF the type-declarations-language becomes highly advanced and thus complex and difficult to understand, that potentially makes your program more DIFFICULT to understand.
So it's good to keep the purpose of type-systems in mind while thinking about their benefits. We declare types only so that we and others can better understand what our programs are doing.
Of course if the program is small, it is typically easy to understand and may be even easier to understand without them.
While it's quite easy to understand what e.g. `c = a + b;` in C does, reasoning about it is comparably hard, as there can be UB (overflow of a signed integer type) involved.
In the extreme, when you have an actual proof (in a dependently typed language), you only have to understand it, but no need to reason about it as the proof is already there ;)
[insert some dependently typed vector example here :D]
I don't agree with this. Part of the benefit of static types is to make it easier for programmers to reason about programs. But part is also to make it easier for compilers to reason about programs. By encoding more invariants in the type system it is possible to turn a larger class of bugs into compiler errors.
I mean people cope with the horrible complexity of TypeScript just fine and that system doesn't even give you the benefit of being sound.
I have hated parts of the TS type system with passion but this is the first time I'm hearing about unsoundness. Would you mind elaborating?
For example: https://www.typescriptlang.org/docs/handbook/type-compatibil...
https://www.typescriptlang.org/docs/handbook/type-compatibil...
Or the type of an array and its elements:
const arr : number[] = [1]
const this_is_actually_undefined : number = arr[456]
const correct_type : number | undefined = arr[idx]
Thanks so much!
A similar constraint will apply to algebraic effects, which is why they're algebraic: only if your code directly depends on some effect will you have to care about effects.
It depends entirely on what those effects and dependencies actually are. If you really want to, you can use an effect system as a dynamically scoped imperative language, just like you can write all your Haskell code in `IO` or use exceptions for control-flow in C++. The value proposition is that you have to do it on purpose.
There's not much that can be said about how effects, in general, are intended to be used. Algebraic effects subsume basically every control flow construct in common use: exceptions, transactional semantics, cooperative multitasking, search, probabilistic programming, IO... non-delimited continuations are the only exception I can think of. Unless you only ever write provably-total pure functions, you're always using effects of some sort. And even then, you might want to think of your program as effectful even when you don't have to: reading `a -> Maybe b` as "`a -> b` with the possibility of failure" is a classic example.
Personally I would recommend Haskell. Native row types are coming "eventually" and always will be, so there's some ceremony involved, but it's the ecosystem with by far the best alternative solutions to the problems algebraic effects are supposed to deal with: idiomatic javascript can make any programming discipline look good, whereas it'll be much more illuminating to compare algebraic effects to a more traditional `mtl`-style approach.
https://www.microsoft.com/en-us/research/publication/fiptree... https://www.microsoft.com/en-us/research/publication/tail-re... https://www.microsoft.com/en-us/research/publication/fp2-ful...
The implications for things like data science frameworks and spreadsheets are particularly interesting. Perhaps we are within reach of a much more equational approach to programming with high performance.
In the code snippet, they define a "yield", and somehow this magically works with the call after that of `traverse`. What happens when you are deeper in a call stack and you accidentally or on purpose have to redefine yield? What if you want to use a generator in a generator?
Also, the `fun yield( x : a ) : ()` syntax is highly unintuitive. It _takes_ an int and returns empty? So it's just a continuation? And magically it transfers control flow to the correct place? How does it know where that is?
You also have to define the name "yield" thrice, once as the "effect declaration", and then twice as a function, once before the call to traverse, and once inside the effect declaration.
These are questions you don't even need to worry about when the handler is a continuation (function) that you pass in as an argument.
There's also a problem that koka seems to ignore, that for resumable coroutines of execution, you really want 2 kinds of resumptions. One that overwrites the `ret` address of the coroutine, and one that does not. The former is useful for generators like `traverse`, where you want to return to just after the latest call site, while the latter is useful for things like `throw`, where you always want to return to the first call site.
I don't know guys. These "algebraic" effects just seem like really bad syntax sugar over delimited continuations.
With `with` you explicitely set the effect handler, no magic involved.
> Also, the `fun yield( x : a ) : ()` syntax is highly unintuitive. It _takes_ an int and returns empty? So it's just a continuation?
A function that does not return anything is (the poster child of) an impure function, that does nothing else but an (side) effect. That's why you need to call it as an effect and not a "normal" (pure) function.
> And magically it transfers control flow to the correct place? How does it know where that is?
It doesn't have to. The hidden `run` function (or whatever you want to call it) of the effect systém that actually calls the right effect handler has to know about that.
The run function does something like (simplified)
- see, that a effect handler with ID 'yield' is called
- call the (currently registered) handler for 'yield' with the given arguments
- call the continuation with the result of the handlerAfter that depends on whether a continuation actually needs to be captured or not. Many useful effects can be implemented as `val` or `fun` clauses which can be called / accessed in place without any unwinding of the stack. Only in cases where a continuation is required is the continuation built up.
effect ctl yield( i : int ) : bool
See bottom of this section https://koka-lang.github.io/koka/doc/book.html#sec-handling.
When handling the effect you don't 'define' the name, you implement it. Of course you have to mention the name then, just like e.g. with interface implementations
It's really trickier than algebraic effects make it seem though. Haskell-ish "monad transfomers" as a stack of wrappers may pick concrete ordering of effects in advance (e.g. there's difference between `State<S, Result<E, T>>` and `Result<E, State<S, T>>`, using Rust syntax), but effect systems like one in Koka either have to do the same decision by using specific order of interpreters, or by sticking to single possible ordering, e.g. using one, more powerful monad. And then there're questions around higher order effects - that is, effects with operations that take effectful arguments - because they have to be able to "weave" other effects through themselves while preserving their behaviour, and this weaving seems to be dependent on concrete choice of effects, thus not being easily composable. In a sense, languages like Koka or Unison have to be restricted in some way, giving up on some types of effects. I'm not saying that's a bad thing though, it's still a improvement over having single effect (IO) or no effects at all.
This is even worse in Rust, which requires you to have a separate implementation for every effect as well (since it doesn't have higher kinded types)
This is more a weakness of Haskell's standard library (which is despite its reputation not very friendly to category theory) than an inherent problem with monads. A more general `map` would look something like this
class Category c => FunctorOf c f where
map :: c a b -> c (f a) (f b)
fmap :: FunctorOf (->) f => (a -> b) -> f a -> f b
fmap = map
type Kleisli m a b = a -> m b
mapM :: (Monad m, FunctorOf (Kleisli m) f) => (a -> m b) -> f a -> m (f b)
mapM = map
type Op c a b = c b a
contramap :: FunctorOf (Op (->)) f => (a -> b) -> f b -> f a
contramap = map
type Product c d (a,x) (b,y) = (c a b, d x y)
bimap :: FunctorOf (Product (->) (->)) f => (a -> b, x -> y) -> f (a, x) -> f (b, y)
bimap = map
-- and so on
As a side note, it has pretty great C interop, so you should be able to use C libraries or your own C code, for missing functionality. Documentation on this feature is unfortunately lacking right now though.
- https://emscripten.org/docs/porting/setjmp-longjmp.html
- https://github.com/koka-lang/libmprompt/blob/main/src/mpromp...
See this paper for details, it gives a good high level overview before diving into the nitty gritty: https://www.microsoft.com/en-us/research/publication/general...