10 ms·
Koka: Strongly typed functional-style language with effect types and handlers
- throw156754228 3y agoMicrosoft really love those angle brackets don't they?
- pharmakom 3y agoWhat are the practical advantages of Koka over say “IO a” or “Async<‘t>” in other languages?
- jitl 3y agoMonads need to wrap each other, effects are more composable
- TheMatten 3y ago> Monads need to wrap each other, effects are more composable 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.
- spicebox 3y agoBeing able to change the ordering of effects on the fly is a benefit of algebraic-effect systems. As you mentioned `State<S, Result<E, T>>` and `Result<E, State<S, T>>`have very different effects. Algebraic-effects let you switch between the two behaviors when you run the effects, whereas with monad transformers you have to refactor all your code to use `State<S, Result<E, T>>` instead of `Result<E, State<S, T>>` or vice-versa
- shirogane86x 3y agoYou can recover the ability to reorder effects by using MTL-style type classes, so you could write that as M<T> where M: MonadState<S> + MonadError<E>, in rust-ish syntax. But that makes the number of trait/typeclass implementation for each transformer explode (given a trait and a type for each transformer, it's O(N^2)), whereas algebraic effect systems don't really have that issue. I also have a hunch that algebraic effects(or, well, delimited continuations in general) are probably easier to optimize than monad transformers, too.
- spicebox 3y agoMonads don’t compose, effects do. ‘IO a’ works great until until you need to add another effect, for example ‘Maybe’. Then you need to bring in monad transformers and create your own monad combining the two, then rewrite all your code to lift the effects from one monad to the other. And you have to do this every time you want to add a new effect.
- ChadNauseam 3y agoNot to mention you need monadic and nonmonadic versions of every higher order function (or so it feels like) - map / mapM, fold / foldM, etc. 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)
- nyssos 3y ago> Not to mention you need monadic and nonmonadic versions of every higher order function (or so it feels like) - map / mapM 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 but this would require somewhat better type-level programming support for the ergonomics to work out.
- grumpyprole 3y agoIt's much easier to adapt existing code. There's no need to rewrite code to use monadic binds.
- jitl 3y ago> Effect handlers let you define advanced control abstractions, like exceptions, async/await, iterators, parsers, ambient state, or probabilistic programs, as a user library in a typed and composable way. > 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.
- phoe-krk 3y agoAlso, as a Lisp programmer, I absolutely loved reading the section at https://koka-lang.github.io/koka/doc/book.html#sec-handlers https://koka-lang.github.io/koka/doc/book.html#sec-handlers - it's essentially like using the Common Lisp condition system, making me feel at home, except it's more generalized (e.g. masking individual condition handlers is not generally possible in CL) and also working in a strongly statically typed environment.
- nerdponx 3y agoAs far as I understand the PL theory involved, it's statically-typed delimited continuation, which I think is even more general than the CL condition system.
- kazinator 3y agoIn CL, you can control the visibility of restarts. In the restart-bind construct, there is a :test-function which serves as a predicate that determines whether the restart is visible. (Unfortunately, this function is referred to as a condition). 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.
- nerdponx 3y ago
- dang 3y agoRelated. Others? Koka: A fast functional programming language with algebraic effects - https://news.ycombinator.com/item?id=38421003 https://news.ycombinator.com/item?id=38421003 - Nov 2023 (2 comments) The Koka Programming Language - https://news.ycombinator.com/item?id=28335043 https://news.ycombinator.com/item?id=28335043 - Aug 2021 (2 comments) Koka: A Functional Language with Effects - https://news.ycombinator.com/item?id=27710267 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 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 https://news.ycombinator.com/item?id=14647415 - June 2017 (1 comment) Koka – A function-oriented programming language - https://news.ycombinator.com/item?id=10131071 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 https://news.ycombinator.com/item?id=4407415 - Aug 2012 (1 comment)
- nerdponx 3y agoNice to finally see this get some attention on the front page.
- anfelor 3y agoSome of the research behind Koka was discussed at: FP2: Fully In-Place Functional Programming [pdf] - https://news.ycombinator.com/item?id=36471591 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 https://news.ycombinator.com/item?id=25464354 - Dec 2020 (44 comments) Implementing Algebraic Effects in C - https://news.ycombinator.com/item?id=14887341 https://news.ycombinator.com/item?id=14887341 - July 2017 (21 comments)
- dang 3y agoNice. Thanks!
- satvikpendem 3y agoFor those who've used effectful languages, how much of a spaghetti code mess do they create, potentially? That's basically my only worry with effects that can be suspended and resumed at basically any point and any location in the codebase.
- naasking 3y agoPreemptive multitasking is an effect handler implemented by the operating system. There are very few instances where you have to worry about process switching by the OS, basically only when you have a handle to a resource outside of your process. 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.
- satvikpendem 3y agoI don't quite understand, let's say I have a bunch of effects in my code, all depending on one another. Will that make a mess? If so, how does one avoid that, or is that an inherent issue in algebraic effects systems?
- nerdponx 3y agoYou mean a situation where the effect handler for effect A invokes effect B? I wonder if the compiler is able to detect and prevent "circular" event invocations.
- nyssos 3y ago> I don't quite understand, let's say I have a bunch of effects in my code, all depending on one another. Will that make a mess? 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.
- 3y ago
- cranberryturkey 3y agodoes this support WASM?
- nateb2022 3y agoyes, use `--target=wasm`
- gpderetta 3y agoMy understanding is that wasm doesn't allow for stack switching yet. How does koka implements effects in wasm? Heap allocated stack frames?
- miclill 3y agoI think the _magic_ here is emscripten: - https://emscripten.org/docs/porting/setjmp-longjmp.html https://emscripten.org/docs/porting/setjmp-longjmp.html - https://github.com/koka-lang/libmprompt/blob/main/src/mprompt/gstack.c https://github.com/koka-lang/libmprompt/blob/main/src/mpromp...
- whitim 3y agoKoka currently uses the same approach that it does for compiling to C. It essentially does a very efficient low level monadic translation of a delimited control monad. So basically it all just ends up as a tiny bit of thread local state, and building up continuations on returns from functions if they are yielding. 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/generalized-evidence-passing-for-effect-handlers-or-efficient-compilation-of-effect-handlers-to-c/ https://www.microsoft.com/en-us/research/publication/general...
- scns 3y agoDot Selection looks neat, no pipeline operator needed. Enables extension functions a la Kotlin too.
- yawaramin 3y agoAlso known as Uniform Function Call Syntax (UFCS).
- solidsnack9000 3y agoSuch a thought provoking language. Docs are a good read, and reach a standard that few production languages come close to.
- whitim 3y agoAgreed, Koka has great documentation, although I will acknowledge that it is incomplete. The papers are suprisingly approachable with good user applicable examples and motivation before they get too deep into type theory etc. I recommend reading a few of the more recent ones, which have mind blowing implications. https://www.microsoft.com/en-us/research/publication/fiptree-tr/ https://www.microsoft.com/en-us/research/publication/fiptree... https://www.microsoft.com/en-us/research/publication/tail-recursion-modulo-context-an-equational-approach-2/ https://www.microsoft.com/en-us/research/publication/tail-re... https://www.microsoft.com/en-us/research/publication/fp2-fully-in-place-functional-programming/ https://www.microsoft.com/en-us/research/publication/fp2-ful...
- solidsnack9000 3y agoAmazing stuff -- thank you for sharing these papers. 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.
- codethief 3y agoDoes anyone here have any experience with Koka? I've been following the language from afar for a while but I have yet to read an account of what it's like to use it in practice.
- hamandcheese 3y agoIt is self-proclaimed as a "research Language" on the homepage, which has kept me away so far.
- Hugsun 3y agoI share this sentiment, although I have wondered if they're being overly conservative with this statement.
- whitim 3y agoI would say that research language is an appropriate description currently. For example it has very little standard library. Though I would say that it is well positioned to take off in the next year with several important improvements coming soon.
- xigoi 3y agoLast time I tried to use it (which was quite long ago), it barely had a print function, making it pretty much unusable.
- ReleaseCandidat 3y agoIt does have `print(ln)` for some time (when I have tried it for the first time) now.
- helix278 3y agoI've tried using it a bit. It works and it is fun to use, but there are quite a number of rough edges. I wouldn't use it in production yet, I don't think they are conservative there.
- djha-skin 3y ago> Koka tracks the (side) effects of every function in its type, where pure and effectful computations are distinguished. The precise effect typing gives Koka rock-solid semantics backed by well-studied category theory, which makes Koka particularly easy to reason about for both humans and compilers. 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.
- yawaramin 3y agoCategory theory is not the headline news here, it's safety without sacrificing performance by using a new technique to compile to binaries without a runtime or garbage collector, with potentially better deallocation performance than Rust, and functional-looking code like `array.map(func)` which performs as fast as a for-loop thanks to advanced analysis.
- djtango 3y agothanks for this, it wasn't immediately obvious to me why the headline example was traversing a list but doing that fast without GC is cool
- galaxyLogic 3y agoSo this means we have benefits of Rust but in a nicer, functional syntax?
- whitim 3y agoYes, essentially. Theoretically it could outperform Rust since it has aggressive local reuse of to-be-freed memory. Several papers have shown that it gets close to or outperforms C in some benchmarks. Whether this holds in practice is up for debate, but if you don't have to annotate lifetimes and don't have to manually manage memory, are you really going to care if you are 5% slower than C? There is a lot of performance optimizations still available for Koka to target as well. So far they've just taken the lowest hanging fruit (memory management).
- codeflo 3y agoInterestingly, this seems to be sponsored by Microsoft Research, which has also heavily supported the development of and research on Haskell. (Source: https://www.microsoft.com/en-us/research/project/koka/ https://www.microsoft.com/en-us/research/project/koka/)
- ed_blackburn 3y agoDid they not effectively acqui-hire or plain hire the pony lang team too?
- ReleaseCandidat 3y agoAnd Lean (which also uses Perceus RC) too: https://www.microsoft.com/en-us/research/project/lean/ https://www.microsoft.com/en-us/research/project/lean/
- mrobot 3y agoI was confused because the reference counting in the "Why Koka" part (section 2) of the book [1] seemed mismatched, so i looked it up in their reference counting TR [2]. It turns out it uses a seemingly novel approach to reference counting where any function you pass a reference to is responsible for decrementing and possibly freeing that reference. If you need to pass a reference to two functions you have to dup it once. 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 https://koka-lang.github.io/koka/doc/book.html [2] https://www.microsoft.com/en-us/research/publication/perceus-garbage-free-reference-counting-with-reuse/ https://www.microsoft.com/en-us/research/publication/perceus... (see section 2.2)
- bruce343434 3y agoWhat I don't like is that the effect handler is decoupled from the effect generator. 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.
- ReleaseCandidat 3y ago> In the code snippet, they define a "yield", and somehow this magically works 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 handler
- palemoonale 3y agoThe talk in office restrooms about using Koka gets a new twist.
- throw156754228 3y agoWhat is the equivalent of the Haskell StateT monad in Koka?
- throw156754228 3y agoI see now, they have mutable variables, within a lexical scope anyway.