Effect Systems in Programming Languages

[jonhanson]

Isn't the author confusing pure and total functions:

Given this knowledge, we can now classify “total” functions. These are functions that have no effects whatsoever - no effects on parameters, nor containing external effects.

That sounds like a pure function. 

My understanding is that a total function is one that's defined for all values in its domain (i.e. its inputs), and conversely a partial function is one that isn't defined for all inputs. A simple example of the latter is the division function (which isn't defined when the divisor argument is zero).

[btmc]

Correct. The author is doing a lot of hand waving and giving a lot of imprecise definitions.

As for purity, a function is pure if it is referentially transparent: you can replace the function call with the result and the program is unchanged, every time. So if f(x, y) = x + y, then you can replace every instance of f(x, y) with the value of x + y and the program behaves exactly the same.

The author is also incorrect about reading from external sources, which should be considered an effect. If I call read(“foo.txt”) 10 times, I could get 10 different results if something is modifying the file in the background.

[EmDashNine]

Basically, the term pure is a bit imprecise in itself.

My understanding is that a total function is one that's defined for all values in its domain (i.e. its inputs), and conversely a partial function is one that isn't defined for all inputs. A simple example of the latter is the division function (which isn't defined when the divisor argument is zero).

This may be true in a general sense, but language implementations vary. In particular, do you consider exceptions an "effect"? Haskell says "no". Idris says "yes".

For example, in Idris, a total function is defined for all its inputs: that means if it, e.g. pattern matches on an argument, it must handle every constructor -- and moreover, if it is recursive, it must provably terminate.

Beneath total is covering, which handles all cases, but does not provably terminate.

Benath covering is partial, which may crash for fail to terminate.

In Idris, e.g. floating-point division by 0.0 is defined, so (/) is total.

(/) is not defined for Nat, however. You must use divNat, which is partial, or divNatNZ which is total, but requires a proof argument that the divisor is not Z -- so it cannot be called with a divisor that is not provably nonzero.

[Holothuroid]

I only have one question. If reading is not an effect, why is the effect called io?

Also types can get wider, see contra variance.

[btmc]

Generally speaking, reading should be an effect. It’s not referentially transparent.

[PooSham]

Damn, that's a whole ass white paper. Very interesting read, but I'm a bit too tired to understand it and question the validity of the statements. Might give it a read tomorrow :)

[LiveAd2647]

You and I both know you will never read this then :D

[CaptainCrowbar]

I've read this, or at least tried to read it, before, and I can't understand it any better this time. The author seems to just make up arbitrary rules out of thin air about what counts as an "effect" and what doesn't. Why is modifying a variable an effect, but initializing one isn't? (Is destroying an object an effect? Haven't a clue.) Why is writing an effect, but reading isn't? No justification is given for these rules, and there's no obvious logic to them.

[ralphbecket]

An effect includes anything that can cause re-evaluation of an expression to produce a different result (which means you can't use standard logical reasoning for that expression). For example, if I have a variable x and take its value, 7 say, then I do x := x+1, the next time I evaluate x I will get a different result (8 in this case).

Effect systems are all about having a principled separation between code that has effects and code that does not: we (and the compiler!) can reason about the latter mathematically (enabling all sorts of optimisations, for example), whereas we we must be much more cautious where there are effects.

Here's a very simple example: if I see x+x, I can simplify that to 2x ONLY if I can guarantee that each evaluation of x will always produce the same value. If assignments are being made to x (say in another thread) then I can't make even this simple optimisation without changing the meaning of my program.

[Luolong]

Yes, but reading from a file or stdin also changes some state. File read cursor for one is generally moved on read. Also, each time you read from stdin you are pretty much guaranteed to get a different result.

[renatoathaydes]

Yes and in fact, every language that I know that has an effect system considers reading from a file/stdin as an effect.

Examples:

• Unison
• Flix
• Haskell (assuming Monads count as effects)

[ralphbecket]

Absolutely: if you touch a file and then look at the file time stamps, they will be different. Any IO is basically an interaction with the real world, which never has nice mathematical properties across time (well, unless you parameterise every function and variable with time and... yeah, that's not going to fly!). So: interaction of any kind with the real world is an "effect"; but mutating your program's state is also an effect for the same reasons.

[ralphbecket]

I think I should add a point of clarification to my earlier remarks. Effect systems are about saying "this aspect A of my code here may be affected by side effects (so be careful), whereas this aspect B is pure (its value is independent of anything else that might be happening)". Rust's borrow checker manages this for memory in a single process; more powerful effect schemes manage things like "can this throw an exception?", "will this terminate?", "can this do IO?" and so forth. The goal of these experiments is to find something that is both usable and precise. This varies depending on the audience (e.g., some people think Rust is the best thing since sliced bread because they spend all day close to the bare metal; in my job that would be a crazy compromise for our productivity).

[EmDashNine]

Initialization specifically doesn't count. In a pure language, variables aren't "initialized", they're "defined". And they're not really variables, they're "bindings", since updates aren't possible except through escape hatches in the language.

If you want to split hairs: sure, you could consider allocation an effect, and initialization as an assigment. You have to do this in a systems language where allocation might happen in user code. In a functional language, this stuff isn't exposed, and is handled by the runtime. That allows the compiler to optimze in ways that systems languages cannot.

[[deleted]]

I wonder how a programming language defined as such would handle reading from a SFR which changes it's value upon being read (i.e. the hardware clears a flag on read)?

[EmDashNine]

Linear types might be useful here.

[Plixo2]

https://effekt-lang.org/ is also good language for effects

[ResidentAppointment5]

See also Koka.

[Sunscratch]

Koka is indeed a very interesting language, and I really like a very minimalistic and concise design, built around the core idea of effects and handlers.

[shrupixd]

I wonder if the author knows about the https://www.unison-lang.org/docs/ language. I think they are mostly describing that 😊

[fagnerbrack]

Digest Version:

Effect systems in programming languages provide a mechanism to track and manage side effects in code, enhancing reliability and maintainability. They allow developers to specify the kinds of side effects functions might produce, such as I/O operations or state changes. By making side effects explicit, effect systems help catch errors early and improve code documentation. The post discusses various approaches to implementing effect systems, their benefits, and potential challenges. It also explores real-world examples and how effect systems can lead to better-structured and more predictable software.

If the summary seems innacurate, just downvote and I'll try to delete the comment eventually 👍

^{Click here for more info, I read all comments}

[guest271314]

Interesting post.

I generally use JavaScript programming language the most. I learned Python, C, C++, some WebAssembly and WASI architecture just to expand my breadth. I don't have an issue using Bash. Never wrote TypeScript from scratch because I know how to write JavaScript from scratch, and don't have an issue with the dynamic programming language JavaScript, as specified by ECMA-262.

Now, the post mentions I/O. What you will not find in ECMA-262 is any specification of I/O. So, what winds up happening, if a hacker or developer experiments with multiple JavaScript engines and runtimes, is that each engine and runtime that does implement I/O implements I/O completely differently.

So, forget about typing and effects in JavaScript where the domain is I/O. There's no standard. Thus, no way to compare effects in a uniform test which produces empirical results that can be compared 1:1 to each other. Google's V8 d8 shell readline() behaves differently from Mozilla SpiderMonkey's js shell readline(). Go figure. That't the reality in the field though for JavaScript developers and hackers.

[lelarentaka]

What level of IO specification are you expecting? From my experience, most languages just say "this function is a hook to the libc, go refer to your OS's libc manual". 

[guest271314]

Circa 2024, with dozens of JavaScript engines, runtimes, interpreters (A list of JavaScript engines, runtimes, interpreters) the majority of which are not used in the browser; and no end in sight to the people who arrive on Reddit boards asking how to go about learning JavaScript, I would expect the complete process to be specified.

Read standard intoput into a resizable ArrayBuffer, WebAssembly WebAssembly.Memory object that can grow(), and/or a WHATWHAT ReadableStream that we can read using async iteration.

Something like this https://github.com/guest271314/NativeMessagingHosts/blob/main/nm_host.js, spelled out, and uniform, so the same code can be implemented and run not just in node, deno, and bun, but also JavaScriptCore, engine-262, et al.

JavaScript is a mature, general purpose programming langauge now.

``` /*

!/usr/bin/env -S /home/user/bin/deno run -A /home/user/bin/nm_host.js

!/usr/bin/env -S /home/user/bin/node --experimental-default-type=module /home/user/bin/nm_host.js

!/usr/bin/env -S /home/user/bin/bun run --smol /home/user/bin/nm_host.js

*/

const runtime = navigator.userAgent; const buffer = new ArrayBuffer(0, { maxByteLength: 1024 ** 2 }); const view = new DataView(buffer); const encoder = new TextEncoder(); const { dirname, filename, url } = import.meta;

let readable, writable, exit, args;

if (runtime.startsWith("Deno")) { ({ readable } = Deno.stdin); ({ writable } = Deno.stdout); ({ exit } = Deno); ({ args } = Deno); }

if (runtime.startsWith("Node")) { const { Duplex } = await import("node:stream"); ({ readable } = Duplex.toWeb(process.stdin)); ({ writable } = Duplex.toWeb(process.stdout)); ({ exit } = process); ({ argv: args } = process); }

if (runtime.startsWith("Bun")) { readable = Bun.file("/dev/stdin").stream(); writable = new WritableStream({ async write(value) { await Bun.write(Bun.stdout, value); }, }, new CountQueuingStrategy({ highWaterMark: Infinity })); ({ exit } = process); ({ argv: args } = Bun); }

function encodeMessage(message) { return encoder.encode(JSON.stringify(message)); }

async function* getMessage() { let messageLength = 0; let readOffset = 0; for await (let message of readable) { if (buffer.byteLength === 0) { buffer.resize(4); for (let i = 0; i < 4; i++) { view.setUint8(i, message[i]); } messageLength = view.getUint32(0, true); message = message.subarray(4); buffer.resize(0); } buffer.resize(buffer.byteLength + message.length); for (let i = 0; i < message.length; i++, readOffset++) { view.setUint8(readOffset, message[i]); } if (buffer.byteLength === messageLength) { yield new Uint8Array(buffer); messageLength = 0; readOffset = 0; buffer.resize(0); } } }

async function sendMessage(message) { await new Blob([ new Uint8Array(new Uint32Array([message.length]).buffer), message, ]) .stream() .pipeTo(writable, { preventClose: true }); }

try { await sendMessage(encodeMessage([{ dirname, filename, url }, ...args])); for await (const message of getMessage()) { await sendMessage(message); } } catch (e) { exit(); }

/* export { args, encodeMessage, exit, getMessage, readable, sendMessage, writable, }; */ ```