Exotic Programming Ideas, Part 3: Effect Systems

Also see Oleg's "Effects without Monads: Non-determinism -- Back to the Meta-Language"

https://arxiv.org/abs/1905.06544

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.

The recent Unison language uses the effect system described in the Frank language https://www.unisonweb.org/

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. :)

Ever seen network protocols modeled in pure FP ?

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.

I always found IOException in Java to suffer from this problem.

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.

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.

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.

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.

Arrow Fx manage to be in a way colorless by obscoleting the need of Applicative, monad, etc https://arrow-kt.io/docs/fx/polymorphism/

> 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.

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.

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.)

Arrow Fx make monads obscoletes, see the table https://arrow-kt.io/docs/fx/polymorphism/

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 :-)

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

...that cannot be determined by the system (and must be specified by the user).

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.

(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)