Wenhao Tang

When I run `make qasm` with Coq 8.13.1, the `id : R -> R` imported by `Require Import Reals.` overrides `Definition id := string.` and causes a compile error. So...

No runtime exception for the escape of named but unscoped handlers

3

The Section 5 of the paper _[First-class names for effect handlers](https://dl.acm.org/doi/abs/10.1145/3563289)_ mentions that when a named but unscoped handler is not found at runtime, an exception will be raised. However,...

[This blog](http://gallium.inria.fr/blog/safely-typing-algebraic-effects/) gives a good example showing the restriction to expressiveness of using row polymorphism for the effect system. In Links, the same problem happens with some slightly modification. Consider...

Why not always eta-expanding block parameters implicitly

2

Sometimes we need to eta-expand block parameters to enable contextual effect polymorphism. For example, ``` effect Ask1(): Int effect Ask2(): Int def asks() = { do Ask1() + do Ask2()...

Impure arity types

11

I tried to define some effects with impure arities / coarities (i.e., impure parameter and result types) but I failed. I wonder if this is possible in Effekt without using...