8 ms·

Moving Beyond Type Systems

77 points by flexagoon 2y ago

sparkie 2y ago
> 4. External resources (files, I/O): this would be a very difficult topic if not for our simple question. Only writing to a file or outputting to an I/O stream is considered an effect, as only the process of writing mutates external state. Reading data creates new state, but does not modify it, therefore reading data of various sorts is not an effect. Because of this, printing is effectful, but reading from stdin is not. Lost me at this part. Of course reading is a side-effect. A function which reads from a file/console cannot be pure. Purity implies referential transparency - a function given the same arguments will always return the same result. If we consider the example given: pub fn read_guess() -> int { return io.read_int("Take a guess (0-100): "); } We should take `read_int` to be effectful because it will have the effect of advancing the position to read from in the console's buffer. If it didn't, it would always read from the same position, so even if the user took a second guess, the first guess would be read again the second time `read_int` is called. So given that `read_int` is effectful, so too is `read_guess`. > 1. Well, creating a variable is creating new state, but it’s not changing the state, therefore creating a variable is not an effect, but changing it is. Creating a local variable isn't a side-effect, but allocating a variable is a side effect. Sure enough, if we also free the allocation before leaving scope, we can avoid propagating that effect, but if you return a value that contains anything allocated by a function, then the function becomes effectful.
- fwlr 2y ago
  Later on the author makes the point that everything changes some various register deep in the guts of the CPU so by definition everything is always effect-full, but since we invented programming languages to get away from writing assembly, we shouldn’t consider that an effect when we’re not writing assembly. We invented many programming languages to get away from writing allocations and pointers into buffers too.
  - empath75 2y ago
    Yeah, but you're losing one of the things that you get from pure functional languages, which is determinism. The same function run multiple times may return different results.
  - chuckadams 2y ago
    It’s usually implied that “effect” pertains to observable effects. Anything that doesn’t affect referential transparency gets handwaved away. A memoized function might use a private stateful cache, but as long as it doesn’t affect determinism, you can keep its existence secret.
    - _nalply 2y ago
      A thought stroke me. Security struggles with timing leaks. That programming language would need something like a timing effect to control timing leaks. In such a programming language a memoized function is effectful on time.
      - deleted 2y ago
        [deleted]
  - jahewson 2y ago
    If you print to stdout but nobody is around to read it, does it count as an effect?
    - sparkie 2y ago
      Perfectly reasonable question. Basically, you can consider it a NOP if there's no observable side-effect. Obviously, stdout has a particular purpose and you wouldn't just disable the side-effect for one use case, but you could imagine having some pseudo console for the purpose of emitting debug messages which is considered a non-effect in your language (provided you can't read from it and reify the text back into values). In .NET for example, you can use `Debug.Write` and `Trace.Write` for emitting debug messages, and these lines are erased from the release version of the binary. You can mark any void-returning function with the `[Conditional("DEBUG")]` attribute and have calls to it erased because the DEBUG symbol is not defined in release versions. IMO, this should be standard in all languages - in languages with effects even moreso because we don't want to pass around an effect if our only use for it is debug or trace messages.
- Groxx 2y ago
  Seems like you could solve that by endlessly buffering stdin? Then you'd have to keep passing higher and higher offsets to read from, and old offsets would simply return their original, old values.
  - mitt_romney_12 2y ago
    What happens if you do: x = read_guess(); y = io.read_int("what's your name: "); z = read_guess(); How would your system ensure x and z are the same?
    - Groxx 2y ago
      You don't have that API. You offer x = read_guess(0) y = read_name("what's your name: ", len(x)) z = read_guess(len(x)+len(y)) If you read(0) twice, you get the same value both times.
      - mitt_romney_12 2y ago
        But now every function that reads from stdin needs to pass around an offset of where to read from which is very unergonomical. It also isn't really pure since offset is now state that is changing whenever a function is called. fn do_stuff(offset: int) -> (string, int) { x = read_guess(offset) y = read_name("what's your name: ", offset + len(x)) z = read_guess(offset+len(x)+len(y)) new_offset = offset+len(x)+len(y)+len(z) return ("name is: {y}, guess is: {x}", new_offset) }
        Groxx 2y ago
        Ergonomics isn't really the point of a hypothetical extreme system. And no, you can compute offset as a result of all inputs to the system, like I did in my example - just keep passing a "previous state" value around, and compute the next state and return it. Like any other functional system already does 99% of the time.
  - sparkie 2y ago
    It doesn't solve the referential transparency problem. To be referentially transparent, the buffer would need to be fixed in size, and have all of its data input prior to being used the first time. Essentially, it would akin to passing a read-only file as a command line argument to `main`.
- swiftcoder 2y ago
  The author has an entire paragraph dedicated to explaining the difference between "pure" in an effect system vs "pure" in a functional language. It might help to read the rest of the article
  - zsyllepsis 2y ago
    I think the author’s choice of function to demonstrate purity made this harder to grok as a reader. Asking the reader to “…exclude the I/O interactions…” when considering functional purity makes the analogy much harder to follow. My interpretation of the thesis of that paragraph is that localized mutation does not violate referential transparency, but getting there required some gracious reading. By the end of the section, we’re given an _example_ of an effectfully pure function, but no standalone definition. Based on that, I agree that this is a weak point in the overall piece.
turnsout 2y ago
What is the actual problem that this effect-oriented approach addresses? The effects of methods that are called by other methods will be concealed, so at the calling site, you'll have no idea that the high-level API `do_stuff` is going to utilize `io`. That is, unless the effect decoration "infects" the caller like `async`, in which case every complex API method will be decorated with a huge number of effects. Simply put, what does this buy us?
- wavemode 2y ago
  Effect systems have always felt to me like the functional programming community re-inventing dependency injection, but at the type level. At the term level, you could just let your function have a function as a parameter `read_file: IO -> String`, vs. annotating it with some kind of type-level "filesystem effect". And the former is a lot more flexible over time.
  - mitt_romney_12 2y ago
    This is an interesting approach but it has some issues with more more advanced effects. For example if you have a function that uses mutable state you would need to have the state both as an input and an output (for the original and the updated state) `update_mut: State -> String -> State` this isn't very economical as is probably worse than just `update_mut: String -> State ()`. If you commit to just having the parameters act as "markers" that don't actually relate to the implementation then you can get away with `update_mut: State -> String -> ()` but then you use one of the big benefits of effect systems which is that you can change the way effects work and have multiple different implementations.
  - 12_throw_away 2y ago
    > Effect systems have always felt to me like the functional programming community re-inventing dependency injection Yeah, so, in python, I've been playing around with "structured dependency injection", basically DI + ideas from structured concurrency (i.e., dependency injection bound to well-defined lexical scopes). And whenever I read about effects systems, it definitely feels like they're talking about, if not the same thing, at least something in the same nuclear family of things.
al2o3cr 2y ago
The article starts off with a motivating example of effects getting "bigger" when composed but I don't see where it does anything to contain / control that expansion (other than "proto" which does full inference) Seems like complex functions could end up with effects lists of unwieldy size, similar to how Elm programs end up with a giant "Msg" type.
- rebeccaskinner 2y ago
  This was the problem we saw in practice building an effects based system at work. It had a lot of nice properties, and type inference worked better than you might expect, but there was no way around the types with 100+ effects in the type signature, and people really disliked it. There are some things you can do to make it more ergonomic. One mistake we made was not focusing on ergonomics early on, and that lead to people having some pretty sour experiences. It's something you really have to pay a lot of attention to.
  - kristiandupont 2y ago
    Can you not combine effects into unions and/or intersections resulting in more abstract effects?
    - nextaccountic 2y ago
      In real world languages with effects, like F* or Koka, you can
- sparkie 2y ago
  The "getting bigger" actually happens in reverse. `main` has god-mode privileges, and it can selectively grant smaller or equivalent privileges to the functions it calls, which in turn, grant smaller or equivalent privileges to the functions they call. A function can't call another with greater privilege than it has itself. Ideally we should aim to grant only the necessary privileges to functions that need them, with the leaf functions in the call graph being pure functions - those which have no privilege to do anything but compute (or never return, which can be considered a side-effect). We might also want total pure functions, which are guaranteed to return (they only use primitive recursion), though there's no guarantee that they'll return in any reasonable time. Haskell is a pretty lousy example because it bundles everything up into one big `IO` privilege, which gets passed around everywhere, and monads aren't that great. Monad transformers are terrible at scaling.
User23 2y ago
Out of curiosity is there any point to a loop that doesn’t produce some effect in its body? Obviously I mean traditional imperative looping constructs and not map functions that return a value.
- kccqzy 2y ago
  No. In fact for example the C++ standard says such a loop can be optimized away by the compiler, even if syntax suggests it is an infinite loop.
  - kibwen 2y ago
    > No. This isn't quite correct, as demonstrated by the example of C++, because the act of turning a function that never halts (i.e. a function that is guaranteed to diverge) into a function that might halt is an observable effect. Rust actually relies on the fact that infinite loops are infinite, and they had to submit patches to LLVM to make it possible for languages to opt out of C++-style semantics: https://github.com/rust-lang/rust/issues/28728 https://github.com/rust-lang/rust/issues/28728
  - jkrejcha 2y ago
    C++ is pretty unique in considering infinite loops without side effects undefined behavior. It's allowed in C[1] as well as pretty much all mainstream programming languages from the low level to the high level (for good reason). Furthermore, there's an active proposal to match C by removing this undefined behavior in the cases C does[2]. Even in C++, it's uncommon for compilers to exploit it (especially in the trivial case) probably because, even if it's undefined, generally such behavior are pretty surprising and unexpected (and programmers do write infinite loops on purpose!). Having non-effect producing infinite loops is useful (and sometimes is the only safe way of performing an operation), especially in some low level code. Another commenter pointed out the idea of delays in microcontrollers[3] but I want to provide an example from operating systems. Take for example a panic function. At the end of it, you usually have an infinite loop of some sort, partly because you can't really safely do too much and panics generally represent a completely unrecoverable state from the operating system's point of view. A trivial for (;;) {} ...is useful. [1]: For constant expressions. [2]: https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2023/p2809r1.html https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2023/p28... [3]: https://news.ycombinator.com/item?id=40542860 https://news.ycombinator.com/item?id=40542860
rebeccaskinner 2y ago
I've been thinking a lot about effects systems recently. A few months ago I implemented an effects system based interpreter in Haskell for an embedded DSL prototype for a project at work. In our case, the effects we were concerned with were all some variation of reading data, and the effects based approach allowed us to statically ensure that data would be available, and let us perform some clever optimizations to reduce the overhead of large IO operations. We've since rewritten the system and, while we still support an optional effects based style in our DSL, it's not being used very heavily. In practice, our user found the ergonomics of the effects system quite challenging, and it introduced some type inference challenges. The biggest problem was that our use-cases ended up with functions that would have hundreds of effects, and it was fairly unwieldy and the type errors were difficult to deal with. Since we've introduced the updated version, most users prefer to user our newer features that allow them to write more traditional code even though it means they don't get composable effects. On the other side of the experience, I've come to believe that effects systems are a good idea, but when adding them to an existing language it's probably best to make them an opt-in feature that can be used to constrain specific small parts of a program, rather than something that should be applied globally. I also think we need a bit more research into the ergonomics before they are going to appeal to a lot of users. That said, the guarantees and optimization opportunities ours gave us were really nice, and were quite difficult to achieve without building on top of the effects system (our new system is about an order of magnitude more code, for example).
- deleted 2y ago
  [deleted]
- chuckadams 2y ago
  Just curious what you think of abilities in Unison? I've yet to use Unison in anger, but from what I've peeked at, abilities look really elegant to me.
  - rebeccaskinner 2y ago
    I like what I’ve seen of unison and I think it has some great ideas, but I haven’t had a chance to dive into it deeply enough to have a stronger opinion than that unfortunately.
name_nick_sex_m 2y ago
This post needs to justify itself with a solid real example of how this additional effect system provides value
taeric 2y ago
I can't but feel this is running head first into statements versus expressions. Specifically the part that views effects as growing in size and that being contrary to desired behavior. Strikes me as worrying about similar concerns. Seems more that it is the eager evaluation of each line of code that is a problem. Nothing wrong with growing the footprint of concern on code. The problem is how to annotate the concern. Consider, adding 'logger.whatever(...)' is likely not a concern to the program. Being able to annotate the logger as not an effect to check makes sense. Of course, all edge cases matter. Are the arguments eagerly evaluated? What if the logger doesn't even use them, due to level? With lisp, the magic wasn't only that you can treat code as data, but also that you could define code that ran at different times. And you could largely do that in "user space."
librasteve 2y ago
in the OP example, this is considered bad let x: string = "hello world"; x = 32; #type error however, a well designed strong typesystem should be able to compose types to allow this if desired by the coder (eg. to read in a column of numbers from a csv) my $forty-two = 42 but 'forty two'; say $forty-two+33; # OUTPUT: «75␤» say $forty-two.^name; # OUTPUT: «Int+{<anon|1>}␤» say $forty-two.Str; # OUTPUT: «forty two␤» Calling ^name shows that the variable is an Int with an anonymous object mixed in. However, that object is of type Str, so the variable, through the mixin, is endowed with a method with that name, which is what we use in the last sentence. https://docs.raku.org/routine/but https://docs.raku.org/routine/but
- 3836293648 2y ago
  It's bad because of the explicit signature. If the signature had been `string | int` thenn it's a type system feature
  - sparkie 2y ago
    Yeah, we can consider `string`, `int` to both be subtypes of `string | int`, and `string & int` to be a subtype of both `string`, `int`. There are some problems with doing so though, such as inferring the types, but this can be mostly mitigated by giving types a polarity, as Dolan introduced in Algebraic Subtyping[1]. This can be a bit hard to wrap your head around at first because given a function `f : a -> b`, the parameter `a` has negative polarity and return type `b` has positive polarity, but in the function body, the polarities are reversed, and the argument becomes positive, with the result value being negative. Local variables are ambipolar as they can be both introduced and eliminated in the function body. It becomes even more of a problem when you have types of kind `* -> *` or higher where the type argument can be covariant or contravariant. As far as I'm aware type inference for handling these in combination with algebraic subtyping is still an open problem. [1]:https://www.cs.tufts.edu/~nr/cs257/archive/stephen-dolan/thesis.pdf https://www.cs.tufts.edu/~nr/cs257/archive/stephen-dolan/the...
  - librasteve 2y ago
    good point - I am just a little reluctant to swallow that a strong type system is intended to stop us accidentally assigning a number to a string var - raku is an interesting case since the strong types in raku (aka perl6) were crafted so that the typical (untyped) perl case of my $x = "1"; print $x+1; #2 print $x.1; #'11' ('.' is perl for string concatenate) so in raku, untyped, thats my $x = "1"; say $x+1; #2 say $x~1; #'11' ('~' is raku for string concatenate) ok, but raku can be strongly typed too, so how to graduate to that without throwing out the first draft my IntStr $x = <1>; ('<>' is raku for Allomorph literal) say $x+1; #2 say $x~1; #'11' just reach for the IntStr type (it's built in and has a literal syntax sugar) the main idea for gradual typing to allow code to be evolved by adding types over time without necessarily knowing all the types you are going to settle on before you start

77 points by flexagoon 2y ago

> 4. External resources (files, I/O): this would be a very difficult topic if not for our simple question. Only writing to a file or outputting to an I/O stream is considered an effect, as only the process of writing mutates external state. Reading data creates new state, but does not modify it, therefore reading data of various sorts is not an effect. Because of this, printing is effectful, but reading from stdin is not. Lost me at this part. Of course reading is a side-effect. A function which reads from a file/console cannot be pure. Purity implies referential transparency - a function given the same arguments will always return the same result. If we consider the example given: pub fn read_guess() -> int { return io.read_int("Take a guess (0-100): "); } We should take `read_int` to be effectful because it will have the effect of advancing the position to read from in the console's buffer. If it didn't, it would always read from the same position, so even if the user took a second guess, the first guess would be read again the second time `read_int` is called. So given that `read_int` is effectful, so too is `read_guess`. > 1. Well, creating a variable is creating new state, but it’s not changing the state, therefore creating a variable is not an effect, but changing it is. Creating a local variable isn't a side-effect, but allocating a variable is a side effect. Sure enough, if we also free the allocation before leaving scope, we can avoid propagating that effect, but if you return a value that contains anything allocated by a function, then the function becomes effectful.

fwlr 2y ago
Later on the author makes the point that everything changes some various register deep in the guts of the CPU so by definition everything is always effect-full, but since we invented programming languages to get away from writing assembly, we shouldn’t consider that an effect when we’re not writing assembly. We invented many programming languages to get away from writing allocations and pointers into buffers too.
- empath75 2y ago
  Yeah, but you're losing one of the things that you get from pure functional languages, which is determinism. The same function run multiple times may return different results.
- chuckadams 2y ago
  It’s usually implied that “effect” pertains to observable effects. Anything that doesn’t affect referential transparency gets handwaved away. A memoized function might use a private stateful cache, but as long as it doesn’t affect determinism, you can keep its existence secret.
  - _nalply 2y ago
    A thought stroke me. Security struggles with timing leaks. That programming language would need something like a timing effect to control timing leaks. In such a programming language a memoized function is effectful on time.
    - deleted 2y ago
      [deleted]
- jahewson 2y ago
  If you print to stdout but nobody is around to read it, does it count as an effect?
  - sparkie 2y ago
    Perfectly reasonable question. Basically, you can consider it a NOP if there's no observable side-effect. Obviously, stdout has a particular purpose and you wouldn't just disable the side-effect for one use case, but you could imagine having some pseudo console for the purpose of emitting debug messages which is considered a non-effect in your language (provided you can't read from it and reify the text back into values). In .NET for example, you can use `Debug.Write` and `Trace.Write` for emitting debug messages, and these lines are erased from the release version of the binary. You can mark any void-returning function with the `[Conditional("DEBUG")]` attribute and have calls to it erased because the DEBUG symbol is not defined in release versions. IMO, this should be standard in all languages - in languages with effects even moreso because we don't want to pass around an effect if our only use for it is debug or trace messages.
Groxx 2y ago
Seems like you could solve that by endlessly buffering stdin? Then you'd have to keep passing higher and higher offsets to read from, and old offsets would simply return their original, old values.
- mitt_romney_12 2y ago
  What happens if you do: x = read_guess(); y = io.read_int("what's your name: "); z = read_guess(); How would your system ensure x and z are the same?
  - Groxx 2y ago
    You don't have that API. You offer x = read_guess(0) y = read_name("what's your name: ", len(x)) z = read_guess(len(x)+len(y)) If you read(0) twice, you get the same value both times.
    - mitt_romney_12 2y ago
      But now every function that reads from stdin needs to pass around an offset of where to read from which is very unergonomical. It also isn't really pure since offset is now state that is changing whenever a function is called. fn do_stuff(offset: int) -> (string, int) { x = read_guess(offset) y = read_name("what's your name: ", offset + len(x)) z = read_guess(offset+len(x)+len(y)) new_offset = offset+len(x)+len(y)+len(z) return ("name is: {y}, guess is: {x}", new_offset) }
      - Groxx 2y ago
        Ergonomics isn't really the point of a hypothetical extreme system. And no, you can compute offset as a result of all inputs to the system, like I did in my example - just keep passing a "previous state" value around, and compute the next state and return it. Like any other functional system already does 99% of the time.
- sparkie 2y ago
  It doesn't solve the referential transparency problem. To be referentially transparent, the buffer would need to be fixed in size, and have all of its data input prior to being used the first time. Essentially, it would akin to passing a read-only file as a command line argument to `main`.
swiftcoder 2y ago
The author has an entire paragraph dedicated to explaining the difference between "pure" in an effect system vs "pure" in a functional language. It might help to read the rest of the article
- zsyllepsis 2y ago
  I think the author’s choice of function to demonstrate purity made this harder to grok as a reader. Asking the reader to “…exclude the I/O interactions…” when considering functional purity makes the analogy much harder to follow. My interpretation of the thesis of that paragraph is that localized mutation does not violate referential transparency, but getting there required some gracious reading. By the end of the section, we’re given an _example_ of an effectfully pure function, but no standalone definition. Based on that, I agree that this is a weak point in the overall piece.

turnsout 2y ago

What is the actual problem that this effect-oriented approach addresses? The effects of methods that are called by other methods will be concealed, so at the calling site, you'll have no idea that the high-level API `do_stuff` is going to utilize `io`. That is, unless the effect decoration "infects" the caller like `async`, in which case every complex API method will be decorated with a huge number of effects. Simply put, what does this buy us?

wavemode 2y ago
Effect systems have always felt to me like the functional programming community re-inventing dependency injection, but at the type level. At the term level, you could just let your function have a function as a parameter `read_file: IO -> String`, vs. annotating it with some kind of type-level "filesystem effect". And the former is a lot more flexible over time.
- mitt_romney_12 2y ago
  This is an interesting approach but it has some issues with more more advanced effects. For example if you have a function that uses mutable state you would need to have the state both as an input and an output (for the original and the updated state) `update_mut: State -> String -> State` this isn't very economical as is probably worse than just `update_mut: String -> State ()`. If you commit to just having the parameters act as "markers" that don't actually relate to the implementation then you can get away with `update_mut: State -> String -> ()` but then you use one of the big benefits of effect systems which is that you can change the way effects work and have multiple different implementations.
- 12_throw_away 2y ago
  > Effect systems have always felt to me like the functional programming community re-inventing dependency injection Yeah, so, in python, I've been playing around with "structured dependency injection", basically DI + ideas from structured concurrency (i.e., dependency injection bound to well-defined lexical scopes). And whenever I read about effects systems, it definitely feels like they're talking about, if not the same thing, at least something in the same nuclear family of things.

al2o3cr 2y ago

The article starts off with a motivating example of effects getting "bigger" when composed but I don't see where it does anything to contain / control that expansion (other than "proto" which does full inference) Seems like complex functions could end up with effects lists of unwieldy size, similar to how Elm programs end up with a giant "Msg" type.

rebeccaskinner 2y ago
This was the problem we saw in practice building an effects based system at work. It had a lot of nice properties, and type inference worked better than you might expect, but there was no way around the types with 100+ effects in the type signature, and people really disliked it. There are some things you can do to make it more ergonomic. One mistake we made was not focusing on ergonomics early on, and that lead to people having some pretty sour experiences. It's something you really have to pay a lot of attention to.
- kristiandupont 2y ago
  Can you not combine effects into unions and/or intersections resulting in more abstract effects?
  - nextaccountic 2y ago
    In real world languages with effects, like F* or Koka, you can
sparkie 2y ago
The "getting bigger" actually happens in reverse. `main` has god-mode privileges, and it can selectively grant smaller or equivalent privileges to the functions it calls, which in turn, grant smaller or equivalent privileges to the functions they call. A function can't call another with greater privilege than it has itself. Ideally we should aim to grant only the necessary privileges to functions that need them, with the leaf functions in the call graph being pure functions - those which have no privilege to do anything but compute (or never return, which can be considered a side-effect). We might also want total pure functions, which are guaranteed to return (they only use primitive recursion), though there's no guarantee that they'll return in any reasonable time. Haskell is a pretty lousy example because it bundles everything up into one big `IO` privilege, which gets passed around everywhere, and monads aren't that great. Monad transformers are terrible at scaling.

User23 2y ago

Out of curiosity is there any point to a loop that doesn’t produce some effect in its body? Obviously I mean traditional imperative looping constructs and not map functions that return a value.

kccqzy 2y ago
No. In fact for example the C++ standard says such a loop can be optimized away by the compiler, even if syntax suggests it is an infinite loop.
- kibwen 2y ago
  > No. This isn't quite correct, as demonstrated by the example of C++, because the act of turning a function that never halts (i.e. a function that is guaranteed to diverge) into a function that might halt is an observable effect. Rust actually relies on the fact that infinite loops are infinite, and they had to submit patches to LLVM to make it possible for languages to opt out of C++-style semantics: https://github.com/rust-lang/rust/issues/28728 https://github.com/rust-lang/rust/issues/28728
- jkrejcha 2y ago
  C++ is pretty unique in considering infinite loops without side effects undefined behavior. It's allowed in C[1] as well as pretty much all mainstream programming languages from the low level to the high level (for good reason). Furthermore, there's an active proposal to match C by removing this undefined behavior in the cases C does[2]. Even in C++, it's uncommon for compilers to exploit it (especially in the trivial case) probably because, even if it's undefined, generally such behavior are pretty surprising and unexpected (and programmers do write infinite loops on purpose!). Having non-effect producing infinite loops is useful (and sometimes is the only safe way of performing an operation), especially in some low level code. Another commenter pointed out the idea of delays in microcontrollers[3] but I want to provide an example from operating systems. Take for example a panic function. At the end of it, you usually have an infinite loop of some sort, partly because you can't really safely do too much and panics generally represent a completely unrecoverable state from the operating system's point of view. A trivial for (;;) {} ...is useful. [1]: For constant expressions. [2]: https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2023/p2809r1.html https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2023/p28... [3]: https://news.ycombinator.com/item?id=40542860 https://news.ycombinator.com/item?id=40542860

rebeccaskinner 2y ago

I've been thinking a lot about effects systems recently. A few months ago I implemented an effects system based interpreter in Haskell for an embedded DSL prototype for a project at work. In our case, the effects we were concerned with were all some variation of reading data, and the effects based approach allowed us to statically ensure that data would be available, and let us perform some clever optimizations to reduce the overhead of large IO operations. We've since rewritten the system and, while we still support an optional effects based style in our DSL, it's not being used very heavily. In practice, our user found the ergonomics of the effects system quite challenging, and it introduced some type inference challenges. The biggest problem was that our use-cases ended up with functions that would have hundreds of effects, and it was fairly unwieldy and the type errors were difficult to deal with. Since we've introduced the updated version, most users prefer to user our newer features that allow them to write more traditional code even though it means they don't get composable effects. On the other side of the experience, I've come to believe that effects systems are a good idea, but when adding them to an existing language it's probably best to make them an opt-in feature that can be used to constrain specific small parts of a program, rather than something that should be applied globally. I also think we need a bit more research into the ergonomics before they are going to appeal to a lot of users. That said, the guarantees and optimization opportunities ours gave us were really nice, and were quite difficult to achieve without building on top of the effects system (our new system is about an order of magnitude more code, for example).

deleted 2y ago
[deleted]
chuckadams 2y ago
Just curious what you think of abilities in Unison? I've yet to use Unison in anger, but from what I've peeked at, abilities look really elegant to me.
- rebeccaskinner 2y ago
  I like what I’ve seen of unison and I think it has some great ideas, but I haven’t had a chance to dive into it deeply enough to have a stronger opinion than that unfortunately.

name_nick_sex_m 2y ago

This post needs to justify itself with a solid real example of how this additional effect system provides value

taeric 2y ago

I can't but feel this is running head first into statements versus expressions. Specifically the part that views effects as growing in size and that being contrary to desired behavior. Strikes me as worrying about similar concerns. Seems more that it is the eager evaluation of each line of code that is a problem. Nothing wrong with growing the footprint of concern on code. The problem is how to annotate the concern. Consider, adding 'logger.whatever(...)' is likely not a concern to the program. Being able to annotate the logger as not an effect to check makes sense. Of course, all edge cases matter. Are the arguments eagerly evaluated? What if the logger doesn't even use them, due to level? With lisp, the magic wasn't only that you can treat code as data, but also that you could define code that ran at different times. And you could largely do that in "user space."

librasteve 2y ago

in the OP example, this is considered bad let x: string = "hello world"; x = 32; #type error however, a well designed strong typesystem should be able to compose types to allow this if desired by the coder (eg. to read in a column of numbers from a csv) my $forty-two = 42 but 'forty two'; say $forty-two+33; # OUTPUT: «75␤» say $forty-two.^name; # OUTPUT: «Int+{<anon|1>}␤» say $forty-two.Str; # OUTPUT: «forty two␤» Calling ^name shows that the variable is an Int with an anonymous object mixed in. However, that object is of type Str, so the variable, through the mixin, is endowed with a method with that name, which is what we use in the last sentence. https://docs.raku.org/routine/but https://docs.raku.org/routine/but

3836293648 2y ago
It's bad because of the explicit signature. If the signature had been `string | int` thenn it's a type system feature
- sparkie 2y ago
  Yeah, we can consider `string`, `int` to both be subtypes of `string | int`, and `string & int` to be a subtype of both `string`, `int`. There are some problems with doing so though, such as inferring the types, but this can be mostly mitigated by giving types a polarity, as Dolan introduced in Algebraic Subtyping[1]. This can be a bit hard to wrap your head around at first because given a function `f : a -> b`, the parameter `a` has negative polarity and return type `b` has positive polarity, but in the function body, the polarities are reversed, and the argument becomes positive, with the result value being negative. Local variables are ambipolar as they can be both introduced and eliminated in the function body. It becomes even more of a problem when you have types of kind `* -> *` or higher where the type argument can be covariant or contravariant. As far as I'm aware type inference for handling these in combination with algebraic subtyping is still an open problem. [1]:https://www.cs.tufts.edu/~nr/cs257/archive/stephen-dolan/thesis.pdf https://www.cs.tufts.edu/~nr/cs257/archive/stephen-dolan/the...
- librasteve 2y ago
  good point - I am just a little reluctant to swallow that a strong type system is intended to stop us accidentally assigning a number to a string var - raku is an interesting case since the strong types in raku (aka perl6) were crafted so that the typical (untyped) perl case of my $x = "1"; print $x+1; #2 print $x.1; #'11' ('.' is perl for string concatenate) so in raku, untyped, thats my $x = "1"; say $x+1; #2 say $x~1; #'11' ('~' is raku for string concatenate) ok, but raku can be strongly typed too, so how to graduate to that without throwing out the first draft my IntStr $x = <1>; ('<>' is raku for Allomorph literal) say $x+1; #2 say $x~1; #'11' just reach for the IntStr type (it's built in and has a literal syntax sugar) the main idea for gradual typing to allow code to be evolved by adding types over time without necessarily knowing all the types you are going to settle on before you start