The alloc effect signifies a function may allocate in a heap h.

An any type. Used for external calls.

The type of booleans has two inhabitants: Truestd/core/types/True: bool and Falsestd/core/types/False: bool.

Explicitly box values using the Boxstd/core/types/Box: forall<a> (unbox : a) -> box<a> constructor.

First-class constructor context (for tail recursion modulo cons (TRMC) optimization). See also samples/learn/contexts for further examples.

A unicode character. Characters are unicode codepoints. This is different from a unicode grapheme which represents a single displayed symbol and can consists of multiple codepoints due to combining characters and marks. (see also std/core/charstd/core/char and the std/text/unicodestd/text/unicode module).

A first-class constructor context where the hole is of the same type as the root of the structure.

The divergence effect: a divergent function may not terminate.

The predicate edivstd/core/types/ediv: (X, V, E) -> P<x,a,e> signifies that if the type a contains a reference to effect constant x then the effect e must contain the divergent effect (divstd/core/types/div: X). This constraint is generated for operations on first-class effects where code can diverge through operations.

The effect constructor extends an effect row with another effect. Usually written as <_|_>.

The choice type represents one of two possible types a or b. See also std/core/eitherstd/core/either.

A 32-bit IEEE 754 single precision floating point value. Provides currently no operations and currently only used for storage and for interaction with external code.

A 64-bit IEEE 754 double precision floating point value. See std/num/float64std/num/float64 for operations on float64std/core/types/float64: Vs.

The globalstd/core/types/global: H heap is a special heap constant to denote the global shared heap.

Handled effects are lifted to an atomic effect using the handledstd/core/types/handled: ((E, V) -> V) -> X type constructor All user defined effects are handledstd/core/types/handled: ((E, V) -> V) -> X since they require a handler to be dismissed. In contrast, some built-in effects, like divstd/core/types/div: X or ststd/core/types/st: H -> E do not require a handler as these are handled by the system. In particular, the runtime evidence vector only contains handledstd/core/types/handled: ((E, V) -> V) -> X (and handled1std/core/types/handled1: ((E, V) -> V) -> X) effects.

Linear effects are lifted to an atomic effect using the handled1std/core/types/handled1: ((E, V) -> V) -> X type constructor.

The predicate hdivstd/core/types/hdiv: (H, V, E) -> P<h,a,e> signifies that if the type a contains a reference to h, then the effect e must contain the divergent effect (divstd/core/types/div: X). This constraint is generated when reading from the heap (see !) and is necessary to catch cases where code can diverge by storing self referential functions in the heap.

An arbitrary precision signed integer. See std/core/intstd/core/int for integer operations.

