RFCs
RFCs copied to clipboard
nim-lang
"Effect system" isn't actually an effect system.
"Effect system" is an already defined technical term; which Nim's doesn't match the requirements. A more accurate name would be "effect tracking".
I believe they are referring to Nim not having runtime effect handling, barring exception handling. Don't know what else is required in an effect system that could be missing.
There are many authoritative sources that show what I'm talking about: https://dl.acm.org/doi/pdf/10.1145/319838.319848 https://arxiv.org/pdf/1306.6316.pdf
A simpler way for me to say it though, is that effect systems are to effects as type systems are to types. In Nim, you do have a working type system and built-in types from what I've seen (built-in functions have types, as well as most built-ins); but that isn't the case for effects in Nim, let alone effect systems. What you've made is more of an effect tracking system in the sense that it's really just mentioning effects that some functions would cause at best. While effect systems involve having built-in effects to most functions that you'd want to have effects, and also involve ways to handle those effects in most effect systems. For an example, monad transformer effect stacks use monad transformers to "handle" functions that are meant to cause side effects; algebraic or extensible effect systems have effect handlers to handle functions that are meant to cause side-effects. The point is that, effect systems are essentially ways to handle ("execute") and track effects; meanwhile in Nim, the closest notion to an effect is merely a phantom type attached to a function. Your effects aren't being executed or created or handled by your "effect system", instead, your "effect system" is merely tracking the possible effects that could occur while running a function. That's why your "effect system" is really closer to an "effect tracking" system.
Well these sources either don't define "effect system" or define it in such a way that it is not in conflict with Nim's effect system:
An effect system supplements a traditional type system for a programming language with information about which computational effects may, will, or will not happen when a piece of code is executed.
The point is that, effect systems are essentially ways to handle ("execute") and track effects; meanwhile in Nim, the closest notion to an effect is merely a phantom type attached to a function. Your effects aren't being executed or created or handled by your "effect system", instead, your "effect system" is merely tracking the possible effects that could occur while running a function. That's why your "effect system" is really closer to an "effect tracking" system.
Nim allows you to handle an exception effect by try except and tag effects can be casted away. It's probably uglier than you would like (it's certainly uglier than I would like) but an ugly effect system is still an effect system.
Well these sources either don't define "effect system" or define it in such a way that it is not in conflict with Nim's effect system:
The former paper was to show the origin of effects, the latter one was to show an application of an effect system. Nevertheless, they do define it; it's just by leaning on the mathematics and code rather than sentences. For an example, the paper you took that quote from cites https://dl.acm.org/doi/pdf/10.1145/73560.73564 for effect systems, which also defines effects and effect systems in a more mathematical way. The point of me linking them was to show that effect systems are more complex than you think.
Nim allows you to handle an exception effect by
try exceptand tag effects can be casted away. It's probably uglier than you would like (it's certainly uglier than I would like) but an ugly effect system is still an effect system.
Exception handling is not effect handling. For an example, what you have in Nim is really closer to checked exceptions in Java; and checked exceptions can barely be considered close to a subset of an effect system.
"Tag effects can be casted away" is an interesting idea, but as I said, it is nothing other than attaching phantom types to a function, less about handing effects, and more about manipulating things to maybe deem some functions marked with the same tag unusable. As I said, this really just sounds like effect tracking; rather than effect handling. In the papers I linked, they use effects to encode/handle the usage of memory allocation features, for an example. The stress is on the fact that effects are what allows these functions to work, and effect handlers are what execute ("handle") the effects. In comparison, Nim's system has no such thing. You can have functions that have tags as "effects", and arbitrarily manipulate them, to try to simulate this... but it's just not how effect systems work. I hate to reiterate, but this is closer to simply tracking the effects rather than being an entire effect system.
which also defines effects and effect systems in a more mathematical way.
I keep skimming the papers and I don't find a definition for what an effect system is, only definitions for concrete language specific effect systems. So how about you tell me the real definition and explain why Nim's isn't one.
I don't know what there is to be done about this. It might be misleading to say Nim has an "effect system" if people expect it to be on the level of Koka but Nim's documentation doesn't seem to say anything like "Nim has a full featured effect system" and I haven't even seen Nim be advertised mentioning effects at all.
From https://web.cs.ucla.edu/~todd/research/tldi09.pdf
"For example, Java’s type system for checked exceptions (Gosling et al. 2005) can be formulated as an effect system."
And Nim goes further than Java and offers .effectsOf and .forbids.
Well, I didn't expect this to not be expected that well. I will say that the difference I'm talking about - which could seem small to people who haven't used effect systems and studied them extensively - could seem like it isn't there to people who aren't familiar with the subject... I'll have to explain using a bit more detail.
I don't know what there is to be done about this. It might be misleading to say Nim has an "effect system" if people expect it to be on the level of Koka but Nim's documentation doesn't seem to say anything like "Nim has a full featured effect system" and I haven't even seen Nim be advertised mentioning effects at all.
I think my suggestion to rename is good. And yes, my issue with this is that it is misleading to people, not because of the expectation of a certain language's effect system, but because they expect at least an effect system.
"For example, Java’s type system for checked exceptions (Gosling et al. 2005) can be formulated as an effect system." Yes, the important part is "can be formulated as", to my knowledge it is missing a few things to be called an effect system as well.
To put it bluntly: you need both effects and effect handlers to have an effect system, and as I explained earlier, those do not really exist in Nim.
To point to the definitions in the literature, they all have a few things in common: The fact that effects are more integrated into each paper as a language feature, rather than simply being around tag manipulation. In every single one of these papers, effects are more than just tags you pass around and manipulate like tags, or effectsOf, or checked exceptions, etc.
To take a few definitions from these papers, and about how and why Nim doesn't fit it:
From https://arxiv.org/pdf/1306.6316.pdf
An effect system supplements a traditional type system for a programming language with information about which computational effects may, will, or will not happen when a piece of code is executed
For Nim's "effect system", this isn't the case because Nim's isn't really about side-effects. It could be marking something arbitrary that isn't exactly an effect like e.g. in the tag example. It could be used to communicate information about computational effects that could occur, but as I said earlier, in reality they aren't communicating effects per se. In that same paper, in the "Effects and Types" section, it shows in the paper what an "effect" really is: A side-effectful operation in a function that's "handled" by an effect handler, to turn that function into a pure one.
This isn't the only case either, you see this theme in every paper here.
From https://web.cs.ucla.edu/~todd/research/tldi09.pdf
Type-and-effect systems (or simply effect systems) (Gifford and Lu- cassen 1986) are an approach for augmenting static type systems to reason about and control a program’s computational effects
What I said above applies here as well, and also from https://dl.acm.org/doi/pdf/10.1145/319838.319848
Effect checking is similar to type checking, but it is used to guarantee side-effect invariants instead of value invariants
Every expression has an effect class; just as the type of an expression describes the value computed by the expression, the e f f e c t class of an expression describes how that value is computed
and the "Effect class" section.
The thing in common with all of these is that effects are implemented as... well, ways of handling side-effects. It isn't just implementing modifiable tags into functions. Effect systems include effect checking, expression effects, expression handling, and etc.
I'm not saying you should implement your effect system the exact same as these papers, I'm just saying that it's misleading to call what you have an effect system because it doesn't do what effect systems are expected to do (work wit effects), and it's way more.. uh, minimalistic? than what you'd have in an actual effect system. I hope this clears things up.
Unfortunately I'm still too stupid to understand your points.
The fact that effects are more integrated into each paper as a language feature, rather than simply being around tag manipulation. In every single one of these papers, effects are more than just tags you pass around and manipulate like tags, or effectsOf, or checked exceptions, etc.
That could also mean that they failed to generalize the concept to be an extensible mechanism which is what Nim provides.
In that same paper, in the "Effects and Types" section, it shows in the paper what an "effect" really is: A side-effectful operation in a function that's "handled" by an effect handler, to turn that function into a pure one.
For example, an IO effect is pretty much universally regarded as an effect or side effect. How can you "handle" these and ensure it can be used in a "pure" function? But even if you can, all that means that you can "consume" an effect, much like try except consumes the exception effect.
I'm not saying you should implement your effect system the exact same as these papers, I'm just saying that it's misleading to call what you have an effect system because it doesn't do what effect systems are expected to do (work wit effects), and it's way more.. uh, minimalistic? than what you'd have in an actual effect system. I hope this clears things up.
Not at all. I don't mind changing the terms and you're probably right about all of this but you need to reply at least one more time.
Please show me in Pseudo-Nim code an example of what a real effect system can do that Nim's cannot or one that is overly tedious to do with Nim's.
I didn't mean to insinuate that you're stupid if that's what you're getting out of my messages. Simply that there are many differences between what you implemented for Nim and what effect systems actually are.
That could also mean that they failed to generalize the concept to be an extensible mechanism which is what Nim provides.
Er, well... if you think so. Iif that was the case, your system would still be way more different than effect systems, since it "generalizes the concept to be an extensiblle mechanism". I will say that your conclusion is n't what I meant, I wasn't talking about extensibility, I was talking about the existence of effects in those effect system, and the technical absence of that in yours.
For example, an IO effect is pretty much universally regarded as an effect or side effect. How can you "handle" these and ensure it can be used in a "pure" function? But even if you can, all that means that you can "consume" an effect, much like try except consumes the exception effect.
This... is probably the most basic thing that you'd expect every effect system to do; which is "handle" IO effects in pure functions to cause side effects (this is already what you have in haskell and eff). I won't explain it here since there are many other sources that can explain this better than I could, and also because it's off-topic to the discussion. And that doesn't really only mean "consuming" effects. Maybe you mean as in effectfulFunc :: Eff [IO, NonDet], running an IO effect handler through that would result in effectfulFunc :: Eff [NonDet], but once again that isn't all that happens. Effect handlers go through functions and see where effectful functions are, then essentially executes the effect. The difference between that and try/catch, is that for effect handlers you actually have the concept of an effect; for try/catch it's just error handling, and steps a tiny bit closer to effect system (but not quite) when you add checked exceptions.
How about:
proc swallowIO(callback: proc () {.tags: IOEffect.}) {.tags: [].} =
{.cast(tags: []).}: callback()
And now please complete this sentence: "swallowIO is not an effect handler as the literature understands it, because ..."
Because it isn't handling the IO effect. It's just removing the "IOEffect" tag from the function it receives, if my Nim doesn't fail me. In the literature (and the implementations), handling the IO effect is much more complex than removing the IO type and then treating it like a normal function.
Well but you cannot undo an IO operation so what does a real effect system do differently? Feel free to change the example to some other effect that might make things clearer.
Just to add my 2 cents here: I think this is a mostly pointless discussion over trivial details. Before Go, I would have argued that the term "pointer" almost always meant an unmanaged pointer to memory, while a "reference" almost always meant a managed pointer to memory. And yet Go did (and continues to) calls its references "pointers" (to my everlasting annoyance).
My point here is that it honestly doesn't matter what terminology is used here, as long as it makes sense to the layman.
I disagree. There is a gigantic difference in how these things work. Effect systems are already properly defined and the user expectation is to have effects be handled... This system is wildly different, and wouldn't be considered an effect system by everyone who knows what an effect system is, and has worked with them. Nevertheless, since the details are trivial, the trivial change I proposed seems like a good solution still.
Of course, a layman wouldn't really even know about effect systems and would likely see them useless, let alone this distinction between your effect tracking system and effect systems.
what does a real effect system do differently? Feel free to change the example to some other effect that might make things clearer.
I will show a couple examples of effects.
First, the IO effect... is actually really a mixture of multiple effects, it's a mixture of the possibility of not terminating, raising exceptions, mutability, and non-determinism. In a language like Haskell, it is defined as a specialisation of the ST monad, which represenst mutability, and the way it is "handled" is by weaving state of the "RealWorld" between effectful computations. The way you handled the effect is by removing the tag from the function.
Secondly, you have the mutability effect I described, ST (State Transformer). It traps mutations inside it's context in a way that preserves purity.
I think the theme is clear here. These effects aren't simply a conditional test like "This function has the IO effect in it's type, so I will allow this function to use print,", it's more like "This function has the IO effect in it's type, so I will run the IO effect handler through it to execute that effect". As you can see here, there's a very big dependence in effect systems on effect handlers, as it's arguable that you can't even really have effects without effect handlers. And to go even further, effect systems allow to write your own handler, which as I've already said isn't simply removing a tag from a function, but it's a generic abstraction that makes implementing things like asynchronous I/O easier as a user library rather than a language patch.
But Haskell does not have an effect system, only a type system. The point of an effects system is its orthogonality with the type system, an expression x has the type t and the effect eff, it can be modelled as a tuple (t, eff). What Haskell instead does is to map it as eff[t] which does not compose as eff1[eff2[t]] is not the same as eff2[eff1[t]] but for an effect system these should be identical. It's not much of a problem since you can patch over this problem with more monads but it means Haskell is a bad example for a "real effect system" since it has none.
This is not me making shit up, see for example: https://tomasp.net/academic/papers/haskell-effects/haskell-effects.pdf
"The first step in using lists to represent sets is to make the ordering irrelevant by (perhaps ironically) fixing an arbitrary ordering on elements of the set and normalising by sorting. We use bubble sort here as it is straightforward to implement at the type level."
Haskell does have an effect system. A very basic one, that is, using monad transformers (mtl, transformers, which are default libraries). Haskell's effect system, while it technically doesn't have the notion of effect handlers, it does actually have some notion of effects. Don't take my word for it, you can see the literature which says (well, the ones I previously linked only imply) that Haskell's monad transformer system is an effect system.
But it doesn't quite matter, even if Haskell specifically wouldn't have had an effect system in an alternative universe, my previous post wouldn't be incorrect either, only that specific example that mentions Haskell wouldn't be a fair comparison. The conclusion would still be the same.
I studied Koka a bit fwiw in order to finally understand what an effect handler actually is. And you're right, Nim doesn't have these. I don't agree these are required for an effect system but nevertheless naming the system "effect tracking" instead is fine.
Thank you very much for listening, despite my explanation! I'm sometimes known to be confusing but I don't really know of a better way to explain it.
Bikeshedding-ish, but everything that does something in a programmatic systematic way is by definition a "system".
Sure. You can name it "effect tracking system" if you want. My issue isn't with the word "system", my issue was with the usage of the term "effect system" which is an already established term that means something very different from what Nim has implemented.
I think CPS conforms with @MonAaraj expectations to an Effect System, but is named to resemble how it does, not what it does.
See also #295
Er, kind of. CPS has a lot of possibilities and it can be used to implement a lot of things. Effect systems are implemented using delimited contiunations, but CPS is.. uh, well, CPS. Calling it an effect system would be a misnomer because it isn't what that concept is, it's very different from that; it's just a style of programming that's kind of different from normal programming. But this is the first time I've heard about CPS for Nim, and that sounds very interesting.
Unless you mean your library rather than the CPS concept... which now that I think about it, I think that's what you meant. And it is a restricted effect system that's specialised for continuations, very nice! Well, if my Nim doesn't fail me, that is.