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.
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
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 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.
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.
We've been there with Java. An API takes a Runnable. You need to do something that does IO, so you catch the exception... and then what? Log and suppress it? This is how bad code happens. At best you get chained exceptions.
With Callable, they got smarter and declared it to throw Exception, which means it can only be easily propagated by other methods that declare they throw Exception. So it's a viral declaration, unless you engage in workarounds like exception wrapping.
You don't need an effect system for this to happen, though. In Go, you don't have the problem with different kinds of errors, but you can still classify functions into two categories: those that may return an error, and those that (apparently) always succeed. If you need to fix the API, you might end up with lots of refactoring [1].
Mistakes at the API level can be hard to fix without touching lots of API's. This is unsolvable in general. The only way to avoid workarounds (via escape hatches or by mocking things out) is to standardize whatever you can so it works together.
[1] https://www.dolthub.com/blog/2020-11-16-panics-to-errors/
Never understood why the browser didn’t ship a full access to something like an EventEmitter. Since you can dispatch events on window document DOM elements etc seems like being able to subscribe to events in a more arbitrary fashion that worked in parallel to the other events would have been useful and solved callback hell all the same
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.
The common modern example being async functions, I would say it's actually quite surprising that JavaScript can't seem to provide the sane default behavior of "block this non-async function until the async function it calls returns a value".
The reason it can't is simply that it chooses not to provide a runtime with a true threading model - blocking a non-async function means literally blocking the entire runtime. But there's a possible world in which a "colored" (async) function could be used directly in a synchronous function using an escape hatch provided by the runtime, and then async functions would no longer be colored in the same way.
R process<R, E extends Exception>(ThrowingFunction<Long, R, E> processor) throws E { ... }
Checked exceptions a "bolted on" effect that sits outside the usual type system in Java, and their presence on a method signature "colours" it in a way that an effect described inside a type system would not. More of a stain than a tint, if you will.
Java 8 resolved it by quietly pretending checked exceptions never happened, which works fine until (1) you get unhandled unchecked exceptions in all their glory at runtime, and (2) you want to use one of the Java 7 or earlier methods as a "processor" but, oh no, it throws an exception.
(It's a deeper colouring than JavaScript's async/await keyword, which is just syntactic sugar around continuations in callbacks and returning promises - you can pass an async "processor" function to a "process" function that has no idea what it's getting and get back the promise you'd expect from it.)
- 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
- 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.Not only can he do it, he even wrote a paper about it: https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.36...
- Oleg can read C++ compiler error messages.
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. :)
To give an example, say you have int* x. When the expression (*x) is used later on, it is the dereference that is effectful. In other words, the expression lacks referential transparency.
Going further, Oleg says that "an expression is effectful if it sends a message to its context". The example he gives is x+1 being impure, since it sends a request to the context to look up the value of x, whereas (λx. x+1) is pure because λ provides a handler for the request to look up the value of x, and the whole expression can be evaluated without sending anything more to the context.
> 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).
Creating a lexical closure (see 1:22:30 of the video) involves capturing the environment in which the closure was created. As in #1, the effectful part comes from a request to the context, which is collecting the free variables in the body of the lambda and building the closure. OTOH for dynamic closures you can create them without sending any request to the context, but when you apply it you have to request from the context.
The discussion on the Actor model is very relevant to understand what it means for expressions to send requests to contexts.
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 }
[[int -> total int]] = Z -> Z
[[int -> exn int]] = Z -> (Z + 1)
[[int -> st<h> int]] = (H,Z) -> (H,Z)
Now, non-termination as an effect makes sense: a function like "turing-machine" may diverge, so:
[[int -> div int]] = Z -> Z_\bot
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)
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.
while true { }
while i < 5 { i—-; }
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.
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.
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).
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.
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
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.)
Scala has a library for the difficult part, but I don't think it was very successful: https://github.com/atnos-org/eff
fun addRefs(
a : forall<h> ref<h,int>,
b : forall<h> ref<h,int>
) : total ()
{
a := 10;
b := 20;
return (!a + !b);
}
fun add-refs( a : ref<h,int>, b : ref<h,int> ) : st<h> int {
a := 10
b := 20
(!a + !b)
}
I believe the typesetting tool Madoko[1] is implemented in Koka, though in fairness Daan Leijen developed both Koka and Madoko.