top | item 25178437

Exotic Programming Ideas, Part 3: Effect Systems

293 points| psibi | 5 years ago |stephendiehl.com

94 comments

order
[+] siraben|5 years ago|reply
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

[1] https://github.com/frank-lang/frank

[2] Implementing free monads from scratch, https://siraben.github.io/2020/02/20/free-monads.html

[+] merelydev|5 years ago|reply
Source: 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.
[+] ledauphin|5 years ago|reply
I'm way out of my depth here, but interested in trying to understand a few of these things, particularly because I've long wondered how functional programmers reason about the "effects" that happen under the hood when dealing with Turing machines which are essentially 100% state.

Specifically:

1) do you consider variable reference to be an effect because you're getting a value from memory/disk/network? Or is it effectful simply because you're replacing a name with a value somehow? I'd love to understand the point of view here.

2) Relatedly, why do you say that creating a lexical closure is effectful (I assume here that we are storing an immutable memory address, or at least a value which represents a way to reliably find another value in the future), but using it (dereferencing that address/value) is not? I can see why you'd say that creating a dynamic closure is not effectful (the code is essentially unattached to anything at the time of creation and can easily be represented by a pure value), but using it is (it now inhabits a scope and will act differently depending on that scope).

Having typed that out, I wonder if what you mean is that creating the lexical closure in a language with immutable data means that at the time of creating the closure, you are (one way or another) making a copy of that data, which is an input "effect" in a sense. That isn't, of course, how things actually work in most non-functional (e.g. OO) languages - the lexical closure only binds the name, but the value represented by the name could in fact change if the data itself is mutable.

Anyway, I'm still curious about #1 above. These are the sorts of comments I come to Hacker News to read, so thank you. :)

[+] agumonkey|5 years ago|reply
Ever seen network protocols modeled in pure FP ?
[+] skybrian|5 years ago|reply
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.

[+] AaronFriel|5 years ago|reply
A properly done effects system with type-level annotation of the "color" of functions helps this, rather than hurts as you might surmise.

Take for example logging or tracing - we almost always in a modern backend application want an ambient trace or span ID and a log destination. What we don't want is to have to add those as parameters to _every function_.

So we want to paint these functions with the "logger" and "traced" colors, which respectively allow a function to send messages to an ambient logger via log(message: str) and to get the current trace context via getTraceContext() each with no other arguments.

The compiler will tell us if we call these functions from an unlogged, untraced function, so at a very high level - say at the RPC request level, we paint them early on. In Haskell we might even be able to do something like

    handleReq req = 
      withTraceSpan (...)
      . withLogging (...)
      $ handleReqInner req
Where handleReqInner requires these "colors".

Having too many effect handlers is never a problem either - you can always call an untraced function from a traced function. The "trace" effect handler just falls off at that call. Or in other words: you can always call a function whose colors are a subset of the call-site's.

This is somewhat a foreign concept to people who haven't worked with type systems like this and whose only concept of the color of function is purely binary - either async or not. In a good typed effect system, the compiler will assist you in knowing where you're missing an effect handler, and it will be easy to add those effect handlers sufficiently far from the business logic that you won't have to think about it.

[+] slaymaker1907|5 years ago|reply
Effect systems can actually make this less bad due to functions which are generic over effects. The function color problem is fundamentally because there usually isn't a way to be generic over different colored functions in a performant and ergonomic way.
[+] lambda_obrien|5 years ago|reply
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.

[+] lalaithion|5 years ago|reply
The "what color is my function" problem is insurmountable in Javascript, because the runtime does not allow you to call an async function from a non-async one. However, most effects aren't like this. If you say "this function needs randomness" then you can create a pure PRNG and call the function with the PRNG providing randomness. If you say "this function needs logging" you can tell it to log to a string and parse/ignore the string. If it throws an exception, you can catch the exception. Haskell even provides `unsafePerformIO`, which lets you run arbitrary computations as if they were pure.
[+] jiggawatts|5 years ago|reply
A lot of people are saying that function coloring is essentially an unsolved problem, and this is true. However, coloring of individual functions is not strictly speaking necessary.

Think of the classic "zlib" style C libraries. Often they can't assume anything about the target platform, even basic stuff like memory allocation or I/O, because there's such a huge variety compilers, standard libraries, and restrictions.

So just about every such library exports an "API context" struct, full of function pointers. These then allow the caller to pass in implementations for malloc, free, threading, I/O, etc...

The trick is that these can have default implementations. So the function pointer in the context for allocation can simply point to "malloc()". This can of course be overriden, so the capability is there, but the caller need not do anything by default.

Features like logging and tracing can be similarly sent through to default implementations that do nothing or call standard APIs in some naive (but sufficient) way.

[+] jahewson|5 years ago|reply
I always found IOException in Java to suffer from this problem.
[+] ianbicking|5 years ago|reply
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).

[+] andrewflnr|5 years ago|reply
I don't even see anything essentially type-based in effect systems. You could totally have effect-style APIs in dynamic languages, they just wouldn't be tracked and checked up front. I expect this has already been done a few times in Scheme.
[+] marcosdumay|5 years ago|reply
> 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.

[+] dan-robertson|5 years ago|reply
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|5 years ago|reply
> 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

[+] klodolph|5 years ago|reply
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.
[+] dustingetz|5 years ago|reply
It's not just about marking regions and checking them, "effect systems are fundamentally about dynamic dispatch (separating effect from effect handler)" Alexis King
[+] smegma2|5 years ago|reply
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|5 years ago|reply
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 :-)
[+] transfire|5 years ago|reply
I believe Kitten is another language exploring this area.
[+] PaulHoule|5 years ago|reply
"Non-termination is an Effect"
[+] daanx|5 years ago|reply
(Daan here, creator of [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)

[+] tomp|5 years ago|reply
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.
[+] SomeHacker44|5 years ago|reply
...that cannot be determined by the system (and must be specified by the user).