> Does your flavor of algebraic effects allow distinct effects of the same type

Could you give an example of what you mean by this? Multiple effects can be combined together (although I'm still working on handlers for multiple effects), for example:

    effect console = input + print

    fn greet_user : console ~ () = {
        print("Please enter your name:")!;
        let name = input!;
        print("Hello, " ++ name)!;
    }

> Do you have plans for making pattern matching extensible?

I have no plans as of yet. Extensible pattern-matching seems to me to be quite hard to unify with exhaustivity. Tao supports most of the patterns that Rust/Haskell supports.

> Could you give an example of what you mean by this?

I mean a type like `yield Nat + yield Nat ~ ()`. Here's how this would occur naturally: Define

    effect yield A is A => ()
    
    fn yield_each A, B, e : (A -> e ~ B) -> [A] -> e + yield B ~ () is
        | _, [] => ()
        \ f, [a .. as] => a->f!->yield!; as->yield_each(f)
    
    fn print_each A, B, e: (A -> e ~ B) -> e + print ~ () is
        f, l => l->yield_each(f)
            handle yield B with x => print(x->show)!

Here my_map should always behave the same as the standard map. The effect `yield B` is handled by collect, and the effect e is handled by the caller. But what happens if the effect e here is also yield?

    fn foo : print ~ [Nat] is
        [1, 2, 3]->my_map(n => yield(n)!; n+1)
         handle yield Nat with n => print("Processing " ++ n->show)!

Now yield_each effectively returns `yield Nat + yield Nat ~ ()`. Does this get combined into a single `yield Nat ~ ()`, so that the handler in print_each handles all yields?

Ah, I see what you mean. Yes, effects are always a set in terms of the final monomorphised type. This is an interesting case though, so I'll look into it further and see whether I can come up with sensible, unsurprising semantics. Thanks for pointing this out!

I think GP is referring to having two effects, like State1 and State2, both of which allow for stateful effects on int references, and then being able to handle the effects uniquely for each effect. I think the underlying type theoretical question would be are Tao’s effects nominally vs. structurally typed.

A more practical example would be having two state-like effects for use as different allocation/deallocation strategies.

Tao's effects are nominally typed, so there's no way to accidentally mix them up in the way I assume you're describing. For example:

    # Define a new effect that yields to the caller
    effect yield A = A => ()

    # A generator that emits numbers
    def one_two_three : yield Nat ~ () = {
        yield(1)!;
        yield(2)!;
        yield(3)!;
    }

    # Print the numbers to the console
    def main : io ~ () = {
        one_two_three
            handle yield Nat with n => print(n->show)!
    }