Effects

Effects

Hydra's effect<t> type constructor represents an effectful computation which, when interpreted by a host application, may perform host interactions and produce a value of type t.

The effect constructor makes host interaction visible in the type of a term. This lets Hydra distinguish pure terms from terms which describe effects.

Motivation

Hydra is built around pure, typed terms. Hidden impure primitives such as:

readFile : string -> string

would not be consistent with that design. The type says the function is pure, even though evaluating it depends on external state and may fail for reasons outside Hydra's data model.

Effectful operations instead return effect<t>:

readFile : FilePath -> effect<either<FileError, binary>>
writeFile : FilePath -> binary -> effect<either<FileError, unit>>

The effect is explicit. Code which consumes the result must sequence the effect rather than treating it as an ordinary pure value. Recoverable failures are explicit in the result type, just as they are in pure Hydra code.

The effect type constructor

effect<t> is a core Type grammar constructor, analogous to optional<t>, either<l, r>, and list<t>.

Examples:

effect<string>
effect<unit>
effect<boolean>
effect<list<string>>

The constructor is effect<t>, part of the type grammar, rather than a named type such as Effect<t> defined in a model module. This follows the same precedent that replaced Hydra's old named Flow monad with the core either<l, r>: an abstraction foundational enough to appear throughout the kernel and in primitive signatures is best represented as a core type constructor. For the general convention on when to prefer a core constructor over a named type in primitive signatures, see Adding primitives § Prefer core type constructors.

Standard combinators

The hydra.lib.effects module provides the standard combinators for working with effects. It is analogous to modules such as hydra.lib.optionals and hydra.lib.eithers.

The primitive set is:

pure : a -> effect<a>

map : (a -> b) -> effect<a> -> effect<b>

bind : effect<a> -> (a -> effect<b>) -> effect<b>

apply : effect<(a -> b)> -> effect<a> -> effect<b>

compose : (a -> effect<b>) -> (b -> effect<c>) -> a -> effect<c>

foldl : (a -> b -> effect<a>) -> a -> list<b> -> effect<a>

mapList : (a -> effect<b>) -> list<a> -> effect<list<b>>

mapOptional : (a -> effect<b>) -> optional<a> -> effect<optional<b>>

pure lifts a pure value into an effect. map transforms the result of an effect. bind sequences effects, passing the first result to a function which produces the next effect. The other combinators follow patterns already used by libraries such as hydra.lib.optionals, hydra.lib.eithers, and hydra.lib.lists. foldl and mapList sequence list elements from left to right. There is no fail primitive in this model.

Failure

effect<t> does not have a separate Hydra-level failure channel. By default, effects are not allowed to fail as Hydra values. An effect is allowed to produce a failure value only when its result type says so.

For example, a file read which may report a structured file error should have a type such as:

readFile : FilePath -> effect<either<FileError, binary>>

Then the effect itself produces an either<FileError, binary>. The left case is an ordinary Hydra value, not a hidden host exception.

This avoids having two incompatible error mechanisms, such as an unstructured string-based fail in hydra.lib.effects plus structured either<e, t> results in domain-specific libraries.

Host interpretation can still fail catastrophically or operationally, for example because a host implementation is missing or an external system crashes. Those are host/application failures at the execution boundary, not Hydra values constructed by effect<t>.

Domain-specific effect libraries

Domain libraries expose effectful operations by returning effect<t>. The first such library is hydra.lib.files, which provides file-system operations:

appendFile      : FilePath -> binary -> effect<either<FileError, unit>>
copy            : boolean -> FilePath -> FilePath -> effect<either<FileError, unit>>
createDirectory : boolean -> FilePath -> effect<either<FileError, unit>>
exists          : FilePath -> effect<either<FileError, boolean>>
listDirectory   : FilePath -> effect<either<FileError, list<FilePath>>>
readFile        : FilePath -> effect<either<FileError, binary>>
removeDirectory : boolean -> FilePath -> effect<either<FileError, unit>>
removeFile      : FilePath -> effect<either<FileError, unit>>
rename          : FilePath -> FilePath -> effect<either<FileError, unit>>
status          : FilePath -> effect<either<FileError, FileStatus>>
writeFile       : FilePath -> binary -> effect<either<FileError, unit>>

