capturing {io} and promising invariants

[marvinborner]

Hi everyone! I wonder if we can revisit the discussion about which functions/builtins capture io. Specifically, I remember discussing whether panic should capture io or not.

I find it very annoying that it does. For example, most map and set functions capture io because they sometimes panic when invariants are broken. For this reason, maps/sets can not be defined at the top-level, which can be useful sometimes.

In contrast, holes <> do not capture io, though they exhibit similar behavior at runtime. This is a bit inconsistent, no? To me, this just leads me to use <> instead of panic because I don't want to capture io everywhere.

If we want to maintain io capturing for panic (and for holes?), we need a different solution for promising invariants. In Effekt code we often have cases where it is 100% clear that a certain branch will not be executed. For example:

// map.effekt
def doubleL[A, B](k1: A, v1: B, t1: Tree[A, B], m: Tree[A, B]): Tree[A, B] = {
  m match {
    case Bin(_, k2, v2, Bin(_, k3, v3, t2, t3), t4) =>
      bin(k3, v3, bin(k1, v1, t1, t2), bin(k2, v2, t3, t4))
    case _ => panic("impossible: doubleL: Tip")
  }
}

Should we track everything via effects in this case, do we have other ways of managing invariants, or is panicking a good solution, even if {io} gets captured?

[jiribenes]

Thanks for this post!
IIRC we currently have panic with a io capture since it semantically requires an IO capability at runtime to print its message -- not remembering this at runtime would cause us to sometimes elide the panic completely, which is undesirable, as it goes against the promise that the panic, well, panics.

[marvinborner]

I see, I somehow assumed that panic was handled internally (like error in Haskell), requiring io for an externally defined panic makes sense.

[jiribenes]

For this specific case, I think you could figure out a way to inline doubleL and similar functions since they only get called after we've verified the invariant a level above. The panic is there because it was very helpful while developing the map :)

[jiribenes]

If my memory serves me well, we considered having panic be a separate capture, but then we'd have to specialize which captures can be top-level and which cannot.

[jiribenes]

RE Haskell: does it consider error to be pure (edit: internally in the compiler)? I'm asking since for us, not having a capture is the defn of purity, esp. for opts.

[marvinborner]

I don't think it's handled as something impure in any internal state of the compiler. It's just a pure bottom value. Not sure how its precise semantics regarding laziness are.

Anyway, what do you think about enforcing (ie. aiming for) an invariant that all non-extern/internal toplevel definitions in the standard library must have empty captures?

[b-studios]

Anyway, what do you think about enforcing (ie. aiming for) an invariant that all non-extern/internal toplevel definitions in the standard library must have empty captures?

I don't see how this is possible if they themselves use extern toplevel definitions?

We could have panic return a pure bottom value. But this could lead to surprising behavior with optimizations, such as in:

def foo() = {
  panic("abort")
  println("still here")
}

where the optimizer might decide to remove panic since its result is unused (there is no data dependency).

[b-studios]

One could also have a rather ad-hoc solution of adding a relevant (made up name) capture with the weird rule that

{relevant} <: {}

that is, we track it and use it in the optimizer, but can forget it if we don't need it. But I don't feel very confident about this. It is super ad-hoc and doesn't fit our theory.