parametric effects: `proc fn(a: proc()) {.raises: [a].}`

timotheecour commented 3 years ago

proposal

track effects through params via symbol references:

proc fn1(a: proc(), b: proc()) # inferred as {.raises: Any.}
proc fn2(a: proc(), b: proc()) {.raises: [].} # raises nothing
proc fn3(a: proc(), b: proc()) {.raises: [a].} # raises whatever param `a` raises, ie raises(a)
proc fn4(a: proc(), b: proc()) {.raises: [a, b, ValueError].} # raises raises(a) + raises(b) + ValueError
proc fn5(a: proc(), b: proc()) = # inferred as {.raises(a).}
a()

in the manual https://nim-lang.org/docs/manual.html#effect-system-exception-tracking, remove distinction between direct and indirect call, it's not what's relevant

benefits

by default, we rely on type effect inference and most code won't have to deal with adding raises annotations
code that wants to annotate explict effects can do so, using explicit raise pragma

this allows being more precise about effect propagation, and would automatically distinguish between these via inference:

proc fn1(a: proc()): auto = a # inferred as {.raises: [].}
proc fn2(a: proc()): auto = a() # inferred as {.raises: [a].}
proc fn3(a: proc()): auto =  # inferred as {.raises: [a, ValueError].}
if a(): raise newException(ValueError, "foo")

this doesn't break genericity of things like sort and cmp, unlike other proposals (eg see https://github.com/nim-lang/RFCs/issues/404#issuecomment-890099626)
```
proc sorted*(a: seq[T], cmp: proc(a, b: T): int): seq[T] = ...
# infered as: {.raises: [cmp].} since cmp is called
```

proc main1(): auto = # infered as {.raises: [].} proc cmp(a,b): int = b-a # infered as {.raises: [].} sorted([1,2])

proc main2(): auto = # infered as {.raises: [ValueError].} because of raises: [cmp] proc cmp2(a, b: string): int = cmp(a.parseInt, b.parseInt) # can raise ValueError sorted(@["12", "3", "01"], cmp2)


* the analysis stays local: once a proc is semchecked, its effects are summarized by its infered raises list (which can include symbols)

* doesn't have the drawbacks of `effectsDelayed` (https://github.com/nim-lang/Nim/pull/18610) which is less flexible, less expressive and requires lots of user code annotations

## note 1
https://github.com/nim-lang/Nim/pull/14976 implements a similar thing, but in the case of raises this is actually a simpler analysis, more local (doesn't require interprocedural analysis, all info is summarized in the raises annotation).

## note 2
this is analog to how purity works in D, eg: https://forum.dlang.org/thread/blwlivyzhgwophxvhuye@forum.dlang.org

> D's working definition of a pure function is "effect only depends on parameters". Mutating parameters does fit the definition.
> This is less tight than other languages' definition, but we believe it's a sweet spot between reaping the modularity benefits of purity, and benefiting of the advantages of mutation.

and related articles, eg: https://klickverbot.at/blog/2012/05/purity-in-d/
> ›Weak‹ Purity Allows for Stronger Guarantees

## links
* originally proposed in https://github.com/nim-lang/RFCs/issues/403#issuecomment-890162087 and supersedes https://github.com/nim-lang/RFCs/issues/403
* would supersede https://github.com/nim-lang/Nim/pull/18610
* https://github.com/nim-lang/Nim/issues/9188

Araq commented 3 years ago

This solves the problem for .raises but not for .sideEffect. We need something more general like:


proc sort(p: proc()) {.raises: [], noSideEffect, effectsOf: p.}

The effectsOf describes additional, conditional effects. p must be a proc type parameter. This is exactly what Nim v1.0 does, except implicitly. The implicitness caused problem https://github.com/nim-lang/Nim/issues/18376

timotheecour commented 3 years ago

The effectsOf describes additional, conditional effects

raises is a bit special because try/except can undo some effects from parameters, unlike tags and nosideeffects (and possibly other effects).

namely, effectsOf doesn't work with the concern from https://github.com/nim-lang/RFCs/issues/403#issuecomment-889743996

it doesn't help me understand if bar1 handles errors that a raised or not

proc f1(p: proc()) {.raises: [], noSideEffect, effectsOf: p.} =
  p()
proc f2(p: proc()) {.raises: [], noSideEffect, effectsOf: p.} =
  try: p()
  except: discard
proc f3(p: proc()) {.raises: [], noSideEffect, effectsOf: p.} =
  try: p()
  except OSError: discard

tags (ReadEnvEffect etc) and sideeffects are indeed parametric on p, but effectsOf doesn't capture the fact that f2 and f3 catch all/some of the exceptions and that the set of things that f1, f2, f3 can raise is different

`calls: [p]`

that said, aside raises, a useful annotation (most of the time automatically inferred) can be to annotate which params are called (this can be inferred and specialized on each instantiation [1]):

proc sort[Fun](a, b: proc(), b, c: Fun) {.calls: [a, c].} # will call a and c
proc sort[Fun](a, b: proc(), b, c: Fun) {.calls: [a, c].} =
  a()
  c()

this captures side effects (and tags) through params, which addresses your concern:

This solves the problem for .raises but not for .sideEffect

examples

in general, APIs shouldn't write any annotations and rely on inference; but here examples with annotations:

proc f(a, b, c: proc()) {.noSideEffects, raises: [OsError, a], calls: [a, b].}
  # side effects depend on a, b
  a()
  try: b() except: discard # b called (hence sideeffect depends on it) but its raises effects are cancelled
  let c2 = c # c not called

note

the need for annotation will drastically reduce when https://github.com/nim-lang/RFCs/issues/416 is implemented (lazy semchecking) since fwd declarations won't be needed anymore.

[1]

refs https://discord.com/channels/371759389889003530/768367394547957761/882537080788484136 see examples in that linked discussion:

proc f1(a: auto): auto =
  when a is int: enforce(a>0) # raises: [a] or [] depending on the instantiation
  a

proc f2[Fun](a: proc(), b: static int) =
  when b == 1: a() # calls[a] or [] depending on the instantiation

Araq commented 3 years ago

namely, effectsOf doesn't work with the concern from #403 (comment)

It's unclear if that concern is enough of a justification to introduce more than a single effectsOf annotation. We can see later if in practice an even more elaborate mechanism is required, for now I'm going with a single effectsOf.

timotheecour commented 3 years ago

without loss of generality you can start with a single pragma (effectsOf or calls), and later if necessary raises can be extended to support the above mentioned use case of try/except negating some of the inferred raises effects

https://github.com/nim-lang/RFCs/issues/419 would be nice to have before further modifications to effect system

Araq commented 3 years ago

This has been implemented.

nim-lang / RFCs