The boolean argument to copy, createDirectory, and removeDirectory selects recursive behavior. File contents are binary (not string): reads and writes move raw bytes, so the host moves the data without imposing a text encoding. To work with text, decode/encode explicitly with hydra.lib.text (see below).

Other effectful libraries may cover console I/O, streams, clocks, randomness, networking, databases, or application-specific host capabilities.

Supporting types: hydra.file and hydra.time

hydra.lib.files is built on a small POSIX-based type vocabulary in hydra.file (and hydra.time), so signatures stay self-describing rather than using bare strings and integers:

• FilePath — a host file-system path (a POSIX pathname, XBD §3.254), modeled as a wrap of string.
• FileType — an enumeration of POSIX file types from <sys/stat.h> (block, character, directory, fifo, regular, link, socket).
• FileStatus — the subset of POSIX struct stat Hydra exposes: fileType, size (bytes), modificationTime, and the optional accessTime and statusChangeTime.
• Timespec (in hydra.time) — the POSIX struct timespec: seconds (int64, signed, since the Unix Epoch) and nanoseconds (uint32, in [0, 999999999]). File timestamps use this type.

FileError is the structured error type returned in the left branch of file results (e.g. not-found, already-exists, permission-denied, invalid-path, other).

Text codecs: hydra.lib.text

Because file contents are binary, hydra.lib.text provides the bridge to and from text:

decodeUtf8 : binary -> either<string, string>
encodeUtf8 : string -> binary

decodeUtf8 returns left with a host-provided message when the bytes are not valid UTF-8, and right with the decoded text otherwise. encodeUtf8 is total: every Hydra string is valid Unicode and always encodes.

Sequencing

Effects are sequenced with bind.

For example:

bind
  (readFile (FilePath "input.txt"))
  (\result -> either
    (\err -> pure (left err))
    (\contents -> writeFile (FilePath "output.txt") contents)
    result)

has type:

effect<either<FileError, unit>>

The type remains effectful. The read must happen before the write because the write is constructed by the continuation passed to bind. The possible file error is also explicit in the result type. Here contents is the binary produced by the read, passed straight to the write; a program that needed the bytes as text would decode them with hydra.lib.text.decodeUtf8 first.

Execution boundary

This design does not include a primitive such as:

perform : effect<a> -> a

as an ordinary Hydra term-level operation. Such a primitive would collapse an effectful computation into a plain value and would resemble the unsafe or partial primitives Hydra avoids.

Instead, execution of an effect is a host or application boundary. A Hydra program may expose an entry point such as:

main : effect<unit>

and the host application decides how to interpret that effect. This is analogous to running a program, not to calling a pure function inside Hydra.

Safety and totality

Hydra avoids primitives which hide failure or partiality. The strictness and precision guidance states that Hydra should fail immediately with informative errors and should not silently recover by returning defaults. This principle motivated #201, which removed unsafe primitives such as hydra.lib.maybes.fromJust.

Effects follow the same discipline. Effectful operations expose effectfulness in their result type. Recoverable failures are represented with ordinary Hydra types such as either<e, t>, rather than being hidden behind a pure type or an untyped effect-level failure channel.

Testing effectful operations

Hydra's common test suite can exercise effectful operations, not just pure ones. Alongside the usual string-comparison test case, there is an effectful test case whose actual is an effect<string> term: the test runner in each host executes the effect (performing real host interactions such as file I/O) and compares the produced string to the expected value.

Because effects cannot be reduced by Hydra's pure evaluator, an effectful test case is only ever compiled to native target code and run — never routed through the interpreter. File-based test cases operate within a temporary directory that the runner guarantees is empty before each such case (currently the fixed path /tmp/hydra-testing, assuming a *nix host). The same test cases run across every host that implements the effect libraries, validating the implementations uniformly. See the contributor-facing test suite architecture for how these cases are authored and mapped into each target.

Open questions

• Which additional effect libraries (console I/O, clocks, randomness, networking) should the standard library grow next?
• What conventions should hosts use for discovering and running effect<unit> entry points?
• Should the effectful-test temporary directory become configurable (it is the fixed /tmp/hydra-testing today)?