3 ms·
This is cool! I really like the syntax for algebraic effects, which would be great for mocking. I also like the way that "impls" can be passed either explicitly
by jasonhansel 4y ago
This is cool! I really like the syntax for algebraic effects, which would be great for mocking. I also like the way that "impls" can be passed either explicitly or implicitly; the lack of global coherence seems like a reasonable tradeoff. Have you thought about using existential types to support dynamic dispatch (like Rust's "trait objects")?
That said, I'm a bit skeptical of the utility of refinement types (and dependent types in general). They greatly increase a language's complexity (by obscuring the type/value distinction and making type inference and checking more complicated). I'm not sure the benefits are worth it, particularly because of the so-called "specification problem."
- jfecher 4y agoThanks! IMO it is very important effects have an easy syntax to read/understand since they will be both used pervasively and be foreign to most new users. I do have an idea for "traits as types" which would cover static and dynamic dispatch: https://antelang.org/docs/ideas/#traits-as-types https://antelang.org/docs/ideas/#traits-as-types. So a use like `print (x: Show) : unit = ...` would be usable with static or dynamic dispatch and more complex cases like `print_all (x: Vec Show) : unit = ...` would use dynamic dispatch always. Perhaps this may be too confusing though, and there are other considerations as well which is why its only an idea for now. Your concern on refinement types is definitely valid and is something I've been thinking about. They are certainly useful in some cases like array indices or passing around certain predicates but whether these are useful enough to offset the implementation cost and brain tax is an open question.
- dixego 4y agoWhat is the specification problem? I don't think I've heard the term before.