Glossary

Action — Sequencing syntax for typed effectful computations.

Algebra — A structure centered on one carrier type.

Binder — A declaration that introduces a scoped name and type.

Coherence — The requirement that implicit evidence or representation selection have one valid intended choice.

Definitional equality — Equality established by permitted terminating normalization and substitution.

Effect row — A typed collection of effect installation requirements, possibly with an open tail.

Evidence — A typed value implementing a structure contract.

Handler — An interpretation of one effect installation.

Intrinsic — A compiler/provider implementation registered for a canonical typed declaration.

Pi type — A function type whose result may depend on its input.

Representation (repr) — A checked mapping between a semantic type and a storage type.

Resumption — The scoped continuation available to a resumable handler operation.

Row — An open or closed set of labeled fields/effects with constraints.

RuntimeCore — The immutable closed executable core shared by target providers.

Sigma type — A product whose later component may depend on an earlier value.

Stage-R — Closed typed elaboration before specialization and RuntimeCore.

Target — A typed environment in which an artifact can execute.

Target handle — A live runtime instance of a target profile.

Target profile — Compile-time evidence describing a target family.

Telescope — An ordered n-ary sequence of binders where later fields may depend on earlier fields.

Universe — A checked level classifying types and type constructors.