An entire post about effect systems and no mention of freer monads/algebraic effects? The Rust community truly is doomed to keep recreating ideas from PLT because, despite the fact that their...
An entire post about effect systems and no mention of freer monads/algebraic effects? The Rust community truly is doomed to keep recreating ideas from PLT because, despite the fact that their language is heavily influenced by PLT and type theory, they're weirdly parochial about it.
I also question the "total function" terminology at the end. It shouldn't be "total", because that implies terminating, but nontermination is not an effect! (Well, in most languages, anyway.) It should be "pure" instead.
I saw that, but I don't think that's what I'm talking about. (Actually, I find that line a little mystifying: just about everything is represented as an ADT in ML-family languages, so I'm not sure...
I saw that, but I don't think that's what I'm talking about. (Actually, I find that line a little mystifying: just about everything is represented as an ADT in ML-family languages, so I'm not sure exactly what concept is being referred to here.) The ideas I'm talking about are from Extensible Effects and Freer Monads, More Extensible Effects, and implemented in libraries like polysemy.
I should also mention that this is somewhat "advanced"; the "state of the art" when it comes to representing effects functionally is monads, or, more generally, monad transformers. This also leverages type system machinery.
I guess my fundamental problem is with this conclusion:
effects have nothing to do with regular old types! Despite being representable in a type system, they don’t have much resemblance to types as we know them.
The way I see it, OP has extended the type system, giving it special machinery to handle effects. That's fine and all, but I don't see how it's moving beyond the type system. And while it probably has upsides, especially WRT usability, adding special machinery to handle something that can already be represented also has downsides.
EDIT: On further thinking, some special machinery is probably much more useful for a non-purely-functional language like Rust than it would be for something like Haskell.
Regarding "do types or effects shrink or grow," I would expect them to grow sometimes and be checked at an API boundary. For example, for a TypeScript function: function foo(x) { if (x) return...
Regarding "do types or effects shrink or grow," I would expect them to grow sometimes and be checked at an API boundary.
For example, for a TypeScript function:
function foo(x) {
if (x) return "hello";
return false;
}
Then it does indeed 'grow' the return type by inferring it to be false | "hello". It will add more possibilities if you add more return statements. That might be more specific or more general than you intended. If you want to catch mistakes and keep the API stable, then you need to declare the return type.
Also, reads often do create new state due to auditing. A HTTP request typically creates a log entry. If a filesystem has the concept of an access time, reading a file will update it. Even reading memory can result in a page getting loaded from disk, and it will update various OS statistics.
Whether these side-effects count depends on what you care about. Often, it simplifies things to ignore them. Type systems shouldn't track more than needed since it adds constraints and complexity.
It seems like effect tracking should be motivated by a problem. In Rust, it was preventing concurrency errors in multithreaded programs.
An entire post about effect systems and no mention of freer monads/algebraic effects? The Rust community truly is doomed to keep recreating ideas from PLT because, despite the fact that their language is heavily influenced by PLT and type theory, they're weirdly parochial about it.
I also question the "total function" terminology at the end. It shouldn't be "total", because that implies terminating, but nontermination is not an effect! (Well, in most languages, anyway.) It should be "pure" instead.
The article does have this:
Is that what you mean by "algebraic effects" or is there more to it?
I saw that, but I don't think that's what I'm talking about. (Actually, I find that line a little mystifying: just about everything is represented as an ADT in ML-family languages, so I'm not sure exactly what concept is being referred to here.) The ideas I'm talking about are from Extensible Effects and Freer Monads, More Extensible Effects, and implemented in libraries like polysemy.
I should also mention that this is somewhat "advanced"; the "state of the art" when it comes to representing effects functionally is monads, or, more generally, monad transformers. This also leverages type system machinery.
I guess my fundamental problem is with this conclusion:
The way I see it, OP has extended the type system, giving it special machinery to handle effects. That's fine and all, but I don't see how it's moving beyond the type system. And while it probably has upsides, especially WRT usability, adding special machinery to handle something that can already be represented also has downsides.
EDIT: On further thinking, some special machinery is probably much more useful for a non-purely-functional language like Rust than it would be for something like Haskell.
Regarding "do types or effects shrink or grow," I would expect them to grow sometimes and be checked at an API boundary.
For example, for a TypeScript function:
Then it does indeed 'grow' the return type by inferring it to be
false | "hello". It will add more possibilities if you add more return statements. That might be more specific or more general than you intended. If you want to catch mistakes and keep the API stable, then you need to declare the return type.Also, reads often do create new state due to auditing. A HTTP request typically creates a log entry. If a filesystem has the concept of an access time, reading a file will update it. Even reading memory can result in a page getting loaded from disk, and it will update various OS statistics.
Whether these side-effects count depends on what you care about. Often, it simplifies things to ignore them. Type systems shouldn't track more than needed since it adds constraints and complexity.
It seems like effect tracking should be motivated by a problem. In Rust, it was preventing concurrency errors in multithreaded programs.