Skip to content
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
70 changes: 2 additions & 68 deletions src/primitive-effects.md
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
## Primitive Effects

> **Note:** This page is slightly updated and pending a rewrite.

Flix comes with a collection of pre-defined primitive effects. Unlike algebraic
and heap effects, primitive effects cannot be handled and never go out of scope.
A primitive effect represents a side-effect that happens on the machine. It
Expand All @@ -25,75 +27,7 @@ is to say, once you have tainted yourself with impurity, you remain tainted.

### The Other Primitive Effects

> **Note:** As of Flix 0.65.0 we are making changes to the primitive effects,
> hence the text below may be slightly outdated.

In addition to the all-important `IO` effect, Flix has a small collection of
pre-defined primitive effects. The point of these primitive effects is to
provide more information about the specific actions a function can take. Except
for the `NonDet` effect, all of the effects below always come together with the `IO`
effect.

- **Env**: The `Env` effect represents actions that involve access to
information about the environment, including information from the operating
system (e.g., the name of the current user, the current working directory, and
so on), as well as information about the hardware (e.g., the number of
processors in the machine, the total amount of memory, and so on).

- **Exec**: The `Exec` effect represents actions that involve process creation
(i.e., spawning new processes that run outside the JVM), including using
`System.exec`, the `Process` and `ProcessBuilder` classes, and dynamic library
loading.

- **FsRead**: The `FsRead` effect represents actions that read from the file
system — for example, reading a file, reading its meta-data, or listing
the contents of a directory.

- **FsWrite**: The `FsWrite` effect represents actions that write to the file
system — for example, creating a file, writing a file, or deleting a
file.

- **Net**: The `Net` effect represents actions that involve network access
— for example, binding to a local port, connecting to a remote socket,
or DNS resolution.

- **NonDet**: The `NonDet` effect represents an almost pure computation. For
example, a function that flips a coin is virtually pure; it has no
side-effects. Yet, it may return different results, even when given the same
arguments.

- **Sys**: The `Sys` effect represents actions that interact with the JVM
— for example, using the `Runtime` and `System` classes, class loaders,
or reflection.

All of the above effects, except for the `NonDet` effect, always occur together
with the `IO` effect. In particular, they capture a more precise aspect of the
`IO` effect. For example, from a security point-of-view, it seems reasonable
that a web server library should have the `FsRead` and `Net` work effects, but
it would be worrying if it had the `FsWrite` and `Sys` effects. As another
example, it seems reasonable that a logging library would have the `FsWrite`
effect, but it would be a cause for concern if it also had the `Exec` and `Net`
effects.

The above effects represent dangerous actions except for `IO`, `Env`, and
`NonDet`, which are relatively harmless. `Exec` allows arbitrary process
execution, `FsRead` can be used to access sensitive data, `FsWrite` can be used
to trash the filesystem, `Net` can be used to exfiltrate data, and `Sys` via
reflection allows access to all of the previous. We should always be suspicious
if unknown or untrusted code uses any of these effects.

The primitive effects are mostly disjoint, but not entirely. For example, we can
use the `Exec` effect to indirectly gain access to the file system. The `FsRead`
effect may allow us to access a mounted network drive, a form of network access.
Ultimately, whether one effect can emulate another depends on what side channels
the underlying operating system allows. The point of the effect system is that
if a function does not have the `FsWrite` effect, it cannot write to the file
system using the ordinary file APIs available on the JVM.

### Where do Primitive Effects Come From?

The Flix compiler ships with a built-in database that maps classes,
constructors, and methods in the Java Class Library to primitive effects. For
example, the database assigns the `Exec` effects to every constructor and method
in the `java.lang.Process`, `java.lang.ProcessBuilder`, and
`java.lang.ProcessHandle` classes.