5 ms·

Effekt – A research language with effect handlers and lightweight polymorphism

77 points by atombender 5y ago

guerrilla 5y ago
The design of Effekt revolves around a different view of effects and effect types. Traditionally, effect types express which _side effects_ a computation might have. In Effekt, effect types express which _capabilities_ a computation requires from its context. This[1] sounds similar to some access control systems. Interesting. While this new point in the design space of effect systems impedes reasoning about the absence of effects, we demonstrate that it significantly simplifies the treatment of effect polymorphism and the related issues of effect parametricity and effect encapsulation. A useful definition for those not in the know: Effectful expressions are expressions that depend on or modify the context they are evaluated in Edit: Can someone tell me... Is it necessary to have a new type system or could this be done with dependent types? 1. http://ps.informatik.uni-tuebingen.de/publications/brachthaeuser20effekt/ http://ps.informatik.uni-tuebingen.de/publications/brachthae...
- mananaysiempre 5y ago
  You can do almost everything with dependent types, but dependent type systems expressive enough to be practical are usually heavy, permit almost no (guaranteed) inference and tend to require a total language (unless you toss out soundness, like TypeScript does with its non-dependent types). The hope is usually that a weaker system might relieve some of these problems; besides, studying the weakest type systems that can express whatever it is you want is good mathematics in any case. I’m absolutely hoping for a practical dependently typed language as well, but we still have a ways to go there.
- saityi 5y ago
  > Edit: Can someone tell me... Is it necessary to have a new type system or could this be done with dependent types? I played around with trying to implement an effect library (via the research) in dependently typed languages (Idris, Agda) and found type inference issues to be too much to work around. I found I was having to help the type checker along at every step -- explicit signatures on everything and, in Haskell terms, type/proof applications on function calls. On the other hand, I have found Koka -- until I started pushing the type system to its limits -- to require no hand-holding to figure out how to type its set of effects. I am curious if a dependently-typed wizard could figure out an encoding to make these issues go away, but it was beyond my capability.
i_don_t_know 5y ago
The example for the Yield effect [1] looks suspiciously like the condition system of Common Lisp and restarts. [1] https://effekt-lang.org/#intro-handlers https://effekt-lang.org/#intro-handlers
- mananaysiempre 5y ago
  Andrej Bauer’s Eff[1] circa 2012 explored the connections with exception systems and delimited continuations pretty thoroughly, IIRC, though I’m not yet sure how the present language relates to it. [1] https://www.eff-lang.org/ https://www.eff-lang.org/
- hencq 5y ago
  You can implement some version of that as long as you have dynamic scope. For simplicity let's just use pseudocode with globals: # By default Yield throws an exception global Yield = function(n) {throw n}; def example() = { var produce = true; var n = 0; while (produce) { produce = Yield(n) n = n + 1 } println("done") } # Temporarily set the global Yield to be a different function with(Yield = function(n) { println(n); return n < 3;}) { example(); } Where algebraic effects typically differ is that the handler receives a continuation. Potentially you could do more with that than just resume. You could for example store that continuation and build coroutines that way. That makes them essentially the same as delimited continuations. That's something that Common Lisp does not support. I'm not sure how that works in Effekt though. Since there seems to be a 'resume' keyword they might not be as powerful as delimited continuations.
- agumonkey 5y ago
  This has been mentionned twice (including you) in this month. Makes me very curious about both CL restarts (never used them for real) and AEff
  - Jtsummers 5y ago
    https://link.springer.com/book/10.1007/978-1-4842-6134-7 https://link.springer.com/book/10.1007/978-1-4842-6134-7 That's a pretty good book (admittedly I have not finished it yet, life got in the way) about CL's condition system. Worth a read if it's something that interests you. Also, I'm pretty sure that price dropped a lot from when I last looked. $10 for the print book isn't a bad price, and $7 for the ebook.
