In my opinion, every effect system I come across makes unnecessary and clunky assumptions, such as:

• Assuming effects are only about some discrete concept in the language, such as control flow or exceptions etc. We want to be able to detect any behavior, and we want to be able to do so in imperative programs.
• Assuming effects have to be "labeled" or all declared up front. When we write a function, we can never have certainty we've predicted and exposed all the possible ways for people to be "alerted" about it. Sure we can label that it could throw an exception, but maybe someone will want to know it calls print, or writes to a file, or performs floating point arithmetic, or reads from a global variable, or uses a particular library.

My concept of Flow Effects is intended to avoid those unnecessary assumptions.

• Flow effects can be defined in terms of any of the other semantic primitives of the language, which can always be boiled down to calling functions/executing instructions, or reading/writing variables/registers/memory. This means flow effects are fully open-ended, and can be used to determine the presence or absence of any behavior that can be performed in the language, not just control flow concepts or asynchrony etc. In combination with full proof checking it would be possible to model any semantic pattern with complete precision.
• Flow effects don't have to be labeled at all, and even further aren't even checked or tracked in any way until a program makes actual assertions about an effect's presence or absence. For example: you can simply write a function that could possibly panic, reads from a global variable, prints to stdout, and makes a network request, and you don't have to annotate it any differently than any other function. Then if some caller needs to either prohibit or require any of those behaviors, it can enter a block that annotates those demands and only then will your function be checked in those ways. (This was directly inspired by the Typescript compiler's flow nodes concept (opens new window).)

You can think of Flow Effects almost like "hooks" in the type system, where all the primitive actions afforded by the language can be detected and have custom assertions placed over them.

Design sketch

Let me play around with some fully realized examples using a syntax I'm making up on the spot. This syntax I'm choosing is much more verbose for clarity's sake: if I were actually building this language I'd figure out the most elegant surface I could.

First we would need whatever syntax for the primitive effects, and a basic "effect naming" keyword effect.

// let's imagine there's some global `Runtime` symbol
// that contains all the "external" functions

// a keyword `calls`,
// and a `..` to say we don't care about the arguments
effect reads_file = calls Runtime.read_file(..)

// effects can be unioned together
effect anything_file =
	| calls Runtime.read_file(..)
	| calls Runtime.write_file(..)
	| calls Runtime.create_file(..)

// `reads` and `writes` can reason about
// global/external variables
GLOBAL_THING: int = 0
effect needs_global =
	| reads GLOBAL_THING
	| writes GLOBAL_THING

// maybe a wildcard on the effect kind itself?
effect needs_global = * GLOBAL_THING

Then syntax to demand either the presence or absence of an effect. Some of these examples are lame without liquid typing which I'll talk about in a second.

// % is just a "separator" from a type and the effects
type SafeIntFn = (int) -> int % !needs_global

fn my_func(f: SafeIntFn) -> int:
	// when I call `f` I am guaranteed
	// the absence of needs_global
	return f()

// of course can be inlined
fn my_func(f: (int) -> int % !needs_global) -> int:
	return f()

// directly annotating a function to assert
// that this calls effect is present
% calls some_func(..)
fn main(i: int) -> int:
	...

// the above is in "decorator style",
// but what about placing it on the return type?
fn main(i: int) -> int % calls some_func(..):
	...

// that would allow discriminating the presence/absence of effects
// based on the return type
// this only asserts the calls if "unit" is returned
fn main(i: int) -> () % calls some_func(..) | int:
	...

GLOBAL_VALUE = 0
fn main():
	global_value_before = GLOBAL_VALUE
	// an "assertion block"
	% !writes GLOBAL_VALUE:
		... do things ...

	// this assertion is guaranteed to succeed
	assert GLOBAL_VALUE == global_value_before

	// you could think of assertion blocks almost like
	// type-level inline tests

It also could be convenient to allow these "effect assertions" at the compiler cli level, for example allowing specifying them on the command line (with the equivalent of cargo build --demand '!anything_file' --demand 'yes_network') or in the project configuration (with the equivalent of Cargo.toml).

An easy thing to add is simple "wrapping cancellation", meaning allowing for an effect to be removed if it's contained within some other effect. As a trite example, say you only wanted to allow a print function to be called by some certain log function. Without anything like cancellation this would be impossible, since a simple !calls print(..) would also reject the usage in the log function.

effect prints =
	calls print(..)
canceled by
	calls log(..)

Flow effects gain their full power in conjunction with liquid types (opens new window) to constrain or narrow the actual data inputs/outputs of called functions or read/written data.

// here I'm assuming the "asserted types" & syntax
effect reads_passwd =
	calls Runtime.read_file(_ & == "/etc/passwd", ..)

// literals could be used to match more tersely
effect reads_passwd =
	calls Runtime.read_file("/etc/passwd", ..)

// effects can of course be generic/parameterized
// open design question of how to accept open-ended patterns
// (as higher order functions?)
effect reads_disallowed(allowed: str) =
	calls Runtime.read_file(_ & != allowed, ..)

effect divides_zero = calls div (_, 0)

effect sets_counter_to_odd_value =
	writes COUNTER <- int & .mod(2) == 1

And of course in the presence of liquid typing we could also have more typical "requires/ensures" concepts.

GLOBAL_VALUE: null | int = null

requires GLOBAL_VALUE == null
ensures GLOBAL_VALUE != null
fn init_func():
	GLOBAL_VALUE = 0
// init_func would have inferred effect `writes GLOBAL_VALUE`

requires GLOBAL_VALUE != null
fn inc_global():
	GLOBAL_VALUE += 1

fn main():
	inc_global() // compiler error! need init

	init_func() // okay so far...
	init_func() // compiler error! redundant

	inc_global() // finally alright

Instantaneous vs attached effects

This way I've defined flow effects makes them necessarily about instantaneous actions, things like function calls or reads or writes, which means these effects are inherently "free-floating" and not "attached" to data, but rather attached to code paths. This doesn't cover lots of things that people often think of as effects, like data that was created in a non-deterministic way, or allocated memory that creates an obligation to deallocate that memory. I think this division is okay, because data-attached concepts are more cleanly modeled as linear obligations (opens new window) or ghost state (opens new window) on those data structures.

It seems perfectly possible for these two concepts to flow into each other: doing (or failing to do) certain operations on data with certain ghost state could generate instantaneous effects at certain points in the program; and creating data using functions that match instantaneous effects could create ghost state attached to that data. I'm not exactly sure what a coherent relationship would be, and I'm going to think about it.

Possibilities

Lots of new abilities would be unlocked by Flow Effects, including making things like capability systems (opens new window) at the type-level.

Here some of the top things I'd like to be able to assert about my programs:

• It's impossible to block your async executor (opens new window).
• It's impossible for any network requests to be made to any hosts you haven't allowed.
• It's impossible for any files to be read or written that you haven't interactively allowed.
• It's impossible for any mutations to be made to your database.
• It's impossible for any arbitrary code from inputs to be executed.
• It's impossible to future lock (opens new window) or deadlock in any way.
• It's impossible for the program to print to stdout.
• If the program can't find all the files it will need, it will terminate with a particular error message.
• The program will always terminate.
• After the program successfully runs, a particular file will exist with particular contents.