12 ms·

Exotic Programming Ideas, Part 3: Effect Systems

293 points by psibi 6y ago

PaulHoule 6y ago
"Non-termination is an Effect"
- SomeHacker44 6y ago
  ...that cannot be determined by the system (and must be specified by the user).
  - daanx 6y ago
    Just to add to this: Koka can (obviously :-)) not always determine if a function will terminate or not so it generally adds a `div` effect whenever there is the possibility of infinite recursion. However, since most data types in Koka are inductive, any recursion over such inductive data types are still inferred to be always terminating. In practice, it looks like about 70% of a typical program can usually be `total`, with 20% being `pure` (which is exceptions + divergence as in Haskell), and the final 10% being arbitrary side effects in the `io` effect.
    - ledauphin 6y ago
      these numbers are very useful to me even as a Python programmer, as they (somewhat) line up with my intuitions about how much of our programs can be expected to be written as (Python-) pure transforms, vs imperative shells. It's cool to think about a language being able to tell me this directly.
- tomp 6y ago
  I never understood this one. I mean obviously a kind compiler should warn you against using while true { } and while i < 5 { i—-; } but in general, I don’t find distinction between “this infinite loop terminates” (e.g. an event loop) and “this code obviously terminates but not in the lifetime of this universe” (e.g. computing Ackermann(5)) to be that useful.
  - creata 6y ago
    It's primarily useful for theorem proving, where a nonterminating argument corresponds to circular or otherwise unfounded reasoning. It's also useful because, in practice, we don't accidentally write code that "obviously terminates but not in the lifetime of this universe" as often as we accidentally write nonterminating code, so a lot of mistakes can still be caught by termination checking.
