What is mask behind?

[osa1]

I understand making, but there seems to be a variant of it with syntax mask behind. It's used in the standard library, but I can't find any documentation of it (either in the book or koka-community docs). What is it, why and how do I use it?

[zephyrtronium]

mask behind is described in the "advanced" sidenote in https://koka-lang.github.io/koka/doc/book.html#sec-overriding-handlers. The description of it is a bit hard for me to follow, but that's probably because I haven't yet actually tried to use it.

[osa1]

Thanks. I also can't follow that section. I think it should give concrete examples: show what happens if you place mask in the places mentioned in the section, with full runnable code + output when you run them, and how to get the intended output with mask behind.

[TimWhiting]

Hmm, I feel like it is a pretty good explanation, but let me try to explain it the same, with examples:

So let's consider multiple of the same effect on the stack. With simple masking we can skip a handler.

effect exn_
   fun throw_(e: string)

fun main()
  with handler
    fun throw_(e: string)
      println("Error in outer")
  with handler
    fun throw_(e2: string)
      println("Error in inner")
      throw_("from inner to outer")
  ...
  throw_("throw to inner")
  mask<exn_>
     throw_("throw to outer")

However let's say we want to override the outer handler (hide it from all code below the inner handler) - all throws must go through the inner to get to the outer. (In other words we want the masked throw to fail - disallowing skipping a handler).
We could try to insert a mask to mask the outer handler in two places - above the inner handler, or below the inner handler.

// Above looks like this

  with handler
    fun throw_(e: string)
      println("Error in outer")
  with mask<exn_> 
  with handler
    fun throw_(e2: string)
      println("Error in inner")
      throw_("from inner to outer") // OH NO! we've masked the effect, and cannot delegate
  ...
  throw_("throw to inner")
  // Good error here, there aren't enough exns in the stack (we have sucessfully masked the exn)
  mask<exn_> 
     throw_("throw to outer")

// Below looks like this

  with handler
    fun throw_(e: string)
      println("Error in outer")
  with handler
    fun throw_(e2: string)
      println("Error in inner")
      throw_("from inner to outer") // Good we can still delegate to the outer handler from the inner handler's clauses
  with mask<exn_> 
  ...
  throw_("throw to inner") // OH NO! we've masked our inner effect, the innermost one is now the outer one
  // Good error here, there aren't enough exns in the stack (However, although we masked the wrong one)
  mask<exn_> 
     throw_("throw to outer")

// With mask behind

  with handler
    fun throw_(e: string)
      println("Error in outer")
  with handler
    fun throw_(e2: string)
      println("Error in inner")
      throw_("from inner to outer") // Good we can still delegate to the outer handler from the inner handler's clauses
  with mask behind<exn_> // Don't mask the innermost, but mask the next one
  ...
  throw_("throw to inner") // Good, we see the inner handler but not the outer
  mask<exn_> // This masks the inner handler one now
    // Good error here, there aren't enough exns in the stack, since we masked the inner, after masking the next one out.
     throw_("throw to outer")

[TimWhiting]

See #635 for maybe an alternate desugaring of overriding that might mean mask behind is unnecessary.