"Effect system" isn't actually an effect system.

[subterfugue]

"Effect system" is an already defined technical term; which Nim's doesn't match the requirements. A more accurate name would be "effect tracking".

[Araq]

Where can I find this definition?

[metagn]

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.

[subterfugue]

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.

[Araq]

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.

[subterfugue]

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 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.

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.

[Araq]

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.

[metagn]

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.

[Araq]

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.

[subterfugue]

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.

[Araq]

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.

[subterfugue]

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.

[Araq]

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 ..."

[subterfugue]

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.

[Araq]

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.