- daanx 6y ago
  (Daan here, creator of [Koka](https://github.com/koka-lang/koka https://github.com/koka-lang/koka) This is an interesting point and comes down to the question -- what is an effect really? I argue that effect types tell you the type signature of the mathematical function that models your program (the denotational semantics). For example, the function fun sqr(x : int) : total int { x*x } has no effect at all. The math function that gives semantics to `sqr` would have a type signature that can be directly derived from the effect type: [[int -> total int]] = Z -> Z (with Z the set of integers). Now, for a function that raises an exception, it would be: [[int -> exn int]] = Z -> (Z + 1) That is, either an integer (Z), or (+), a unit value (1) if an exception is raised. Similarly, a function that modifies a global heap h, would look like: [[int -> st<h> int]] = (H,Z) -> (H,Z) that is, it takes an initial heap H (besides the integer) and returns an updated heap with the result. Now, non-termination as an effect makes sense: a function like "turing-machine" may diverge, so: [[int -> div int]] = Z -> Z_\bot That is, its mathematical result is the set of integers (Z) together with an injected bottom value that represents non-termination. (note: We don't use "Z + \bot" here since we cannot distinguish if a function is not terminating or not (in contrast to exceptions)). In a language like Haskell every value may not terminate or cause an exception -- that is a value `x :: Int` really has type `Int_\bot`, and we cannot replace for example `x*0` with `0` in Haskell. Note that in almost all other languages, the semantic function is very complex with a global heap etc, any function `[[int -> int]]` becomes something like `(H,Z_32) -> (H,(Z_32 + 1))_\bot`. This is the essence of why it much harder for compilers and humans to reason about such functions (and why effect types can really help both programmers and compilers to do effective local reasoning)
  - skybrian 6y ago
    I'm wondering if you've found it useful in practice to distinguish between total and possibly-diverging functions? It seems like it's the sort of thing that's useful in something like Agda, where you use the existence of a function (without running it) to prove that its result exists. (The type is inhabited.) Or so I've read; I haven't used it. But if you're going to run the program, you typically want to know if a function will return promptly, and a total function could still spin for a million years calculating something, in a way that's indistinguishable in practice from diverging.
siraben 6y ago
I highly recommend Oleg Kiselyov's talk titled "Having an Effect"[0] in which he talks about - purely functional model of computation and its pitfalls - Actor model, effectful programming with requests and responses and an implementation in Haskell. - denotational semantics and combining effects. Once you have a model of your language, what if you want to extend it by adding another effect? It forces you to rewrite the semantics (and thus any interpreter of your language) completely. Taking using the effects-as-requests viewpoint, only the request and handler for an effect needs to be added or changed, and the rest untouched. This is known as "stable denotations". - really evaluating what it means for an expression to be pure or effectful. Even variable reference should be considered an effect. - different scoping rules in lambda calculus can be expressed in terms of effects! Creating a dynamic closure is not effectful, though applying it usually is, OTOH, creating a lexical closure is effectful but using it is not. I think Haskell provides a good example of how a purely functional language can still express effectful computation. through a monadic interface. Though monad transformers have their share of problems when heavily nested (n^2 instances, performance), various effect system libraries are gaining traction.[2] On the bleeding edge of research there's languages like Frank[1] where the effect system is pervasive throughout the language. [0] https://www.youtube.com/watch?v=GhERMBT7u4w https://www.youtube.com/watch?v=GhERMBT7u4w [1] https://github.com/frank-lang/frank https://github.com/frank-lang/frank [2] Implementing free monads from scratch, https://siraben.github.io/2020/02/20/free-monads.html https://siraben.github.io/2020/02/20/free-monads.html
- cultus 6y ago
  Also see Oleg's "Effects without Monads: Non-determinism -- Back to the Meta-Language" https://arxiv.org/abs/1905.06544 https://arxiv.org/abs/1905.06544
- merelydev 6y ago
  Source: https://www.reddit.com/r/programming/comments/7wbtg/who_is_oleg_kiselyov_no_really_can_anyone_post_a/ https://www.reddit.com/r/programming/comments/7wbtg/who_is_o... - Oleg eats lambdas for breakfast - The Y combinator fears Oleg - Oleg knows all the programs that halt on a Turing machine - Oleg is the guy that Chuck Norris goes to when he has an algorithm complexity question - Oleg reprograms his own DNA with Scheme macros - All of Oleg's Haskell programs are well-typed by definition - Oleg can read C++ compiler error messages. - Oleg built his house out of Prolog relations - Oleg speaks machine lanugage - Oleg once turned a zero into a one. - Emacs? Vi? Oleg wills files into existance - Oleg has the Haskell98 Report memorized. In Binary. In UTF-EBCDIC - Oleg can write unhygienic syntax-rules macros. - Sometimes Recursion gets confused when Oleg uses it.
skybrian 6y ago
I expect that, as with any other type system extension, the more granular your effects are, the more likely you are to run into a “what color is my function” problem. If you have a public API that declares certain effects, you’re stuck with those unless you break backward compatibility. In a practical system, when writing a library and especially an abstract interface, you’d want to be careful what you promise and declare effects that you might need (but currently don’t use), just in case you will need them later. It’s not that easy even to distinguish functions that can fail from those that can’t, if you’re trying to anticipate how a system will evolve. Something that’s in-memory now might change to being done over the network later.
- lambda_obrien 6y ago
  An effects system like this is more about controlling your own code and allowing for switching off implementations easily versus declaring what effects it has. Your declaration of effects on your function is saying, for example, "I need to output some text," and then in the caller of that function you have to do some action to "consume" that effect. For instance, your example might be an effect called "WriteState" and then you could call that function in a small unit test with a thin layer over a Map, in dev you could call it with a local sqlite db, and in prod you'd call it with your postgres or whatever. Each implementation shares a common interface, but does something different with the data. If you were writing a library, you'd give your public API as the base monad of your library, or as IO maybe, or even give a pure API. You should be dealing with the possible failures under that base context and then the user doesn't need to know about the inner failures. The effects system effectively acts as an abstraction for some side effect, like an interface, and gets ride of a lot of the boilerplate code needed for mtl or custom transformer stacks. Also, in strict typing it's pretty easy to refactor with modern linters and such, it actually makes refactoring an API change delightfully simple, just get rid of the red squiggle lines telling you you types are wrong.
  - skybrian 6y ago
    Refactoring tools are nice so long as you are in a closed-world environment where you can see all the code and make whatever changes are needed. They don't help nearly as much in an open environment where there are many code owners and not all code is visible to you. When you publish a library, a refactoring tool isn't going to tell you everyone who uses your library, and you don't have permission to change the call sites anyway. The only thing for it is to push a new, incompatible version and other people will have to migrate. So you're pushing off the work onto them. I don't see how an effects system helps with this much? It might help you better understand how you painted yourself in a corner, but I don't see how it helps you get out of it.
transfire 6y ago
I believe Kitten is another language exploring this area.
smegma2 6y ago
I was curious about this function: fun addRefs( a : forall<h> ref<h,int>, b : forall<h> ref<h,int> ) : total () { a := 10; b := 20; return (!a + !b); } Why is it total instead of st<h>? Won't this have a side effect of setting the references?
- daanx 6y ago
  Ah, I think Stephen meant to write the following: fun add-refs( a : ref<h,int>, b : ref<h,int> ) : st<h> int { a := 10 b := 20 (!a + !b) } where indeed the effect is `st<h>` as the updates are observable. How the function was written before, the two arguments use a "rank-2" polymorphic type and the heaps are fully abstract -- in that case it would be unobservable but you cannot create such values :-)
ianbicking 6y ago
I've had this idea of "dynamic returns" (akin to dynamic scope) in my head for a while. Reading this, it feels like a dynamically typed companion to effect systems. The idea of a dynamic return is just to give a formal way to accumulate things during a set of function calls, without having every function to be aware of what might be happening. In Python context managers are often used for this (e.g., contextlib.redirect_stdout to capture stdout), but thinking about it as another kind of return value instead of "capturing" would be an improvement IMHO. (You have to "capture" when hardcoded imperative code later needs to be retrofitted, but as it is retrofitting is all we have.) But dynamic returns aren't quite like an effect system unless you also create something more-or-less like a transaction or a changeset. We usually think about transactions as simply a way to rollback in case of an error, but as a changeset there's all kinds of interesting auditing and logging and debugging possibilities. E.g., if your effect is writing to stdout, you could rewrite all those changes (e.g., apply a filter, or add a text prefix to each line).
- marcosdumay 6y ago
  > E.g., if your effect is writing to stdout, you could rewrite all those changes Could you? Once you write something into stdout, as far as your program knows it could already be sent across the world and turned into a set of bank transactions, or missiles fired.
  - a1369209993 6y ago
    I think what they're proposing is that you'd buffer (not necessarily literally) those writes, then later (also not necessarily literally) pass them through a rewriting function before actually interacting with the operating system / environment.
- dan-robertson 6y ago
  Here are some features like that in Common Lisp, I think. Let me be clear about definitions: The dynamic extent of (an evaluation of) an expression is the interval of the program’s execution starting when evaluation of the expression begins and ending when control flows out of the expression (ie it returns a value or does some kind of nonlocal transfer of control) Something is lexically scoped if it may only be referred to by code which is syntactically inside the expression that creates the scope (eg in lisp, a let ordinarily creates a lexical scope but an anonymous function in the body of the let may continue to refer to the lexically scoped binding outside the dynamic extent of the binding; in JavaScript a var binding is in the lexical scope of body of the function in which it is bound) Something is dynamically scoped if it is available for the dynamic extent of whatever creates the scope. In Common Lisp most variables are lexically scoped inside the body of the let that defines them. Global variables (or other variables declared special) are dynamically scoped. One can write code like this: (defvar x 0) ; x is global so dynamically scoped (defun f (g) (let ((x 1)) (funcall g)) (let ((x 2)) (f (lambda () (print x)))) ; => 1 (print x) ; => 0 If x were not defined as a global the output would be 2. If the language had some kind of block scope which was neither dynamic nor lexical, the output would be 0. This dynamic scope is often used for the kind of “dynamic returns” you describe. There are global variables called e.g. standard-output [written with an asterisk on either side but hn just makes it italic] which one may (dynamically) bind to another stream to capture the output. Apart from the ordinary control flow out of expressions where they evaluate to something, there are three non local transfer of control constructs: - catch/throw are a dynamically scoped way of returning values. They work similarly to exceptions in Java or JavaScript except that instead of catch dispatching on the type of the object which is thrown, it dispatches on the identity of a “catch tag” which is associated with whatever value is thrown, and there is no catch-all construct (so it is relatively hard to interfere with someone else’s catch/throw. This is the Common Lisp construct I would refer to as “dynamic return.” These aren’t used very commonly as the below operators tend to be preferred. - block/return-from is lexically scoped but return-from is only valid within the dynamic extent of the corresponding block. Blocks are named by symbols. - tagbody/go is much like block/return-from except it is a lexically scoped goto rather than a return. Either could be implemented (potentially less efficiently) in terms of the other. There is another operator, unwind-protect, which works like a try–finally block in JavaScript to cause some code to run whenever the dynamic extent of an expression ends. Another example of these scoping concepts is in the condition system which handles errors and other conditions (like warnings or “signals”.) Typically this is implemented using a dynamically scoped variable holding the list of handlers which are currently in scope, and another for the restarts which are just functions. When a condition is signalled, the list of handlers is searched for a suitable handler which is a function that is called. This function has access to the lexical scope from where the handler was defined but runs in the dynamic scope from where the condition was signalled. It may choose to invoke one of the dynamically scoped restarts (proposed solutions to the condition, eg retry or abort) which is just a function that will typically transfer control to some place near to where it was defined. This is different from the traditional exception systems where by the time you catch an exception you’ve already unwound a lot of the stack (so it’s hard to resume from an earlier stage now.)
aozgaa 6y ago
> As far as I can tell no one uses this language [Koka] for anything, however it is downloadable and quite usable to explore these ideas. I believe the typesetting tool Madoko[1] is implemented in Koka, though in fairness Daan Leijen developed both Koka and Madoko. [1] https://github.com/koka-lang/madoko https://github.com/koka-lang/madoko
The_rationalist 6y ago
Arrow Fx implement this idea for Kotlin -> https://arrow-kt.io/docs/fx/ https://arrow-kt.io/docs/fx/
- valenterry 6y ago
  It only implements the first part, not the more difficult one of composing different kind of effects. Scala has a library for the difficult part, but I don't think it was very successful: https://github.com/atnos-org/eff https://github.com/atnos-org/eff
  - atennapel 6y ago
    There's also effekt for Scala: https://github.com/b-studios/scala-effekt https://github.com/b-studios/scala-effekt though it does not seem to be maintained.
    - valenterry 6y ago
      Yes - I think we can conclude that these techniques are both too complicated and not ergonomic enough as of now. If that does not work in Scala, it will work even less in Kotlin (where many people go when they find Scala too complex).
      - atennapel 6y ago
        I think something like algebraic effects can definitely be ergonomic and understandable, but a language definitely has to be designed for it. Algebraic effects are like exceptions in a lot of ways, so I think people will be able to understand them. See Effekt [1] and Koka [2] for languages that are designed with them in mind. [1] https://effekt-lang.org/ https://effekt-lang.org/ [2] https://koka-lang.github.io/koka/doc/kokaspec.html https://koka-lang.github.io/koka/doc/kokaspec.html
klodolph 6y ago
There's some interesting research and ideas here, but it does seem like monads "ate everything for lunch" back in the late 1990s and 2000s when it comes to encoding effects, probably because monads are a bit more ergonomic (which seems like a weird thing to say, given the reputation monads have for being abstract nonsense). So effect systems didn't get as much research as everyone was interested in monads, and now that monads have dried up a bit as a field of research for encoding effects, I'm interested to see what other systems people invent.
- The_rationalist 6y ago
  Arrow Fx make monads obscoletes, see the table https://arrow-kt.io/docs/fx/polymorphism/ https://arrow-kt.io/docs/fx/polymorphism/
  - klodolph 6y ago
    The page you linked to describes monads. It sounds like you’re not describing something that makes monads obsolete, but merely a DSL for Kotlin that makes it easier to use monads. Haskell doesn't need that, because monads are already part of the core syntax of the language.
    - The_rationalist 6y ago
      You clearly didn't read the table that compare the verbosity and cognitive overhead of the Haskell way vs the fx way
      - klodolph 6y ago
        > You clearly didn't read… Just a word of advice—you’re digging yourself in a hole if you make low-quality, ad-hominem comments like that. Comments of the form “you didn’t read X” are specifically discouraged on HN. Maybe you feel good writing it, but nobody feels good reading it and nobody learns anything. I took another look at the page you linked and it still looks like syntactic sugar for Monads. It’s still monads. Monads monads monads. Applicative and Functor are generalizations of Monad.
toolslive 6y ago
Ocaml (almost ?) has it. https://www.janestreet.com/tech-talks/effective-programming/ https://www.janestreet.com/tech-talks/effective-programming/
dustingetz 6y ago
It's not just about marking regions and checking them, "effect systems are fundamentally about dynamic dispatch (separating effect from effect handler)" Alexis King

293 points by psibi 6y ago

PaulHoule 6y ago

"Non-termination is an Effect"

SomeHacker44 6y ago
...that cannot be determined by the system (and must be specified by the user).
- daanx 6y ago
  Just to add to this: Koka can (obviously :-)) not always determine if a function will terminate or not so it generally adds a `div` effect whenever there is the possibility of infinite recursion. However, since most data types in Koka are inductive, any recursion over such inductive data types are still inferred to be always terminating. In practice, it looks like about 70% of a typical program can usually be `total`, with 20% being `pure` (which is exceptions + divergence as in Haskell), and the final 10% being arbitrary side effects in the `io` effect.
  - ledauphin 6y ago
    these numbers are very useful to me even as a Python programmer, as they (somewhat) line up with my intuitions about how much of our programs can be expected to be written as (Python-) pure transforms, vs imperative shells. It's cool to think about a language being able to tell me this directly.
tomp 6y ago
I never understood this one. I mean obviously a kind compiler should warn you against using while true { } and while i < 5 { i—-; } but in general, I don’t find distinction between “this infinite loop terminates” (e.g. an event loop) and “this code obviously terminates but not in the lifetime of this universe” (e.g. computing Ackermann(5)) to be that useful.
- creata 6y ago
  It's primarily useful for theorem proving, where a nonterminating argument corresponds to circular or otherwise unfounded reasoning. It's also useful because, in practice, we don't accidentally write code that "obviously terminates but not in the lifetime of this universe" as often as we accidentally write nonterminating code, so a lot of mistakes can still be caught by termination checking.
daanx 6y ago
(Daan here, creator of [Koka](https://github.com/koka-lang/koka https://github.com/koka-lang/koka) This is an interesting point and comes down to the question -- what is an effect really? I argue that effect types tell you the type signature of the mathematical function that models your program (the denotational semantics). For example, the function fun sqr(x : int) : total int { x*x } has no effect at all. The math function that gives semantics to `sqr` would have a type signature that can be directly derived from the effect type: [[int -> total int]] = Z -> Z (with Z the set of integers). Now, for a function that raises an exception, it would be: [[int -> exn int]] = Z -> (Z + 1) That is, either an integer (Z), or (+), a unit value (1) if an exception is raised. Similarly, a function that modifies a global heap h, would look like: [[int -> st<h> int]] = (H,Z) -> (H,Z) that is, it takes an initial heap H (besides the integer) and returns an updated heap with the result. Now, non-termination as an effect makes sense: a function like "turing-machine" may diverge, so: [[int -> div int]] = Z -> Z_\bot That is, its mathematical result is the set of integers (Z) together with an injected bottom value that represents non-termination. (note: We don't use "Z + \bot" here since we cannot distinguish if a function is not terminating or not (in contrast to exceptions)). In a language like Haskell every value may not terminate or cause an exception -- that is a value `x :: Int` really has type `Int_\bot`, and we cannot replace for example `x*0` with `0` in Haskell. Note that in almost all other languages, the semantic function is very complex with a global heap etc, any function `[[int -> int]]` becomes something like `(H,Z_32) -> (H,(Z_32 + 1))_\bot`. This is the essence of why it much harder for compilers and humans to reason about such functions (and why effect types can really help both programmers and compilers to do effective local reasoning)
- skybrian 6y ago
  I'm wondering if you've found it useful in practice to distinguish between total and possibly-diverging functions? It seems like it's the sort of thing that's useful in something like Agda, where you use the existence of a function (without running it) to prove that its result exists. (The type is inhabited.) Or so I've read; I haven't used it. But if you're going to run the program, you typically want to know if a function will return promptly, and a total function could still spin for a million years calculating something, in a way that's indistinguishable in practice from diverging.

siraben 6y ago

I highly recommend Oleg Kiselyov's talk titled "Having an Effect"[0] in which he talks about - purely functional model of computation and its pitfalls - Actor model, effectful programming with requests and responses and an implementation in Haskell. - denotational semantics and combining effects. Once you have a model of your language, what if you want to extend it by adding another effect? It forces you to rewrite the semantics (and thus any interpreter of your language) completely. Taking using the effects-as-requests viewpoint, only the request and handler for an effect needs to be added or changed, and the rest untouched. This is known as "stable denotations". - really evaluating what it means for an expression to be pure or effectful. Even variable reference should be considered an effect. - different scoping rules in lambda calculus can be expressed in terms of effects! Creating a dynamic closure is not effectful, though applying it usually is, OTOH, creating a lexical closure is effectful but using it is not. I think Haskell provides a good example of how a purely functional language can still express effectful computation. through a monadic interface. Though monad transformers have their share of problems when heavily nested (n^2 instances, performance), various effect system libraries are gaining traction.[2] On the bleeding edge of research there's languages like Frank[1] where the effect system is pervasive throughout the language. [0] https://www.youtube.com/watch?v=GhERMBT7u4w https://www.youtube.com/watch?v=GhERMBT7u4w [1] https://github.com/frank-lang/frank https://github.com/frank-lang/frank [2] Implementing free monads from scratch, https://siraben.github.io/2020/02/20/free-monads.html https://siraben.github.io/2020/02/20/free-monads.html

cultus 6y ago
Also see Oleg's "Effects without Monads: Non-determinism -- Back to the Meta-Language" https://arxiv.org/abs/1905.06544 https://arxiv.org/abs/1905.06544
merelydev 6y ago
Source: https://www.reddit.com/r/programming/comments/7wbtg/who_is_oleg_kiselyov_no_really_can_anyone_post_a/ https://www.reddit.com/r/programming/comments/7wbtg/who_is_o... - Oleg eats lambdas for breakfast - The Y combinator fears Oleg - Oleg knows all the programs that halt on a Turing machine - Oleg is the guy that Chuck Norris goes to when he has an algorithm complexity question - Oleg reprograms his own DNA with Scheme macros - All of Oleg's Haskell programs are well-typed by definition - Oleg can read C++ compiler error messages. - Oleg built his house out of Prolog relations - Oleg speaks machine lanugage - Oleg once turned a zero into a one. - Emacs? Vi? Oleg wills files into existance - Oleg has the Haskell98 Report memorized. In Binary. In UTF-EBCDIC - Oleg can write unhygienic syntax-rules macros. - Sometimes Recursion gets confused when Oleg uses it.

skybrian 6y ago

I expect that, as with any other type system extension, the more granular your effects are, the more likely you are to run into a “what color is my function” problem. If you have a public API that declares certain effects, you’re stuck with those unless you break backward compatibility. In a practical system, when writing a library and especially an abstract interface, you’d want to be careful what you promise and declare effects that you might need (but currently don’t use), just in case you will need them later. It’s not that easy even to distinguish functions that can fail from those that can’t, if you’re trying to anticipate how a system will evolve. Something that’s in-memory now might change to being done over the network later.

lambda_obrien 6y ago
An effects system like this is more about controlling your own code and allowing for switching off implementations easily versus declaring what effects it has. Your declaration of effects on your function is saying, for example, "I need to output some text," and then in the caller of that function you have to do some action to "consume" that effect. For instance, your example might be an effect called "WriteState" and then you could call that function in a small unit test with a thin layer over a Map, in dev you could call it with a local sqlite db, and in prod you'd call it with your postgres or whatever. Each implementation shares a common interface, but does something different with the data. If you were writing a library, you'd give your public API as the base monad of your library, or as IO maybe, or even give a pure API. You should be dealing with the possible failures under that base context and then the user doesn't need to know about the inner failures. The effects system effectively acts as an abstraction for some side effect, like an interface, and gets ride of a lot of the boilerplate code needed for mtl or custom transformer stacks. Also, in strict typing it's pretty easy to refactor with modern linters and such, it actually makes refactoring an API change delightfully simple, just get rid of the red squiggle lines telling you you types are wrong.
- skybrian 6y ago
  Refactoring tools are nice so long as you are in a closed-world environment where you can see all the code and make whatever changes are needed. They don't help nearly as much in an open environment where there are many code owners and not all code is visible to you. When you publish a library, a refactoring tool isn't going to tell you everyone who uses your library, and you don't have permission to change the call sites anyway. The only thing for it is to push a new, incompatible version and other people will have to migrate. So you're pushing off the work onto them. I don't see how an effects system helps with this much? It might help you better understand how you painted yourself in a corner, but I don't see how it helps you get out of it.

transfire 6y ago

I believe Kitten is another language exploring this area.

smegma2 6y ago

I was curious about this function: fun addRefs( a : forall<h> ref<h,int>, b : forall<h> ref<h,int> ) : total () { a := 10; b := 20; return (!a + !b); } Why is it total instead of st<h>? Won't this have a side effect of setting the references?

daanx 6y ago
Ah, I think Stephen meant to write the following: fun add-refs( a : ref<h,int>, b : ref<h,int> ) : st<h> int { a := 10 b := 20 (!a + !b) } where indeed the effect is `st<h>` as the updates are observable. How the function was written before, the two arguments use a "rank-2" polymorphic type and the heaps are fully abstract -- in that case it would be unobservable but you cannot create such values :-)

ianbicking 6y ago

I've had this idea of "dynamic returns" (akin to dynamic scope) in my head for a while. Reading this, it feels like a dynamically typed companion to effect systems. The idea of a dynamic return is just to give a formal way to accumulate things during a set of function calls, without having every function to be aware of what might be happening. In Python context managers are often used for this (e.g., contextlib.redirect_stdout to capture stdout), but thinking about it as another kind of return value instead of "capturing" would be an improvement IMHO. (You have to "capture" when hardcoded imperative code later needs to be retrofitted, but as it is retrofitting is all we have.) But dynamic returns aren't quite like an effect system unless you also create something more-or-less like a transaction or a changeset. We usually think about transactions as simply a way to rollback in case of an error, but as a changeset there's all kinds of interesting auditing and logging and debugging possibilities. E.g., if your effect is writing to stdout, you could rewrite all those changes (e.g., apply a filter, or add a text prefix to each line).

marcosdumay 6y ago
> E.g., if your effect is writing to stdout, you could rewrite all those changes Could you? Once you write something into stdout, as far as your program knows it could already be sent across the world and turned into a set of bank transactions, or missiles fired.
- a1369209993 6y ago
  I think what they're proposing is that you'd buffer (not necessarily literally) those writes, then later (also not necessarily literally) pass them through a rewriting function before actually interacting with the operating system / environment.
dan-robertson 6y ago
Here are some features like that in Common Lisp, I think. Let me be clear about definitions: The dynamic extent of (an evaluation of) an expression is the interval of the program’s execution starting when evaluation of the expression begins and ending when control flows out of the expression (ie it returns a value or does some kind of nonlocal transfer of control) Something is lexically scoped if it may only be referred to by code which is syntactically inside the expression that creates the scope (eg in lisp, a let ordinarily creates a lexical scope but an anonymous function in the body of the let may continue to refer to the lexically scoped binding outside the dynamic extent of the binding; in JavaScript a var binding is in the lexical scope of body of the function in which it is bound) Something is dynamically scoped if it is available for the dynamic extent of whatever creates the scope. In Common Lisp most variables are lexically scoped inside the body of the let that defines them. Global variables (or other variables declared special) are dynamically scoped. One can write code like this: (defvar x 0) ; x is global so dynamically scoped (defun f (g) (let ((x 1)) (funcall g)) (let ((x 2)) (f (lambda () (print x)))) ; => 1 (print x) ; => 0 If x were not defined as a global the output would be 2. If the language had some kind of block scope which was neither dynamic nor lexical, the output would be 0. This dynamic scope is often used for the kind of “dynamic returns” you describe. There are global variables called e.g. standard-output [written with an asterisk on either side but hn just makes it italic] which one may (dynamically) bind to another stream to capture the output. Apart from the ordinary control flow out of expressions where they evaluate to something, there are three non local transfer of control constructs: - catch/throw are a dynamically scoped way of returning values. They work similarly to exceptions in Java or JavaScript except that instead of catch dispatching on the type of the object which is thrown, it dispatches on the identity of a “catch tag” which is associated with whatever value is thrown, and there is no catch-all construct (so it is relatively hard to interfere with someone else’s catch/throw. This is the Common Lisp construct I would refer to as “dynamic return.” These aren’t used very commonly as the below operators tend to be preferred. - block/return-from is lexically scoped but return-from is only valid within the dynamic extent of the corresponding block. Blocks are named by symbols. - tagbody/go is much like block/return-from except it is a lexically scoped goto rather than a return. Either could be implemented (potentially less efficiently) in terms of the other. There is another operator, unwind-protect, which works like a try–finally block in JavaScript to cause some code to run whenever the dynamic extent of an expression ends. Another example of these scoping concepts is in the condition system which handles errors and other conditions (like warnings or “signals”.) Typically this is implemented using a dynamically scoped variable holding the list of handlers which are currently in scope, and another for the restarts which are just functions. When a condition is signalled, the list of handlers is searched for a suitable handler which is a function that is called. This function has access to the lexical scope from where the handler was defined but runs in the dynamic scope from where the condition was signalled. It may choose to invoke one of the dynamically scoped restarts (proposed solutions to the condition, eg retry or abort) which is just a function that will typically transfer control to some place near to where it was defined. This is different from the traditional exception systems where by the time you catch an exception you’ve already unwound a lot of the stack (so it’s hard to resume from an earlier stage now.)

aozgaa 6y ago

> As far as I can tell no one uses this language [Koka] for anything, however it is downloadable and quite usable to explore these ideas. I believe the typesetting tool Madoko[1] is implemented in Koka, though in fairness Daan Leijen developed both Koka and Madoko. [1] https://github.com/koka-lang/madoko https://github.com/koka-lang/madoko

The_rationalist 6y ago

Arrow Fx implement this idea for Kotlin -> https://arrow-kt.io/docs/fx/ https://arrow-kt.io/docs/fx/

valenterry 6y ago
It only implements the first part, not the more difficult one of composing different kind of effects. Scala has a library for the difficult part, but I don't think it was very successful: https://github.com/atnos-org/eff https://github.com/atnos-org/eff
- atennapel 6y ago
  There's also effekt for Scala: https://github.com/b-studios/scala-effekt https://github.com/b-studios/scala-effekt though it does not seem to be maintained.
  - valenterry 6y ago
    Yes - I think we can conclude that these techniques are both too complicated and not ergonomic enough as of now. If that does not work in Scala, it will work even less in Kotlin (where many people go when they find Scala too complex).
    - atennapel 6y ago
      I think something like algebraic effects can definitely be ergonomic and understandable, but a language definitely has to be designed for it. Algebraic effects are like exceptions in a lot of ways, so I think people will be able to understand them. See Effekt [1] and Koka [2] for languages that are designed with them in mind. [1] https://effekt-lang.org/ https://effekt-lang.org/ [2] https://koka-lang.github.io/koka/doc/kokaspec.html https://koka-lang.github.io/koka/doc/kokaspec.html

klodolph 6y ago

There's some interesting research and ideas here, but it does seem like monads "ate everything for lunch" back in the late 1990s and 2000s when it comes to encoding effects, probably because monads are a bit more ergonomic (which seems like a weird thing to say, given the reputation monads have for being abstract nonsense). So effect systems didn't get as much research as everyone was interested in monads, and now that monads have dried up a bit as a field of research for encoding effects, I'm interested to see what other systems people invent.

The_rationalist 6y ago
Arrow Fx make monads obscoletes, see the table https://arrow-kt.io/docs/fx/polymorphism/ https://arrow-kt.io/docs/fx/polymorphism/
- klodolph 6y ago
  The page you linked to describes monads. It sounds like you’re not describing something that makes monads obsolete, but merely a DSL for Kotlin that makes it easier to use monads. Haskell doesn't need that, because monads are already part of the core syntax of the language.
  - The_rationalist 6y ago
    You clearly didn't read the table that compare the verbosity and cognitive overhead of the Haskell way vs the fx way
    - klodolph 6y ago
      > You clearly didn't read… Just a word of advice—you’re digging yourself in a hole if you make low-quality, ad-hominem comments like that. Comments of the form “you didn’t read X” are specifically discouraged on HN. Maybe you feel good writing it, but nobody feels good reading it and nobody learns anything. I took another look at the page you linked and it still looks like syntactic sugar for Monads. It’s still monads. Monads monads monads. Applicative and Functor are generalizations of Monad.

toolslive 6y ago

Ocaml (almost ?) has it. https://www.janestreet.com/tech-talks/effective-programming/ https://www.janestreet.com/tech-talks/effective-programming/

dustingetz 6y ago

It's not just about marking regions and checking them, "effect systems are fundamentally about dynamic dispatch (separating effect from effect handler)" Alexis King