Distinct occurrences of the same effect per function?

[dan-zheng]

Koka has effect types in function types. Example:

effect state<a> {
  fun get() : a
  fun set( x : a ) : ()
}

fun sumdown( sum : int = 0 ) : <state<int>,div> int {
  val i = get()
  if (i <= 0) then sum else {
    set( i - 1 )
    sumdown( sum + i )
  }
}

Can Koka support distinct state<int> effects in the same function type, each representing a separate heap reference? Use cases include representing programs operating on multiple mutable references at once: get<state1>() and get<state2>(). Without loss of generality, does this feature extend to other effect types too?

The theory behind effect handlers (multi-prompt delimited continuations) seems to allow this flexibility? I wonder if that is indeed supportable, and if it is implemented in Koka.

[xnning]

Koka supports multiple instances of the same effect in two ways: masking, and named handlers (WIP).

Masking allows you to skip the innermost handler for that corresponding effect, so that the operation is handled by the second to innermost handler, e.g.,

effect read<a> {
  fun get() : a
}

fun sum() : <read<int>,read<int>> int {
  val i = get()
  val j = mask<read<int>> {get()}
  i + j
}

fun main() {
  with handler {
    fun get() { 1 }
  }
  with handler {
    fun get() { 2 }
  }
  sum() // 3
}

A more concise way is to use named handlers, where handlers are given named so that operations can be performed directly on a specific handler. There are some samples regarding named handlers.

named effect read<a> {
  fun get() : a
}

fun main() {
  with i = named handler {
    fun get() { 1 }
  }
  with j = named handler {
    fun get() { 2 }
  }
  i.get() + j.get() // 3
}

[daanx]

Hi Dan, good to see you here :-) Just to add to Ningning's excellent answer, named handlers is still active research (and mask is a bit cumbersome). However, I feel that in practice we should not use either for the state example you gave: I think when possible it is best to create specific effect instances for the actual domain specific use case. For example, when I write a type inferencer, I may need multiple states, like a unique counter to generate unique names, and a current substitution. Now, instead of using two generic state effects, it would be better to create a new effect type for the domain:

effect infer {
   fun unique() : int 
   fun add-subst( x : typevar, t : monotype ) : ()
   fun subst( t : monotype ) : monotype 
}

for example.

The intended use case for named handlers is when you need dynamic "resources", e.g. say a number of files or network connections. Although, even in that case we may get away with a single effect handler that hands out "handles" to access individual items.

[dan-zheng]

Thanks Ningning and Daan, this is quite neat! I'll close since my question has been answered.

[dan-zheng]

Masking allows you to skip the innermost handler for that corresponding effect, so that the operation is handled by the second to innermost handler, e.g.,

Would it be fair to compare "effect masking" tolift in monad transformer stacks? Are there any differences, or is it an exact analogy?

A more concise way is to use named handlers, where handlers are given named so that operations can be performed directly on a specific handler.

Nice. Named handlers seem more flexible and easier-to-use, it reminds me of named typeclass instances.

[dan-zheng]

However, I feel that in practice we should not use either for the state example you gave: I think when possible it is best to create specific effect instances for the actual domain specific use case.

That's an astute high-level design observation!

I guess in a language like Koka with first-class effects, it makes sense to make one-off effects for a specific purpose (for clarity and ease of understanding). In languages with ADTs (first-class datatypes), this is analogous to the design principle of creating custom ADTs instead of using existing, less-informative ones like Bool.

[daanx]

mask is indeed like lift in a monad transformer stack -- not exactly the same thing, but used for the same situation. And I agree with defining custom ADT's , here is an interesting post by Bob Harper on this: https://existentialtype.wordpress.com/?s=boolean

[daanx]

I dislike losing these interesting issues with nice responses by closing them... I think I will add discussions to the koka github so it is easier to discuss things like this (as with the partially applied type aliases topic)

[dan-zheng]

And I agree with defining custom ADT's , here is an interesting post by Bob Harper on this: https://existentialtype.wordpress.com/?s=boolean

Thanks for sharing! In addition to "boolean blindness", I think there's also the unfortunate consequence of "boolean information narrowing": we discard a lot of information when we narrow an information-rich ADT to data Bool = True | False. I recall reading about that in a different blog post, but I unfortunately couldn't find it so I cannot cite it.