saityi 5y ago
How does this compare to other effect-oriented languages like Koka, Frank, and Eff? I've been doing some work with Koka lately, but I briefly looked into the other three (including Effekt) and it mostly came down to, 'Koka seems most active in development'[1] and 'Koka had the easiest to use documentation for me'[2], which are both kind of subjective ways of choosing between them rather than an objective comparison. [1] E.g. https://github.com/effekt-lang/effekt https://github.com/effekt-lang/effekt had its last commit back in June; https://github.com/frank-lang/frank https://github.com/frank-lang/frank last commit last year; but https://github.com/koka-lang/koka https://github.com/koka-lang/koka last update was Oct 15. Effekt seems semi-active, at least, compared to Frank. While stability is good, I wouldn't expect it in a language actively being used for research. [2] Comparing https://koka-lang.github.io/koka/doc/book.html https://koka-lang.github.io/koka/doc/book.html and https://effekt-lang.org/docs/ https://effekt-lang.org/docs/ and https://www.eff-lang.org/learn/ https://www.eff-lang.org/learn/
- CornCobs 5y ago
  Koka is very interesting I must say. It's really cool to see how far they managed to make a functional language look imperative superficially, while being entirely functional under the hood and managing semantics via effects. However, I believe they aren't really able to present a full imperative API to write programs in (or maybe they just haven't fully implemented the needed parts in the stdlib). For example IIRC, the use of mut variables (internal mutability within a function and implicitly handled effect) and the related explicit heap effect don't seem to be able to share functions? And while they seem to work with entire objects the functions for mutations within arrays seemed limited the last time I tried Koka out. And everything being exposed only through the API presented some things were not possible to work around. I believe I was unable to write functions that mutated an array in place. If anyone has had experience with Koka I would love to be proven wrong! That said my initial point still stands - I think its an amazingly cool language and clearly a lot of interesting ideas are in it for sure.
  - lakecresva 5y ago
    Their section on development tasks mentions fleshing out std and improving array/mutable reference programming, so I think it just hasn't been redone yet. It seems like they spent a lot of development time recently (with great success) working on foundational stuff like perceus/fbip and doing a major version bump, so std is pretty bare.
karmakaze 5y ago
This is an exciting design exploring a different combination of language features. From the Design Considerations page: > For this reason we purposefully leave out one otherwise very prominent feature: there are no first-class functions! > Instead, we treat all functions as second-class (Osvald et al.). While functions which (following Ruby jargon) we call blocks can take other blocks as arguments, they always have to be fully applied. I'm still trying to figure out the implications and limitations of this choice. There's no composition by returning a function but can still compose effects.

77 points by atombender 5y ago

The design of Effekt revolves around a different view of effects and effect types. Traditionally, effect types express which _side effects_ a computation might have. In Effekt, effect types express which _capabilities_ a computation requires from its context. This[1] sounds similar to some access control systems. Interesting. While this new point in the design space of effect systems impedes reasoning about the absence of effects, we demonstrate that it significantly simplifies the treatment of effect polymorphism and the related issues of effect parametricity and effect encapsulation. A useful definition for those not in the know: Effectful expressions are expressions that depend on or modify the context they are evaluated in Edit: Can someone tell me... Is it necessary to have a new type system or could this be done with dependent types? 1. http://ps.informatik.uni-tuebingen.de/publications/brachthaeuser20effekt/ http://ps.informatik.uni-tuebingen.de/publications/brachthae...

mananaysiempre 5y ago
You can do almost everything with dependent types, but dependent type systems expressive enough to be practical are usually heavy, permit almost no (guaranteed) inference and tend to require a total language (unless you toss out soundness, like TypeScript does with its non-dependent types). The hope is usually that a weaker system might relieve some of these problems; besides, studying the weakest type systems that can express whatever it is you want is good mathematics in any case. I’m absolutely hoping for a practical dependently typed language as well, but we still have a ways to go there.
saityi 5y ago
> Edit: Can someone tell me... Is it necessary to have a new type system or could this be done with dependent types? I played around with trying to implement an effect library (via the research) in dependently typed languages (Idris, Agda) and found type inference issues to be too much to work around. I found I was having to help the type checker along at every step -- explicit signatures on everything and, in Haskell terms, type/proof applications on function calls. On the other hand, I have found Koka -- until I started pushing the type system to its limits -- to require no hand-holding to figure out how to type its set of effects. I am curious if a dependently-typed wizard could figure out an encoding to make these issues go away, but it was beyond my capability.

i_don_t_know 5y ago

The example for the Yield effect [1] looks suspiciously like the condition system of Common Lisp and restarts. [1] https://effekt-lang.org/#intro-handlers https://effekt-lang.org/#intro-handlers

mananaysiempre 5y ago
Andrej Bauer’s Eff[1] circa 2012 explored the connections with exception systems and delimited continuations pretty thoroughly, IIRC, though I’m not yet sure how the present language relates to it. [1] https://www.eff-lang.org/ https://www.eff-lang.org/
hencq 5y ago
You can implement some version of that as long as you have dynamic scope. For simplicity let's just use pseudocode with globals: # By default Yield throws an exception global Yield = function(n) {throw n}; def example() = { var produce = true; var n = 0; while (produce) { produce = Yield(n) n = n + 1 } println("done") } # Temporarily set the global Yield to be a different function with(Yield = function(n) { println(n); return n < 3;}) { example(); } Where algebraic effects typically differ is that the handler receives a continuation. Potentially you could do more with that than just resume. You could for example store that continuation and build coroutines that way. That makes them essentially the same as delimited continuations. That's something that Common Lisp does not support. I'm not sure how that works in Effekt though. Since there seems to be a 'resume' keyword they might not be as powerful as delimited continuations.
agumonkey 5y ago
This has been mentionned twice (including you) in this month. Makes me very curious about both CL restarts (never used them for real) and AEff
- Jtsummers 5y ago
  https://link.springer.com/book/10.1007/978-1-4842-6134-7 https://link.springer.com/book/10.1007/978-1-4842-6134-7 That's a pretty good book (admittedly I have not finished it yet, life got in the way) about CL's condition system. Worth a read if it's something that interests you. Also, I'm pretty sure that price dropped a lot from when I last looked. $10 for the print book isn't a bad price, and $7 for the ebook.

saityi 5y ago

How does this compare to other effect-oriented languages like Koka, Frank, and Eff? I've been doing some work with Koka lately, but I briefly looked into the other three (including Effekt) and it mostly came down to, 'Koka seems most active in development'[1] and 'Koka had the easiest to use documentation for me'[2], which are both kind of subjective ways of choosing between them rather than an objective comparison. [1] E.g. https://github.com/effekt-lang/effekt https://github.com/effekt-lang/effekt had its last commit back in June; https://github.com/frank-lang/frank https://github.com/frank-lang/frank last commit last year; but https://github.com/koka-lang/koka https://github.com/koka-lang/koka last update was Oct 15. Effekt seems semi-active, at least, compared to Frank. While stability is good, I wouldn't expect it in a language actively being used for research. [2] Comparing https://koka-lang.github.io/koka/doc/book.html https://koka-lang.github.io/koka/doc/book.html and https://effekt-lang.org/docs/ https://effekt-lang.org/docs/ and https://www.eff-lang.org/learn/ https://www.eff-lang.org/learn/

CornCobs 5y ago
Koka is very interesting I must say. It's really cool to see how far they managed to make a functional language look imperative superficially, while being entirely functional under the hood and managing semantics via effects. However, I believe they aren't really able to present a full imperative API to write programs in (or maybe they just haven't fully implemented the needed parts in the stdlib). For example IIRC, the use of mut variables (internal mutability within a function and implicitly handled effect) and the related explicit heap effect don't seem to be able to share functions? And while they seem to work with entire objects the functions for mutations within arrays seemed limited the last time I tried Koka out. And everything being exposed only through the API presented some things were not possible to work around. I believe I was unable to write functions that mutated an array in place. If anyone has had experience with Koka I would love to be proven wrong! That said my initial point still stands - I think its an amazingly cool language and clearly a lot of interesting ideas are in it for sure.
- lakecresva 5y ago
  Their section on development tasks mentions fleshing out std and improving array/mutable reference programming, so I think it just hasn't been redone yet. It seems like they spent a lot of development time recently (with great success) working on foundational stuff like perceus/fbip and doing a major version bump, so std is pretty bare.

karmakaze 5y ago

This is an exciting design exploring a different combination of language features. From the Design Considerations page: > For this reason we purposefully leave out one otherwise very prominent feature: there are no first-class functions! > Instead, we treat all functions as second-class (Osvald et al.). While functions which (following Ruby jargon) we call blocks can take other blocks as arguments, they always have to be fully applied. I'm still trying to figure out the implications and limitations of this choice. There's no composition by returning a function but can still compose effects.