4 ms·

> 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 com

> 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.

throwaway17_17 4y ago
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.
- zesterer 4y ago
  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)! }
yccs27 4y ago
> 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?
- zesterer 4y ago
  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!

throwaway17_17 4y ago

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.

zesterer 4y ago
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)! }

yccs27 4y ago

> 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?

zesterer 4y ago
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!