[HN Gopher] Effekt - A research language with effect handlers an...
___________________________________________________________________
Effekt - A research language with effect handlers and lightweight
polymorphism
Author : atombender
Score : 71 points
Date : 2021-11-19 10:50 UTC (12 hours ago)
(HTM) web link (effekt-lang.org)
(TXT) w3m dump (effekt-lang.org)
| karmakaze wrote:
| 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.
| saityi wrote:
| 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 had its last
| commit back in June; https://github.com/frank-lang/frank last
| commit last year; but 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 and
| https://effekt-lang.org/docs/ and https://www.eff-lang.org/learn/
| CornCobs wrote:
| 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 wrote:
| 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.
| saityi wrote:
| So I would say this echoes my experience with it so far -- it
| is definitely a work in progress! However, I tend to approach
| Koka as if it were Standard ML with an effect system (up to a
| point), so the lack of a full imperative API hasn't been felt
| too much. I am more missing ad-hoc polymorphism than
| imperative tooling.
|
| I am not sure I understand your comment about mut variables;
| my understanding is there are two types of mutable variables
| in Koka -- 'local' and 'ref'. 'local' is a locally mutable
| variable, and 'refs' are globally shareable. A 'ref' can be
| shared between functions, 'local' is just to give an
| imperative API using mutable variables. How 'local' works
| kind of confuses me so I tend to avoid it altogether in
| favour of local names (i.e. 'val' rather than 'var') and tail
| recursion (instead of loops with mutation). 'ref' seems quite
| usable to me and seems to reflect the SML usage of it.
|
| I have felt the pain of a lack of an array, but I ported over
| an Okasaki data structure which has served well for a random-
| update, sequential data structure. Their data structures in
| the stdlib just have comments that say 'TODO':
| https://github.com/koka-
| lang/koka/blob/master/lib/std/data/m... that I am hoping are
| open to pull requests.
| anfelor wrote:
| You might be interested in the FBIP versions of Okasakis
| datastructures in https://github.com/koka-
| lang/koka/tree/master/test/perf/sets Most of them only have
| 'insert' and 'lookup', but they are ~10% faster than
| Okasakis versions. For red-black trees in particular the
| fastest implementation is https://github.com/koka-
| lang/koka/blob/master/test/bench/kok...
| i_don_t_know wrote:
| 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
| agumonkey wrote:
| 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 wrote:
| 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.
| agumonkey wrote:
| I might actually buy one of these. Thanks.
| mananaysiempre wrote:
| 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/
| hencq wrote:
| 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.
| guerrilla wrote:
| 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/brachthae...
| mananaysiempre wrote:
| 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 wrote:
| > 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.
___________________________________________________________________
(page generated 2021-11-19 23:01 UTC)