A 16-bit signed integer (represented in two's complement). Provides no operations and used only for storage and interaction with external code.

A 32-bit signed integer (represented in two's complement). See the std/num/int32std/num/int32 module for operations on 32-bit integers.

A 64-bit signed integer (represented in two's complement). See the std/num/int64std/num/int64 module for operations on 64-bit integers.

A 8-bit signed integer (represented in two's complement). Provides no operations and used only for storage and interaction with external code.

A signed two's complement integer equal to an intptr_t in C, i.e. it has the same bit-size as a native pointer (void*). Provides no operations but is used mostly for interaction with external code. The Javascript backend uses int64 for this.

The type of lists, which can be either empty (Nilstd/core/types/Nil: forall<a> list<a>) or an element followed by a list (Consstd/core/types/Cons: forall<a> (head : a, tail : list<a>) -> list<a>). See std/core/liststd/core/list for operations on lists.

A local heap effect.

A local variable local-varstd/core/types/local-var: (H, V) -> V<s,a> points to a value of type a in local scope s.

The maybestd/core/types/maybe: V -> V type is used to represent either a value (Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>(x)) or Nothingstd/core/types/Nothing: forall<a> maybe<a>. This type is often used to represent values that can be null. See also std/core/maybestd/core/maybe.

The maybe2std/core/types/maybe2: (V, V) -> V type is used to represent either two values (Just2std/core/types/Just2: forall<a,b> (fst : a, snd : b) -> maybe2<a,b>(x,y)) or Nothing2std/core/types/Nothing2: forall<a,b> maybe2<a,b>. A type like maybe2std/core/types/maybe2: (V, V) -> V<a,b> can be used instead of maybestd/core/types/maybe: V -> V<(a,b)> to avoid boxing and heap allocating the tuple. See also std/core/maybe2std/core/maybe2.

The non-determinism effect.

Named effects are lifted to an atomic effect with the nhandledstd/core/types/nhandled: ((E, V) -> V) -> X type constructor. In contrast to handledstd/core/types/handled: ((E, V) -> V) -> X effects, these effects are not passed in the evidence vector.

Linear named effects are lifted to an atomic effect using the nhandled1std/core/types/nhandled1: ((E, V) -> V) -> X type constructor.

An enumeration to represent order: Ltstd/core/types/Lt: order, Eqstd/core/types/Eq: order, or Gtstd/core/types/Gt: order. See also std/core/orderstd/core/order.

Represent two elements in ascending order. This is used to allow comparison on elements to be used linearly for fip functions. See also std/core/orderstd/core/order.

A padding type pad. This is sometimes used for fbip programming to match up the size of constructors for reuse.

The read effect: signifies that a function may read from from heap h.

A reference refstd/core/types/ref: (H, V) -> V<h,a> points to a value of type a in heap h.

A signed two's complement integer equal to a signed size_t in C, i.e. it can hold the byte size of any object, in particular the maximum possible byte size of a vector or string. Provides no operations but is used mostly for interaction with external code. The Javascript backend uses int32 for this.

Stateful functions can manipulate heap h using allocations, reads and writes.

A string is a sequence of unicode character points (char). The encoding of a string is internal and there is no constant-time indexing of characters in a string. Use the sslice type for efficient matching and retrieving sub-strings from string. See std/core/stringstd/core/string and std/core/sslicestd/core/sslice for string operations.

The total effect represents the absence of any effect. Usually written as <>.

A pair of values a and b. Usually written as (x,y) (for types and terms).

A triple of values. Usually written as (x,y,z) (for types and terms).

A quadruple of values. Usually written as (a,b,c,d) (for types and terms).

A quintuple of values. Usually written as (a,b,c,d,e) (for types and terms).

The unit type unitstd/core/types/unit: V is inhabited by just a single value, namely Unitstd/core/types/Unit: (). Usually the type and constructor are written as (). See also the voidstd/core/types/void: V type and the boolstd/core/types/bool: V type.

The type of immutable polymorphic arrays is called vectorstd/core/types/vector: V -> V. See std/core/vectorstd/core/vector for vector operations.

The voidstd/core/types/void: V type is empty and has no constructors. See also the unitstd/core/types/unit: V unit type and the boolstd/core/types/bool: V type.

The write effect: signifies that a function may write to heap h.

Force lazy constructors.

The identity function returns its argument unchanged.

Prevent inlining an expression by passing it to keepstd/core/types/keep: forall<a> (x : a) -> a (which is a non-inlineable identity function).

Internal: if local mutation is unobservable, the localstd/core/types/local: H -> X effect can be erased by using the local-scopestd/core/types/local-scope: forall<a,e> (action : forall<h> () -> <local<h>|e> a) -> e a function. See also: State in Haskell, by Simon Peyton Jones and John Launchbury.

Mask the state effect. This is more convenient than masking each readstd/core/types/read: H -> X, writestd/core/types/write: H -> X, and allocstd/core/types/alloc: H -> X effect separately.

If a heap effect is unobservable, the heap effect can be erased by using the runstd/core/types/run: forall<e,a> (action : forall<h> () -> <alloc<h>,read<h>,write<h>|e> a) -> e a fun. See also: State in Haskell, by Simon Peyton Jones and John Launchbury.