Composable exception effect type?

[osa1]

Effects generalize exceptions, but I'm not sure how to make user code that throws exceptions compose.

Consider:

// Defined in standard library.
effect exn_<a>
  ctl throw_(exn: a): b // doesn't return
// End of standard library part

// Defined in third-party library
struct exception1
  value_: int

fun f1(): <exn_<exception1>>()
  ()
// End of third-party library

// Defined in another third-party library
struct exception2
  value_: string

fun f2(): <exn_<exception2>>()
  ()
// End of third-party library

// My application:
fun f3() // won't type check
  f1()
  f2()

fun main()
  ()

The standard library seems to work around this with an "open type":

koka/lib/std/core/exn.kk

Lines 35 to 42 in e285887

	pub open type exception-info
	ExnError // Generic error
	ExnAssert
	ExnTodo
	ExnRange
	ExnPattern( location : string, definition : string )
	ExnSystem( errno : int )
	ExnInternal( name : string )

I'm not sure what an open type is as I can't find any documentation on it, but regardless, it's clear that with this type a function with the standard library exn effect can throw anything value in this type, so the handlers also need to handle everything, which is also not ideal.

I think ideally, the type system should allow for:

• Calling functions that throw different types of exceptions, and reflecting this in the caller's type.
• Handling some of the exceptions and not the others, and reflecting this in the handler's type (i.e. remove handled exceptions from the exn<...here...>).
• Passing a function that throws less as a function that throws more. E.g. if a function throws exception1, it should be allowed to be passed as a function that throws exception1 and exception2. (e.g. as a callback)

At least the first two seems to be what row types do in the effect system, but they're not available in the user types as far as I can see?

Is this kind of thing possible right now? Are there any plans to support this use case?

[TimWhiting]

This is definitely possible right now. You just have to explicitly mask the first exception in the row to match types for the second one.

// My application:
fun f3(): <exn_<exception2>, exn_<exception1>> () 
  mask<exn_>{f1()}
  f2()

fun main()
  with handler 
    final ctl throw_(e: exception1)
      e.value_.show.println
  with handler 
    final ctl throw_(e: exception2)
      e.value_.show.println
  f3()

This is partially due to the fact that for polymorphic exceptions you cannot assume one ordering or the other. Should f1 use the first or second ?

// My application:
fun f3(f1, f2): <exn_<b>, exn_<a>> ()
  f1()
  f2()

Personally I believe that we could probably auto-insert masks for duplicate effect labels when they are fully concrete. But the inference would be more complicated, in addition to the fact that the ordering of handlers on the stack is made more explicit and less flexible.

I would suggest creating different effect types instead.

effect ctl type-error(info ...): a  // or a single object for info
effect ctl syntax-error(info ...): a  
effect ctl empty-collection(): a
effect ctl break<a>(a: a): b

This is in general more composable, at least the way Koka's effect inference works. There are other effect systems that use sets rather than rows.

As far as the builtin exception type you can extend it using:

extend type exception-info 
   ExnType 
   ExnBreak 

fun handle-typeerror(f)
  try(f) fn(err)
     match err
         ExnType -> xxx
         _ -> throw-exn(err)

Or something like that.

As a side note, I'd love for open types to group constructors as a row, and then let you add / remove / specify which constructors, but I don't think this completely solves this problem since the open type (exception-info) is embedded into the exception type.

[osa1]

Thanks for the answer.

This is partially due to the fact that for polymorphic exceptions you cannot assume one ordering or the other. Should f1 use the first or second ?

I think it would be acceptable in these cases to require the user to specify types, but I don't know if there are other issues.

I realize now that even without the need to explicitly mask, <exn_<a>, exn_<b>> does not really work as "checked exceptions" as you can't "catch all" and then rethrow (like in a finally block), each exn_ need to be separately handled.

As a side note, I'd love for open types to group constructors as a row, and then let you add / remove / specify which constructors,

Yeah, I think this is the way. I think ideally I would have exn_<[a, b]> (maybe with a better syntax) where [...] is a polymorphic variant.

but I don't think this completely solves this problem since the open type (exception-info) is embedded into the exception type.

Why is the exception types being embedded in another type a problem?

[TimWhiting]

My bad, but we would probably need to change exception to

struct exception<r>
   message: string
   info: exception-info<r>

Where r stands for this union type of constructors / i.e. row type.

[zephyrtronium]

As an aside, open types are described under Extensible Types at https://koka-community.github.io/koka-docs/koka-docs.kk.html#sec-type-definitions.

[osa1]

Didn't know about this manual, thanks.