Pondering Effects
22 points by icefox
22 points by icefox
I’m pretty sure the “effects on data” that you’re talking about is modelled by coeffects, which have a wonderful introductory tutorial at https://tomasp.net/coeffects/
Great reference, thanks!
...though unfortunately the fancy presentation detracts from the content, at least for me. Hard for me to pay much attention to the theory after I manage to crash their interpreter.
Zig is not that unique in you having to pass around something fairly "fundamental" in a way. Go is a higher-level language, but it requires explicitly plumbing a Context object for cancellation (and you need to check it manually). Go codebases where you pass the logger explicitly introduce more verbosity, sure, but because of the way, interface subtyping works, you could fold the Logger and Context into a single parameter that gets silently narrowed depending on what's needed.
A bigger problem with effects as I see it (and have covered in https://typesanitizer.com/blog/effects-convo.html) is that it becomes a breaking change to do a variety of useful things like adding assertions, instrumenting your code for coverage points for tests (e.g. what matklad has written about as "coverage marks") and so on, without punching a hole through the effect system.
Koka has support for functions that are effect-polymorphic: fun map( xs : list<a>, f : a -> e b ) : e list<b> means that map has the effects of f. Perhaps this could be used somewhat-silently for assertions and logging.
I do hope this works for resumptive effects too, since then one could do interactive debugging using this technique
I think there's a possible workaround for the assertion problem by taking the same approach as Rust with unsafe blocks. Unsafe functions are colored, but if you call an unsafe function in an unsafe block, you promise to the compiler that there will be no real unsafe behavior at runtime.
More generally, you could add a class of unsafe block that forgets effects. This would allow you to have assertions in non-panicking functions. However, the ramifications of those semantics could be disastrous if (e.g.) compiler optimizations get involved.
I experienced a similar problem and wrote a wonky article about it some time ago: https://claytonwramsey.com/blog/effect-polymorphism/ -- TL;DR: if you have polymorphic effects, you can at least handle things like dependency injection of effectful functions.
Well, I did end my sentence with "without punching a hole through the effect system." :D What you've done with the equivalent of an unsafe block is essentially that. Unsafe though is expected to uphold certain invariants which do not disable optimizations, but the equivalent for effects does not get the same benefit.
Yeah there's a difference between telling the compiler what effects something has, and telling the compiler to not care about the effects. An unsafe block says "I'm doing some stuff you can't analyze but I promise it will be fine". A similar case in an effect system might be marking a function as "cannot panic" even though it contains a panic call, because the panic call is in an unreachable code branch.
Yes! The Java checked exception problem! My hope is that effect polymorphism and inference can mostly cover it up; you write down the effects you care about, and the compiler doesn't bother much with the ones you don't care about until you say that they actually matter. This isn't a perfect solution, since "actually mattering" is a bit of a non-local property. It's the sort of thing where we'd have to try it out for real and see how it works.
This is an interesting idea. I'm currently sketching out ideas for my own effect-typed little language so I'm deep, deep in thought on what kinds of things make sense here.
We can annotate non-resumptive effects with typed effects. An effect that returns an unconstrained polymorphic type necessarily cannot be resumed, so that works (and on the compilation side we can detect that and avoid capturing a resumption).
The effect pollution problem is kind of fascinating. You can imagine there being "ambient" or "private" effects like assert and coverage marking. Depending on how the system is compiled/interpreted they could just be no-ops. Maybe you could even decide that locally by installing the proper handler.
But then do you want to be able to assert the non-existence of those effects in certain "really, truly pure" code?
This is quite some pondering! I wonder from what kind of perspective this was written, because I really like algebraic effects in OCaml and Unison, but I've only used handlers and almost never written one(well, technically there was also a F# effect library that popped up some years ago).
But I like them because they make reasoning about the flow of the program a lot easier, without too much type tetris, even without tools that help passing a big context around.
I find all the things mentioned here quite fascinating(even though hard to understand sometimes), but it's always funny to contrast my experience with algebraic effects(terrible marketing name btw) and then go back to write some badly behaved TypeScript code.
It's written from the perspective of someone who loves writing Rust 'cause it doesn't cover up much of the interesting stuff, and who has been rubbing shoulders with high-assurance software for almost a decade. :D It is, somewhat hilariously, not written from the perspective who has actually used algebraic effects in OCaml and Unison. So it's quite possible I'm missing plenty; I'm down in the dirt rummaging around in root systems and worm ecology, totally blind to the flowers. :D
Gardens are fun and there is a wealth of things to consider when tending to a garden.
I generally keep myself to languages that have ADTs and pattern matching, but I've been meaning to look more into Zig or Rust because they seem like a great into to low level programming.
Some gardens are bigger than they seem.