tulam Language Reference
Contents
- Status and Authority
- Source Files and Modules
- Lexical Structure
- Universes and Type Expressions
- Data Type Declarations
- Existential Values
- Functions and Values
- Local Bindings and Control Flow
- Structures, Algebras, and Morphisms
- Laws
- Primitive Types, Intrinsics, and Representations
- Classes and Objects
- Effects and Handlers
- Actions
- Explicit Laziness
- Targets and Placement
- Concurrency and Mutation
- Interop
- Static Semantics
- Desugaring Summary
- Canonical Grammar
- Quick Reference
1. Status and Authority
This is the normative specification of tulam’s surface language. Parser, formatter, diagnostics, examples, tests, and documentation must follow it.
The document specifies the intended language, including features not yet fully implemented. Implementation status belongs only in ImplementationPlan.md. An implementation quirk does not change this specification.
Core semantics are defined in LanguageDesign.md. Abstract target semantics are defined in TargetDesign.md. If a focused design document proposes different syntax, this reference wins.
1.1 Change-Control Rule
Changing this surface contract requires the user’s explicit approval of the specific programmer-visible change before any normative text, grammar, implementation, example, syntax-highlighting rule, or conformance expectation is updated to adopt it. A general request to continue implementation or proceed with a phase is not approval for an unlisted language change, and silence is not approval.
This requirement applies to lexical syntax, grammar, operators and precedence, desugaring, declaration and expression forms, accepted/rejected-program rules, typing, effects, evidence, coherence, inference and resolution defaults, and all other programmer-visible semantics. Implementing an existing rule in this reference is not a surface-language change. If an existing rule is ambiguous, incomplete, contradictory, or cannot be implemented as written, work on that decision must stop until the user explicitly approves a clarified contract.
1.2 Scope and Reading This Reference
Sections 2 through 19 define the programmer-visible language. Section 20 lists required desugarings, Section 21 collects the canonical grammar, and Section 22 is a non-exhaustive lookup table. The prose and examples remain normative when the compact grammar omits a semantic restriction such as coherence, exhaustiveness, or relevance.
Parser acceptance alone does not define tulam. A compatibility or transitional form that is not described by this reference is not available to portable programs and must not be emitted by formatters, documentation, or new source. Known implementation gaps are inventoried in tests/conformance/catalog.json and their delivery phases are owned by ImplementationPlan.md. The LLVM native provider is the current reference execution target; front-end acceptance and rejection remain authoritative for non-execution rules.
2. Source Files and Modules
tulam source files use the .tl extension. A file contains an optional module header, imports, an optional export list and default target, followed by declarations.
module Math.Matrix;
import Core;
import Math.Algebra (Field, zero);
import Backend.API hiding (unsafeCall);
export (Matrix, multiply, identity);
default target compute;
type Matrix(a:Type, rows:Nat, cols:Nat) = ...;
function multiply(...) : ... = ...;Module names are dot-separated uppercase identifiers. Imports are explicit; transitive dependencies do not enter lexical scope automatically.
module_decl = "module", module_name, ";" ;
import_decl = "import", module_name, import_filter?, target_qualifier?, ";" ;
import_filter = "(", name, { ",", name }, ")"
| "hiding", "(", name, { ",", name }, ")" ;
target_qualifier = "target", target_ref ;
export_decl = "export", "(", name, { ",", name }, ")", ";" ;
open Module.Name; imports all exported names unqualified. Prefer explicit imports in public libraries.
private prevents a declaration from being exported. opaque type exports a type identity while hiding its constructors.
3. Lexical Structure
3.1 Comments
// line comment
/* block comment */
/// documentation comment for the following declarationBlock comments do not nest.
3.2 Identifiers
- Type, constructor, class, and module components begin with an uppercase letter:
Nat,Just,Text.Buffer. - Functions, values, fields, variables, instances tags, and policies begin with a lowercase letter or underscore:
map,x,compute. - Identifiers may contain letters, digits, underscores, apostrophes, and a trailing
#where a legacy/compiler binding requires it. - Symbolic operators are declared as parenthesized function names:
function (+)(x,y) = ....
Self is a conventional compiler-recognized type name inside a class. on is a contextual word recognized only in declaration headers, and with is a contextual word after a handle expression. resume is a handler-scoped binding, not a globally reserved word. return and finally are contextual handler-clause names; they remain ordinary identifiers everywhere else.
3.3 Keywords
The following ASCII words are reserved:
abstract action algebra as bridge class default derive deriving effect else
exists export extends extern final fn forall function handle handler hiding if
implements import in infix infixl infixr instance intrinsic invariant law let
match module morphism opaque open override primitive private repr requires
sealed static structure super target then trait type unpack value where
The Unicode spellings for universal and existential quantification are also reserved. record, realm, runOn, runAt, marshal, portable, policy, lazy, and force are not keywords.
3.4 Separators
The separator rule is uniform:
- Semicolons separate declarations or sequential statements.
- Commas separate data: arguments, tuple components, fields, constraints, and pattern components.
- A trailing semicolon is allowed in a declaration block.
algebra PairLike(p:Type1) = {
function first(x:p(a,b)) : a;
function second(x:p(a,b)) : b;
};
let { x = 1; y = 2; z = x + y } in z3.5 Literals
The language has integer, floating-point, character, string, list, tuple, and vector literals:
42
3.14159
'x'
"hello\n"
[1, 2, 3]
{1, True, "three"}
{x = 1, y = 2}
<1.0, 2.0, 3.0, 4.0>Numeric and string literals are elaborated through expected type and standard literal algebras. Int, Float64, and the standard string type are defaults only when context does not determine a more specific type.
Character and string source text is Unicode. A character literal denotes exactly one Unicode scalar value; surrogate code points are not values of Char. The closed escape set for character and string literals is \\, \", \', \0, \n, \r, \t, and \u{HEX}. A Unicode escape contains one to six hexadecimal digits and must denote a scalar in 0 through 10FFFF, excluding D800 through DFFF. Unknown escapes, malformed escapes, literal line breaks, and invalid scalar escapes are lexical errors.
4. Universes and Type Expressions
4.1 Universes
Type
Type1
Type2Type is U(0), Type1 is U(1), and so on. Universes are cumulative. Level-polymorphic binders may be inferred; explicit level syntax is reserved for a later revision and is not currently part of the surface grammar.
4.2 Type application
Type constructors use ordinary application syntax:
Maybe(Int)
Either(String, Int)
Matrix(Float32, rows, cols)Types and terms share the same expression language, subject to universe and phase checking.
4.3 Pi types
Int -> Bool
Int -> Int -> Int
(n:Nat) -> Vec(a,n)
(n:Nat) -> (m:Nat) -> Matrix(a,n,m)-> associates to the right. (x:A) -> B(x) binds the term x in the codomain. Application substitutes the actual argument term into the codomain.
Universal syntax introduces implicit Pi binders:
forall a. a -> a
forall (a:Type)(n:Nat). Vec(a,n) -> NatThe Unicode universal-quantifier spelling is equivalent.
4.4 Sigma types
Int * Bool
(n:Nat) * Vec(a,n)
(t:Type) * TargetHandle(t)(x:A) * B(x) binds x in the second component. Every product chain is one canonical n-ary telescope in the typed language and at runtime. The compiler does not encode A * B * C as A * (B * C) or (A * B) * C.
Parentheses and tuple values can request actual nesting. Thus {a,b,c} is one three-field tuple while {a,{b,c}} is a two-field tuple whose second field is a two-field tuple. This distinction is preserved by checking, optimization, layout, reflection, and debugging.
Existential syntax hides Sigma witnesses:
exists (a:Type). { value:a, show:a -> String }The Unicode existential-quantifier spelling is equivalent.
4.5 Sum and product type operators
In type expressions, + forms a sum and * forms a product. In a type declaration body, the same tokens separate constructors and fields as described in Section 5.
4.6 Structural record types
{ name:String, age:Int }
{ name:String, ..r }Named record types are structurally typed and support open row tails. Nominal record-like data is declared with type.
4.7 Effect types
Eff {} Int
Eff { console:Console } Unit
Eff { state:State(s), console:Console | e } aEff {} a is observationally pure and can be written as a where no explicit effect-polymorphic form is required.
4.8 Type precedence
From loosest to tightest:
forallandexists;->(right associative);+;*;- type application, projection, and parentheses.
5. Data Type Declarations
5.1 Empty and enumeration types
type Void;
type Bool = True + False;
type Ordering = Less + Equal + Greater;Void has no constructors. Nullary constructors have no payload.
5.2 Sum types with fields
type Maybe(a:Type) =
Nothing
+ Just * value:a;
type Either(a:Type,b:Type) =
Left * value:a
+ Right * value:b;+ separates constructors. * introduces fields belonging to the preceding constructor. Fields are comma-free because * is part of the type declaration grammar; function and tuple data still use commas.
5.3 Implicit-constructor types
When a type body begins with a lowercase field, the compiler creates one constructor with the same name as the type:
type Point = x:Float64 * y:Float64;
// Constructor: Point(x:Float64, y:Float64)The record keyword is not part of tulam.
5.4 Field spread
type Point3D = ..Point * z:Float64;Spread copies the visible fields of the named nominal data type in declaration order. Field collisions are errors. Spread is layout composition, not class inheritance or structural row extension.
5.5 Dependent fields
Later fields may depend on earlier fields:
type SizedVector(a:Type) =
size:Nat * values:Vec(a,size);Construction checks the telescope from left to right. Projection substitutes preceding field values into later field types.
5.6 GADTs
A constructor may specify its result type:
type Vec(a:Type,n:Nat) =
VNil : Vec(a,Z)
+ VCons * head:a * tail:Vec(a,n) : Vec(a,Succ(n));Pattern matching refines indices according to the selected constructor.
5.7 Deriving
type Color = Red + Green + Blue deriving Eq, Show;Each listed algebra must supply a valid derive definition. Derivation creates ordinary checked instances and does not bypass laws or coherence.
5.8 Computed data declarations
A data body may be a compile-time expression returning a typed DataCode:
type Source(a:Type) = None + Some * item:a;
function schema(code:DataCode(Unit, Z)) : DataCode(Unit, Z) =
renameConstructor(
renameConstructor(renameDataType(code, "Generated"),
"None", "Absent"),
"Some", "Present");
type Generated(a:Type) = schema(dataCode(reflect(Source(a))));The body begins with an ordinary lowercase function application and must evaluate at compile time to DataCode. The result must have the declared type name, parameter count, valid scope indices, and universe level. The computation is pure and target-neutral: it cannot perform effects, inspect target layout, call foreign code, use runtime reflection, or rely on unrestricted recursion.
After evaluation, the generated declaration is checked exactly like a written data declaration, including constructor validity, positivity, coverage, interfaces, deriving, and target compilation. Compile-time reflection values cannot escape into executable code.
5.9 Construction
Constructors use positional application or named fields:
Just(42)
Point(1.0, 2.0)
Point { x = 1.0, y = 2.0 }Named construction checks every required field exactly once and is insensitive to source field order. A missing, duplicate, or unknown field is a static error.
5.10 Tuple and record values
{1, True}
{name = "Ada", age = 36}Positional braces produce tuple/telescope values. Named braces produce structural record values. Both are canonical n-ary telescopes and use flat runtime layout. Field names affect projection and structural compatibility, not whether a value is represented as a tuple.
5.11 Record update and projection
point.x
point { x = point.x + 1.0 }
triple.0Update produces a new value unless the type and effect explicitly describe mutation. A labelled telescope field is projected by its label. An anonymous tuple field is projected by its zero-based numeric position. Projection never changes or recursively reassociates tuple structure.
6. Existential Values
6.1 Introduction
No pack keyword is needed. An expected existential type guides witness inference:
type Showable = exists (a:Type).
{ value:a, display:a -> String };
value item : Showable =
{ value = 42, display = showInt };If the witness cannot be inferred uniquely, the programmer supplies a more specific type annotation on the value or a component. Existential construction never relies on an unchecked dynamic cast.
6.2 Elimination
unpack item as (a, x) in x.display(x.value)a is a fresh rigid type within the body and x is the payload at that witness. The result type must not mention a, and values whose types mention a cannot escape their scope.
Field access may implicitly open an existential only when the complete expression can be checked with the same skolem/escape rule. unpack is the canonical explicit form.
7. Functions and Values
7.1 Named functions
function add(x:Int, y:Int) : Int = x + y;
function replicate(n:Nat, x:a) : Vec(a,n) = ...;Parameter annotations and the return annotation may be inferred when the result remains unambiguous and does not weaken a public interface.
7.2 Implicit parameters
Square brackets introduce implicit parameters:
function id[a:Type](x:a) : a = x;Implicit arguments are supplied by elaboration or explicitly through the corresponding advanced application form. Type-only implicit arguments are normally erased.
7.3 Constraints
function maximum(xs:c(a)) : Maybe(a)
requires Foldable(c), Ord(a) = ...;requires requests coherent implicit structure evidence. Constraints are checked at the call site after type/value substitution. Missing or ambiguous evidence is a compile error.
7.4 Placement clause
function multiply(a:Matrix(f,m,k), b:Matrix(f,k,n)) : Matrix(f,m,n)
requires Field(f)
on compute = ...;The canonical clause order is return type, requires, then on. on accepts a pure closed TargetPolicy expression and is declaration metadata, not part of the Pi type. See Section 16.
7.5 Anonymous functions
fn(x) = x + 1
fn(x:Int, y:Int) : Int = x + y
fn(x) = match | Nothing -> 0 | Just * value -> valuefn mirrors named function parameter and return syntax. Anonymous functions do not carry placement clauses; their containing declaration is planned as a unit unless the compiler proves a legal split.
7.6 Values
value answer : Int = 42;
value inferred = 40;
value computed : Int = inferred + 2;
value increment : Int -> Int = fn(x:Int) : Int = x + 1;Inside structures and instances, value declares a required or supplied constant. At top level it declares an immutable binding. An ordinary top-level value may infer its type from its initializer. A reference uses the bound value directly (computed, not computed()), including from another top-level value or through a higher-order function. Implementations may normalize, inline, share, or emit storage for the binding only when that preserves these value semantics.
An intrinsic constant uses the same declaration form:
value machineEpsilon : Float64 = intrinsic;
instance Floating(Float64) = {
value pi = intrinsic
};A top-level intrinsic value must state its type. An intrinsic value supplied by an instance may omit the annotation when its type is inherited unambiguously from the matching structure member. Intrinsic values are pure constants: an Eff type is rejected. Target-dependent or effectful retrieval is expressed by an intrinsic function or action, not by a value.
7.7 Application and operators
f(x, y)
(+)(x, y)
x + yApplication binds more tightly than infix operators. User-defined operator fixity is declared with:
infixl 6 (+);
infixr 5 (++);
infix 4 (==);Precedence is 0 through 9. Unknown operators default to left-associative precedence 9 only in interactive recovery; published modules should declare non-standard fixity.
8. Local Bindings and Control Flow
8.1 Let expressions
let x = expression in body
let {
x = 1;
double(n:Int) : Int = n * 2;
y = double(x)
} in x + yBlock bindings are sequential: a later binding sees all earlier bindings. A local function may optionally repeat the function keyword.
8.2 Conditionals
if condition then whenTrue else whenFalseThe condition has type Bool; both branches check against one result type. Conditionals desugar to pattern matching on Bool.
8.3 Pattern matching
match value
| Nothing -> fallback
| Just * x -> use(x)Function-body form:
function length(xs:List(a)) : Nat = match
| Nil -> Z
| Cons * head * tail -> Succ(length(tail));Patterns include literals, variables, wildcards, constructors, tuples, and named fields. Constructor field syntax mirrors declarations:
Point { x = px, y = py }Matches must be exhaustive unless the result type/effect explicitly represents failure. Redundant cases are diagnosed. Sealed class hierarchies participate in exhaustiveness; open class hierarchies require a fallback.
8.4 Expression annotation
expression : TypeAnnotations guide checking and existential witness inference. They do not cast.
9. Structures, Algebras, and Morphisms
9.1 General structure
structure Hashes(hash:Type, value:Type) = {
function hash(x:value) : hash
};structure is the general evidence contract and may have any number of type or value parameters.
9.2 Algebra and trait
algebra Monoid(a:Type) extends Semigroup(a) = {
value empty : a;
law leftIdentity(x:a) = combine(empty, x) === x;
law rightIdentity(x:a) = combine(x, empty) === x
};trait is an exact surface alias for algebra. An algebra is a structure centered on one carrier; the compiler validates that use.
9.3 Morphism and bridge
bridge Iso(a:Type,b:Type) = {
function convert(x:a) : b;
function unconvert(x:b) : a;
law roundTripA(x:a) = unconvert(convert(x)) === x;
law roundTripB(x:b) = convert(unconvert(x)) === x
};morphism and bridge are exact aliases. They identify directional relationships and do not imply automatic global composition.
9.4 Extends and requires
algebra Group(a:Type) extends Monoid(a) = { ... };
structure OrderedCollection(c:Type1,a:Type)
requires Ord(a) = { ... };extends inherits members and laws. Multiple parents are allowed for structures when member resolution is coherent. requires adds evidence needed to construct an instance.
9.5 Instances
instance Monoid(List(a)) requires Monoid(a) = {
value empty = Nil;
function combine(xs, ys) = append(xs, ys)
};
instance Additive(Int) = intrinsic;
instance Show(MyData) = derive;
instance Format(Date) as iso8601 = { ... };Named instance tags disambiguate intentional alternatives. Unnamed implicit resolution must be coherent in lexical and target context.
9.6 Derive blocks
An algebra can define checked derivation logic:
algebra Show(a:Type) = {
function show(x:a) : String;
derive {
function show(x:a) : String = structuralShow(reflect(x), x)
}
};Derivation is procedural, algebra-owned, and opt-in. A request such as instance Show(Box(a)) = derive executes the algebra’s checked recipe over the target declaration’s semantic data shape and produces ordinary instance members. The generated members pass through normal type checking, evidence resolution, coherence, laws, specialization, and target compilation.
The Derivation compile-time effect supplies requireEvidence and rejectDerivation. Structural recipe operations traverse the declaration’s flat constructor telescopes and request the field evidence they use. Closed requirements must resolve immediately. Requirements mentioning only parameters of the instance head are inferred and become implicit evidence requirements of the generated provider. An explicit requires clause on a derived instance is a checked contract and must entail all inferred requirements.
A recipe may make an additional compile-time request explicitly:
derive {
function checkedShow(x:a) : String =
let available = requireEvidence(Show(String)) in
structuralShow(reflect(x), x)
}The returned evidence handle belongs to recipe execution; it is not emitted as runtime data. rejectDerivation(error) aborts the request with the supplied structured DeriveError. Missing or ambiguous closed evidence, an escaping evidence goal, and an explicit rejection are static errors.
Compile-time reflection, derivation effects, and structural plan operations must disappear before executable RuntimeCore. They cannot be called as runtime introspection APIs.
10. Laws
10.1 Syntax
law associativity(x:a, y:a, z:a) =
combine(combine(x,y),z) === combine(x,combine(y,z));
law transitivity(x:a, y:a, z:a) =
(x <= y) === True ==>
(y <= z) === True ==>
(x <= z) === True;=== forms propositional equality in a law expression. ==> forms implication and associates to the right.
10.2 Semantics
A law declaration must be well typed. It is recorded as a named proposition and is inherited with the structure. It does not automatically construct Refl and does not become an optimizer rewrite merely because it was declared.
The test runner may generate property tests when suitable generator evidence is available. Proof/trust status and optimizer eligibility follow LanguageDesign.md; there is no additional surface modifier in this language revision.
11. Primitive Types, Intrinsics, and Representations
11.1 Primitive declarations
primitive Int;
primitive Float64;
primitive Array(a:Type);A primitive has compiler/runtime storage but no implicit operations. Operations come from ordinary algebras, functions, effects, and target implementations.
11.2 Intrinsics
function clockNanos() : Int = intrinsic;
value machineEpsilon : Float64 = intrinsic;
instance Additive(Int) = intrinsic;
instance Floating(Float64) = {
value pi = intrinsic
};intrinsic promises a compiler/provider implementation matching the canonical declaration. It may supply a function body, a complete instance, or a pure value body. A top-level intrinsic value requires an explicit type; an instance value may inherit its type from its structure declaration. An intrinsic value whose type is Eff is invalid. Unsupported intrinsics are target-planning errors.
11.3 Representation declarations
repr Nat as Int default where {
function toRepr(n:Nat) : Int = ...;
function fromRepr(i:Int) : Nat = ...
};Parameterized form:
repr Vec(a,n) as PackedVector(a,n) where { ... };A total representation is an Iso-like round trip. A restricted representation must declare and check its validity domain:
repr Natural as Int32 where {
function toRepr(n:Natural) : Int32 = ...;
function fromRepr(i:Int32) : Natural = ...;
invariant(i:Int32) = i >= 0
};The compiler treats this as an embedding over the valid domain, not an unconditional isomorphism.
11.4 Repr cast
value encoded = natural as Int32;as selects a declared representation direction. It is not an OOP downcast, numeric coercion, or arbitrary conversion.
11.5 Floating multiply-add contraction policy
Floating-point expressions use the same surface operators in every mode. The compiler build option selects whether a target may contract an adjacent floating multiplication and addition:
--fp-contract=off
--fp-contract=fast
off is the default. It requires the multiplication and addition in an expression such as a * b + c to remain separate operations, including the rounding boundary between them. A target that cannot provide this guarantee must reject the build.
fast permits, but does not require, the target to contract that pair into a fused multiply-add with one rounding. Programs compiled in this mode must not depend on whether a particular target or optimizer performs the contraction.
This option permits only implicit multiply-add contraction. It does not permit general reassociation, reciprocal approximation, algebraic rewriting under exact Field laws, assumptions that NaN or infinity cannot occur, or other unsafe floating-point transformations. It introduces no source annotation and does not change operator spelling, typing, evidence resolution, or placement. Each compilation target maps the policy to its own conforming toolchain or runtime controls.
11.6 Primitive floating division
The standard Field(a) algebra retains its generic definition:
function (/)(x:a, y:a) : a = x * recip(y);Primitive Float32 and Float64 instances override that default. For those types, x / y has the observable semantics of one IEEE floating division with one rounding, and recip(y) has the semantics of one direct 1 / y division. A provider may use any instruction sequence that preserves those results and exceptional cases.
Primitive floating division must not be implemented observably as x * recip(y): the intermediate reciprocal introduces a second rounding and can overflow or underflow even when the direct quotient is finite. The --fp-contract policy does not alter division and never permits reciprocal replacement or approximation. A future relaxed numerical policy would require a separate language decision.
11.7 Typed semantic reflection
The Reflection module defines target-neutral, compile-time reflection:
primitive TypeRep(a:Type);
primitive TypeCode(context:Type, level:Nat);
primitive TypeView(context:Type, level:Nat);
primitive DataShape(context:Type, level:Nat);
function reflect(item:a) : TypeRep(a) = intrinsic;
function typeCode(rep:TypeRep(a)) : TypeCode(Unit, Z) = intrinsic;
function typeView(rep:TypeRep(a)) : TypeView(Unit, Z) = intrinsic;
function dataShape(rep:TypeRep(a)) : DataShape(Unit, Z) = intrinsic;TypeRep(a) is an unforgeable witness for the checked semantic type a. TypeCode represents universes, nominal applications, Pi types, n-ary telescopes, effects, and rows while preserving binder scope and universe level. The context index prevents a code containing a local type binder from escaping its scope. Compiler implementations use binder identity, not source names, to validate substitution.
TypeView classifies a semantic declaration. DataShape exposes a transparent data declaration’s parameter and constructor telescopes. Private declarations are unavailable outside their module, and an opaque declaration exports only nominal identity. Reflection never exposes size, alignment, offsets, object headers, calling convention, or target instructions.
In ordinary expressions, reflect(value) infers the represented type from the checked value. Within a computed data declaration, reflect(TypeExpression) reflects the checked type term without constructing a runtime value. All four types in this subsection are compile-time-only.
11.8 Data codes and transformations
primitive DataCode(context:Type, level:Nat);
function dataCode(rep:TypeRep(a)) : DataCode(Unit, Z) = intrinsic;
function renameDataType(code:DataCode(c,l), name:String) : DataCode(c,l) = intrinsic;
function renameConstructor(code:DataCode(c,l), oldName:String, newName:String)
: DataCode(c,l) = intrinsic;
function dropConstructor(code:DataCode(c,l), name:String)
: DataCode(c,l) = intrinsic;
function addNullaryConstructor(code:DataCode(c,l), name:String)
: DataCode(c,l) = intrinsic;
function replaceFieldType(code:DataCode(c,l), constructorName:String,
fieldName:String, replacement:TypeCode(c,l))
: DataCode(c,l) = intrinsic;DataCode is the transformable semantic description used by computed data declarations. It preserves one flat telescope for parameters and one flat telescope for each constructor’s fields. It carries no methods, visibility authority, or target layout. Each transformation preserves its context and universe indices. Unknown or duplicate names, invalid constructors or fields, scope escape, and a final declaration-name or parameter mismatch are static errors.
11.9 Runtime semantic reflection
Runtime reflection is explicit and distinct from compile-time reflection:
primitive RuntimeTypeRep(a:Type);
function runtimeTypeRep(item:a) : RuntimeTypeRep(a) = intrinsic;
function runtimeTypeName(rep:RuntimeTypeRep(a)) : String = intrinsic;RuntimeTypeRep(a) is an ordinary typed runtime value. Its identity is the canonical semantic type, including closed type arguments. A generic function using runtime reflection must be specialized to a closed type before an artifact can execute it. The reflected item is evaluated according to ordinary strict semantics.
The runtime API exposes semantic identity only. It does not expose compile-time DataCode, hidden constructors, private fields, or provider LayoutRep.
11.10 Unicode text and UTF-8
Char denotes a Unicode scalar value, not a UTF-8 byte or UTF-16 code unit. codePoint is its integer code point. charFromCodePoint is checked and returns Nothing for negative values, surrogate code points, and values above 10FFFF. nextChar and previousChar are checked scalar successors and skip the surrogate range. Consequently Char does not implement Enum: an unconditional succ, pred, or toEnum cannot satisfy the Enum laws at the scalar boundaries and surrogate gap.
String is an immutable finite sequence of Unicode scalar values. It may contain the zero scalar. It performs no implicit Unicode normalization: canonically equivalent scalar sequences remain distinct unless a separate normalization API is applied. Eq(String) compares exact scalar sequences and Ord(String) is lexicographic scalar order.
The portable text contract is:
algebra Textual(text:Type) = {
function concat(left:text, right:text) : text;
function length(value:text) : Int;
function utf8ByteLength(value:text) : Int;
function charAt(value:text, index:Int) : Maybe(Char);
function slice(value:text, start:Int, end:Int) : Maybe(text);
function indexOf(value:text, needle:text) : Maybe(Int);
function trimAscii(value:text) : text;
function toAsciiUpper(value:text) : text;
function toAsciiLower(value:text) : text;
function startsWith(value:text, prefix:text) : Bool;
function endsWith(value:text, suffix:text) : Bool;
function replace(value:text, old:text, replacement:text) : text;
function split(value:text, delimiter:text) : List(text);
function join(parts:List(text), separator:text) : text;
function fromChar(value:Char) : text;
function toChars(value:text) : List(Char)
};Every index and range in this contract is a scalar index. Ranges are half-open. charAt and slice return Nothing for negative or out-of-bounds indices. indexOf returns a scalar index, returns Just(0) for an empty needle, and returns Nothing when no match exists. Replacing an empty pattern leaves the input unchanged; splitting on an empty delimiter returns a singleton list. trimAscii removes only 09 through 0D and 20 at both ends. ASCII case conversion changes only A through Z or a through z; its name makes the limited mapping explicit.
Show(String) emits a canonical Tulam string literal. Printable ASCII scalar values are emitted directly except for quote and backslash; the named escape set is used for supported controls, and every other non-ASCII or non-printable scalar is emitted as an uppercase \u{HEX} escape. Hashable(String) is the unsalted FNV-1a 64-bit hash of the canonical UTF-8 encoding, interpreted as a signed Int. Runtime hash tables may apply a private per-table salt after this stable semantic hash.
Utf8 is the portable opaque type of validated, canonical UTF-8 bytes. Its public constructors are encodeUtf8 : String -> Utf8 and utf8FromBytes : Array(Byte) -> Either(Utf8Error, Utf8); decodeUtf8 and utf8Bytes are total. Validation rejects invalid leading bytes, unexpected continuations, truncated sequences, overlong encodings, surrogate encodings, and values above 10FFFF, and reports the failing byte offset. Utf8 implements Textual, Eq, Ord, Show, Hashable, Semigroup, and Monoid with the same scalar semantics as String.
repr String as Utf8 where {
function toRepr(value:String) : Utf8 = encodeUtf8(value);
function fromRepr(value:Utf8) : String = decodeUtf8(value)
};This portable representation edge is semantic evidence, not a mandate for one physical layout. The native provider uses validated UTF-8 as the physical String representation, so these conversions erase to identity. A future .NET provider may instead map String to System.String while retaining the portable Utf8 type and implementing both through the same Textual API.
String literals use FromString(result) when an expected result type supplies that evidence; otherwise they have type String. FromString receives the already validated semantic String, never raw source bytes:
algebra FromString(result:Type) = {
function fromStringLiteral(text:String) : result
};12. Classes and Objects
12.1 Class declaration
class Animal(name:String, age:Int) = {
function describe(self:Self) : String = self.name
};Fields are constructor parameters. Methods take an explicit self parameter; Self is preferred for methods intended to participate in inheritance.
12.2 Construction, fields, and calls
value animal = Animal.new("Milo", 4);
value name = animal.name;
value text = animal.describe();Method syntax inserts the receiver as self. Field access remains ordinary dot projection.
12.3 Inheritance
class Dog(breed:String) extends Animal("unknown", 0) = {
override function describe(self:Self) : String = self.breed;
final function species(self:Self) : String = "Canis familiaris";
static function family() : String = "Canidae"
};A class has at most one implementation parent in this language revision. Inherited fields are laid out parent-first. override is required when replacing an inherited virtual method. final prevents further override. static has no receiver. super.method(args) invokes the parent implementation.
12.4 Abstract and sealed classes
abstract class Shape = {
function area(self:Self) : Float64
};
sealed class Result(a:Type) = { ... };Abstract classes cannot be directly constructed. A sealed class can only be subclassed in its defining module, enabling exhaustive matching over known children.
12.5 Algebra implementation
class User(name:String) implements Show(User), Eq(User) = {
function show(self:User) : String = self.name;
function (==)(self:User, other:User) : Bool = self.name == other.name
};implements constructs ordinary algebra evidence from matching explicit class methods and applicable structure defaults. It represents class-owned behavior and never silently selects an algebra’s structural derive recipe. Missing minimal methods are a static error.
Structural class behavior is requested separately:
sealed class Point(x:Int, y:Int) = {};
instance Eq(Point) = derive;Structural derivation is valid only for a sealed leaf class whose semantic field shape is closed. Open, abstract, and non-leaf class hierarchies require explicit behavior. Class and algebra hierarchies remain distinct in both forms.
12.6 Subtyping and casts
If Dog extends Animal, then Dog <: Animal. Upcasts are inserted as explicit core coercions and preserve normal dependent Pi substitution.
Downcasts use ordinary checked APIs such as:
downcast(Dog, animal) : Maybe(Dog)as is never used for class downcasting.
13. Effects and Handlers
13.1 Effect declarations
effect Console = {
function readLine() : String;
function putStrLn(text:String) : Unit
};Effects may be parameterized. Their type variables follow ordinary declaration scope and universe rules.
The default resumption upper bound is affine (zero or one resume). An effect requiring multi-shot continuations declares ordinary evidence:
effect Choice requires Resumption(Many) = {
function choose[a:Type](options:List(a)) : a
};No new resumption keyword is introduced.
13.2 Effectful functions
function greet() : Eff { console:Console } Unit = action {
name <- readLine();
putStrLn("Hello " ++ name)
};Effects are inferred when omitted, but exported declarations should normally state effect contracts. Open rows make higher-order functions effect polymorphic:
function twice(f:a -> Eff { | e } a, x:a) : Eff { | e } a = ...;An effect row label names one installation requirement, not a runtime string. An unqualified operation call is accepted when its operation identity is unique in context. If two row entries expose the same operation name, qualify the request with the row label:
function compare()
: Eff { left:LocalState, right:RemoteState } Bool = action {
a <- left.read();
b <- right.read();
a == b
};label.operation(args) is resolved statically to the label, effect contract, and operation declaration. If the left name resolves to an ordinary lexical value, ordinary field or method resolution takes precedence. An unqualified or qualified request whose identity is still ambiguous is rejected; operation dispatch never uses dynamic name lookup.
13.3 Handlers
handler SilentConsole : Console = {
function readLine() = "";
function putStrLn(text) = Unit
};
handler RefState(initial:s) : State(s) = {
let cell = newRef(initial);
function get() = readRef(cell);
function put(value) = writeRef(cell, value)
};
handler RaiseToEither : Raise(Error) = {
return(item) = Right(item);
function raise(error) = Left(error)
};Install a handler with:
handle computation with SilentConsole
handle computation with RefState(0)Handling removes exactly the handled effect label and adds effects used by the handler implementation. A handler implements every required operation exactly once. Operation parameter and result types are inherited from the effect after substituting the handler’s effect arguments.
The optional contextual clause return(item) = expression handles normal completion. It may transform the computation result from a to the handler result b. If omitted, it is the identity transformation, so a and b are the same. There may be at most one return clause. Writing function return still implements an effect operation literally named return.
The optional contextual clause finally() = expression registers deep finalization for the dynamic handler installation. Its expression must produce Unit, may use the handler’s parameters and initialized local bindings, and cannot use resume. There may be at most one finally clause. Its effects are part of the handler’s resulting effect row. Writing function finally still implements an effect operation literally named finally.
Deep finalization runs exactly once when that dynamic installation exits by a language-observable path: normal completion, an abortive operation, an exception effect, cancellation, or recoverable target failure. On normal completion the return transformation runs before the installation exits. Finalization is also required if that transformation or an operation clause then exits nonlocally. The guarantee cannot cover termination that no Tulam runtime can observe, such as forced process/container destruction, hardware loss, or SIGKILL.
A continuation that encloses a resource-bearing finalized scope is affine unless the resource contract supplies explicit duplication evidence. A Many handler may not duplicate or repeatedly finalize a non-duplicable resource.
13.4 Resumption
Inside a resumable operation implementation, resume is a scoped function provided by handler elaboration:
handler FirstChoice : Choice = {
function choose[a:Type](options:List(a)) = resume(head(options))
};The compiler infers whether the continuation is abortive, linear, or affine and checks it against the effect’s upper bound. Calling resume multiple times requires Resumption(Many) and target/runtime support.
Handlers are deep: resumed computation remains under the same handler unless an explicit library combinator defines another scope.
13.5 Default handlers
handler StdConsole : Console = default { ... };A default handler is a deployment convenience, not removal of the effect from the function type. Defaults must be coherent per target/deployment context.
14. Actions
Actions are sequencing syntax over typed effectful computations:
action main() : Eff { console:Console, file:FileIO } Unit = {
path = "input.txt";
text <- readFile(path);
putStrLn(text)
};Statements are:
| Form | Meaning |
|---|---|
x <- effectful; |
bind the produced value |
x = pure; |
local pure binding |
effectful; |
sequence and discard Unit/result |
| final expression | action result |
Actions desugar into typed sequencing/bind operations while preserving effect rows and handler scope. An action may carry requires and on clauses in the same canonical order as a function.
15. Explicit Laziness
15.1 Lazy type
primitive Lazy(a:Type);
function delay(body:Unit -> a) : Lazy(a) = intrinsic;
function force(value:Lazy(a)) : a = intrinsic;Lazy(a) is memoized call-by-need. It is distinct from a; no implicit auto-force occurs.
15.2 Expression sugar
~expressiondesugars to:
delay(fn() = expression)15.3 Lazy fields and binders
type Stream(a:Type) =
Empty
+ More * head:a * ~tail:Stream(a);~field:T desugars to field:Lazy(T). The same notation may be used on a parameter when the grammar expects a binder. The bound variable has type Lazy(T) and must be forced explicitly.
function streamHead(~xs:Stream(a)) : Maybe(a) =
match force(xs) | Empty -> Nothing | More * x * tail -> Just(x);Effectful suspension uses an effect-indexed library type and is not silently stored in pure Lazy.
16. Targets and Placement
16.1 Policy values
Policies are ordinary values:
value compute : TargetPolicy =
prefer(capability(ParallelCompute), current);There is no policy declaration or target-specific processor keyword.
16.2 Declaration placement
function matrixMultiply(a:Matrix(f,m,k), b:Matrix(f,k,n))
: Matrix(f,m,n) on compute = ...;Callers use ordinary calls. A module default avoids repetition:
default target compute;16.3 Target blocks
target FastAccelerator {
function matrixMultiply(a,b) = intrinsic;
instance Lane(Float32) = intrinsic;
handler DeviceClock : Clock = {
function clockNanos() = intrinsic
};
repr Matrix(f,m,n) as DeviceMatrix(f,m,n) where { ... };
};A target block supplies implementations for canonical declarations. It does not perform expression-level conditional compilation and cannot introduce a public API available on only one target.
16.4 Foreign declarations
target dotnet {
extern function writeLine(text:String) : Unit;
};Foreign declarations are checked against target metadata where available and carry inferred or declared effects. Target imports provide metadata:
import System.Console target dotnet;16.5 No call-site target syntax
The following are not language forms: execute, runOn, runAt, @device, call-site on, expression target switches, or implicit marshal. Explicit expert scheduling and transfer use ordinary typed libraries and target handles.
17. Concurrency and Mutation
The core surface needs no special concurrency grammar. Standard libraries expose effectful, scope-indexed operations:
withScope(fn(scope) = ...)
spawn(scope, fn() = work())
await(task)
atomically(fn(tx) = ...)
readTVar(tx, cell)
writeTVar(tx, cell, value)These names are library APIs, not keywords. Their types enforce lifetime, cancellation, effect, and ownership rules. Future ergonomic sugar may be added only after the underlying types are stable and this reference is updated.
18. Interop
Interop composes existing features:
- a portable algebra/class/effect defines the semantic contract;
- a target import provides foreign metadata;
- a target block supplies extern functions, instances, handlers, methods, or representations;
reprhandles explicit storage conversion;Transferhandles cross-target movement;- target planning selects a conforming implementation.
Foreign null, exceptions, mutation, async behavior, and ownership must appear in types/effects or be discharged by a checked boundary. They are not silently treated as pure tulam behavior.
19. Static Semantics
19.1 Strict validity
The batch compiler rejects lexical, parse, name, kind, type, universe, positivity, required-termination, coverage, coherence, effect, representation, class, target-refinement, and backend-reachability errors.
A future interactive shell may continue after selected diagnostics in an explicit recovery mode, but it must use the canonical artifact pipeline and cannot emit a valid artifact until strict checks pass.
19.2 Bidirectional checking
Expressions synthesize types where possible and check against expected types where context is available. Expected types guide literals, constructors, existential witnesses, higher-order calls, and instance resolution.
19.3 Definitional equality
Types are compared modulo capture-avoiding substitution and terminating normalization. Type checking never evaluates effects or unrestricted recursion.
19.4 Subtyping
Nominal class subtyping and universe cumulativity are directed relations. Structural record compatibility is row-based. Algebra satisfaction is evidence, not subtyping. Implicit subtype conversion is elaborated into explicit core coercions.
19.5 Coverage
Sum types and sealed class families support exhaustiveness checking. Open rows, open class families, and abstract foreign inputs require a catch-all unless a refinement proves completeness.
20. Desugaring Summary
| Surface form | Core-oriented meaning |
|---|---|
A -> B |
anonymous Pi |
(x:A) -> B(x) |
dependent Pi |
forall x. T |
implicit/erased Pi |
(x:A) * B(x) |
dependent Sigma |
exists (x:A). T |
Sigma with hidden witness |
if c then a else b |
match on Bool |
let x = a in b |
lambda application |
block let |
nested sequential lets |
fn(x) = body |
anonymous lambda |
action |
typed sequencing/bind chain |
~expr |
delay(fn() = expr) |
~field:T |
field:Lazy(T) |
obj.method(args) |
method call with receiver |
| class upcast | explicit core coercion |
expr as T |
declared repr conversion |
requires C |
implicit evidence Pi/obligation |
on policy |
non-semantic placement metadata |
| target function | checked variant of canonical function |
21. Canonical Grammar
This EBNF collects the canonical forms defined by the preceding sections. It is complete at the level of surface constructs, but leaves character escapes, Unicode categories, operator tokenization, and semantic restrictions to the corresponding prose. { x } means repetition and [ x ] means optional syntax in this grammar; literal braces and brackets are quoted.
21.1 Files and declarations
program = [ module_decl ],
{ import_decl | open_decl },
[ export_decl ], [ default_target ],
{ declaration, ";" } ;
module_decl = "module", module_name, ";" ;
module_name = upper_name, { ".", upper_name } ;
import_decl = "import", module_name, [ import_filter ],
[ target_qualifier ], ";" ;
import_filter = "(", name, { ",", name }, ")"
| "hiding", "(", name, { ",", name }, ")" ;
target_qualifier = "target", target_ref ;
open_decl = "open", module_name, ";" ;
export_decl = "export", "(", name, { ",", name }, ")", ";" ;
default_target = "default", "target", policy_expr, ";" ;
declaration = type_decl | opaque_type_decl | primitive_decl
| function_decl | action_decl | value_decl
| structure_decl | instance_decl | repr_decl
| effect_decl | handler_decl | class_decl
| target_block | fixity_decl | private_decl ;
private_decl = "private", declaration ;
opaque_type_decl = "opaque", "type", upper_name, [ binders ],
"=", type_expr ;
function_decl = "function", function_name, [ implicit_parameters ],
parameters, [ return_clause ], [ requires_clause ],
[ placement_clause ], [ "=", function_body ] ;
function_name = lower_name | "(", operator, ")" ;
function_body = expr | "intrinsic"
| "match", match_arm, { match_arm } ;
action_decl = "action", lower_name, parameters,
[ return_clause ], [ requires_clause ],
[ placement_clause ], "=", action_block ;
value_decl = "value", lower_name, [ return_clause ],
[ "=", (expr | "intrinsic") ] ;
parameters = "(", [ parameter, { ",", parameter } ], ")" ;
implicit_parameters = "[", parameter, { ",", parameter }, "]" ;
parameter = [ "~" ], lower_name, [ ":", type_expr ] ;
binders = "(", binder, { ",", binder }, ")" ;
binder = name, ":", type_expr ;
return_clause = ":", type_expr ;
requires_clause = "requires", structure_ref,
{ ",", structure_ref } ;
placement_clause = "on", policy_expr ;
structure_ref = upper_name, [ type_arguments ] ;
type_decl = "type", upper_name, [ binders ],
[ "=", (type_body | computed_data_expr) ],
[ deriving_clause ] ;
type_body = constructor, { "+", constructor }
| field, { "*", field }
| exists_type ;
computed_data_expr = lower_name, arguments ;
constructor = upper_name, { "*", field }, [ ":", type_expr ] ;
field = [ "~" ], lower_name, ":", type_expr
| "..", upper_name ;
deriving_clause = "deriving", upper_name, { ",", upper_name } ;
primitive_decl = "primitive", upper_name, [ binders ] ;
structure_decl = structure_kind, upper_name, [ binders ],
[ extends_clause ], [ requires_clause ],
"=", structure_block ;
structure_kind = "structure" | "algebra" | "trait"
| "morphism" | "bridge" ;
extends_clause = "extends", structure_ref,
{ ",", structure_ref } ;
structure_block = "{", [ structure_member,
{ ";", structure_member }, [ ";" ] ], "}" ;
structure_member = function_decl | value_decl | law_decl | derive_block ;
instance_decl = "instance", upper_name, type_arguments,
[ instance_tag ], [ requires_clause ], "=",
(instance_block | "intrinsic" | "derive") ;
instance_tag = "as", lower_name ;
instance_block = "{", [ instance_member,
{ ";", instance_member }, [ ";" ] ], "}" ;
instance_member = function_decl | value_decl | law_decl ;
law_decl = "law", lower_name, parameters, "=", law_expr ;
derive_block = "derive", "{", function_decl,
{ ";", function_decl }, [ ";" ], "}" ;
repr_decl = "repr", type_application, "as", type_application,
[ "default" ], "where", repr_block ;
repr_block = "{", repr_member, { ";", repr_member }, [ ";" ], "}" ;
repr_member = function_decl | invariant_decl ;
invariant_decl = "invariant", parameters, "=", expr ;
fixity_decl = fixity_kind, precedence, "(", operator, ")",
{ ",", "(", operator, ")" } ;
fixity_kind = "infixl" | "infixr" | "infix" ;
precedence = "0" | "1" | "2" | "3" | "4"
| "5" | "6" | "7" | "8" | "9" ;
At top level and inside declaration blocks, semicolons separate declarations; the block productions make the optional trailing semicolon explicit.
21.2 Effects, classes, and targets
effect_decl = "effect", upper_name, [ binders ],
[ requires_clause ], "=", effect_block ;
effect_block = "{", effect_member, { ";", effect_member },
[ ";" ], "}" ;
effect_member = function_decl ;
handler_decl = "handler", upper_name, [ parameters ],
":", type_expr, "=", [ "default" ],
handler_block ;
handler_block = "{", handler_member, { ";", handler_member },
[ ";" ], "}" ;
handler_member = local_binding | function_decl
| handler_return | handler_finalizer ;
handler_return = "return", "(", lower_name, ")", "=", expr ;
handler_finalizer = "finally", "(", ")", "=", expr ;
class_decl = [ class_modifier ], "class", upper_name,
[ parameters ], [ class_extends ],
[ implements_clause ], "=", class_block ;
class_modifier = "abstract" | "sealed" ;
class_extends = "extends", upper_name, [ arguments ] ;
implements_clause = "implements", structure_ref,
{ ",", structure_ref } ;
class_block = "{", [ class_member, { ";", class_member },
[ ";" ] ], "}" ;
class_member = { method_modifier }, function_decl ;
method_modifier = "override" | "final" | "static" ;
target_block = "target", target_ref, "{",
{ target_declaration, ";" }, "}" ;
target_declaration = function_decl | instance_decl | handler_decl
| repr_decl | extern_decl ;
extern_decl = "extern", "function", function_name, parameters,
return_clause ;
target_ref = name ;
policy_expr = expr ;
21.3 Types
type_expr = forall_type | exists_type | arrow_type ;
forall_type = ("forall" | "∀"), quantified_binder,
{ quantified_binder }, ".", type_expr ;
exists_type = ("exists" | "∃"), quantified_binder,
{ quantified_binder }, ".", type_expr ;
quantified_binder = name | "(", binder, ")" ;
arrow_type = sum_type, [ "->", arrow_type ] ;
sum_type = product_type, { "+", product_type } ;
product_type = type_postfix, { "*", type_postfix } ;
type_postfix = type_atom, { ".", (name | integer) } ;
type_atom = universe | type_application
| record_type | effect_type | "(", type_expr, ")" ;
universe = "Type" | higher_universe ;
type_arguments = "(", type_expr, { ",", type_expr }, ")" ;
record_type = "{", record_type_field,
{ ",", record_type_field },
[ ",", "..", lower_name ], "}" ;
record_type_field = lower_name, ":", type_expr ;
effect_type = "Eff", effect_row, type_expr ;
effect_row = "{", [ effect_entries, [ "|", lower_name ]
| "|", lower_name ], "}" ;
effect_entries = effect_entry, { ",", effect_entry } ;
effect_entry = lower_name, ":", type_application ;
type_application = identifier, [ type_arguments ] ;
The higher_universe lexical family is the Type1, Type2, and subsequent spelling described in Section 4.1. This grammar does not add a separate programmer-written universe-level expression.
21.4 Expressions and patterns
expr = annotation_expr ;
annotation_expr = repr_expr, [ ":", type_expr ] ;
repr_expr = infix_expr, [ "as", type_expr ] ;
infix_expr = prefix_expr, { operator, prefix_expr } ;
prefix_expr = [ prefix_operator ], postfix_expr ;
postfix_expr = primary_expr, { postfix_part } ;
postfix_part = arguments | ".", (name | integer)
| record_update ;
primary_expr = literal | identifier | "super" | tuple_record_expr
| named_construction | if_expr | let_expr | match_expr
| action_expr | handle_expr | unpack_expr
| anonymous_function | lazy_expr | "(", expr, ")" ;
arguments = "(", [ expr, { ",", expr } ], ")" ;
named_construction = upper_name, "{", named_expr,
{ ",", named_expr }, "}" ;
record_update = "{", named_expr, { ",", named_expr }, "}" ;
named_expr = lower_name, "=", expr ;
tuple_record_expr = "{", [ tuple_items | named_items ], "}" ;
tuple_items = expr, { ",", expr } ;
named_items = named_expr, { ",", named_expr } ;
literal = integer_literal | floating_literal | character_literal
| string_literal | list_literal | vector_literal ;
list_literal = "[", [ expr, { ",", expr } ], "]" ;
vector_literal = "<", expr, { ",", expr }, ">" ;
if_expr = "if", expr, "then", expr, "else", expr ;
let_expr = "let", (local_binding | let_block), "in", expr ;
let_block = "{", local_binding, { ";", local_binding },
[ ";" ], "}" ;
local_binding = [ "function" ], lower_name, [ parameters ],
[ return_clause ],
"=", expr ;
match_expr = "match", [ expr ], match_arm, { match_arm } ;
match_arm = "|", pattern, "->", expr ;
pattern = literal | lower_name | "_" | constructor_pattern
| tuple_pattern | named_pattern ;
constructor_pattern = upper_name, { "*", pattern } ;
tuple_pattern = "{", pattern, { ",", pattern }, "}" ;
named_pattern = upper_name, "{", named_pattern_field,
{ ",", named_pattern_field }, "}" ;
named_pattern_field = lower_name, "=", pattern ;
anonymous_function = "fn", parameters, [ return_clause ], "=",
(expr | "match", match_arm, { match_arm }) ;
lazy_expr = "~", expr ;
handle_expr = "handle", expr, "with", expr ;
unpack_expr = "unpack", expr, "as", "(", lower_name, ",",
lower_name, ")", "in", expr ;
action_expr = "action", action_block ;
action_block = "{", action_statement,
{ ";", action_statement }, [ ";" ], "}" ;
action_statement = lower_name, "<-", expr
| lower_name, "=", expr
| expr ;
law_expr = equality_proposition, [ "==>", law_expr ] ;
equality_proposition = expr, [ "===", expr ] ;
name = lower_name | upper_name ;
identifier = lower_name | upper_name ;
Application and projection bind more tightly than prefix operators; prefix operators bind more tightly than infix operators; representation casts and annotations bind more loosely. Infix association and precedence come from the declared fixity table.
The parser may retain transitional acceptance while an implementation phase is in progress, but such acceptance is an implementation gap, not an extension of this grammar. The formatter and all new source emit only canonical forms.
22. Quick Reference
| Feature | Canonical syntax |
|---|---|
| Module | module Math.Matrix; |
| Selective import | import Math.Algebra (Field, zero); |
| Hiding import | import Backend.API hiding (unsafeCall); |
| Open module | open Math.Algebra; |
| Export list | export (Matrix, multiply); |
| Private declaration | private value secret = ...; |
| Opaque type | opaque type Token = Int; |
| Function | function f(x:A) : B = body; |
| Implicit parameter | function id[a:Type](x:a) : a = x; |
| Constraint | requires Eq(a), Show(a) |
| Placement | on compute |
| Module default | default target compute; |
| Lambda | fn(x:A) : B = body |
| Value | value x : A = body; |
| Intrinsic value | value x : A = intrinsic; |
| List literal | [a, b, c] |
| Tuple value | {a, b, c} |
| Structural record | {name = "Ada", age = 36} |
| Sum type | type T = A + B * value:Int; |
| Product type | type P = x:Int * y:Int; |
| Computed data | type T = schema(dataCode(reflect(Source))); |
| Named construction | P { x = 1, y = 2 } |
| Record update | p { x = 3 } |
| Projection | p.x, triple.0 |
| Pi | (x:A) -> B(x) |
| Sigma | (x:A) * B(x) |
| Universal | forall (a:Type). T |
| Existential | exists (a:Type). T |
| Unpack | unpack e as (a,x) in body |
| Let | let x = value in body |
| Sequential let | let { x = 1; y = f(x) } in y |
| Conditional | if c then a else b |
| Match | match x | A -> a | B * y -> b |
| Annotation | expression : Type |
| Fixity | infixl 6 (+); |
| Structure | structure S(a,b) = { ... }; |
| Algebra | algebra A(a) = { ... }; |
| Morphism | bridge M(a,b) = { ... }; |
| Instance | instance A(T) = { ... }; |
| Named instance | instance Format(Date) as iso8601 = { ... }; |
| Law | law name(args) = lhs === rhs; |
| Derive instance | instance Eq(T) = derive; |
| Typed reflection | typeCode(reflect(T)) |
| Runtime reflection | runtimeTypeName(runtimeTypeRep(value)) |
| Primitive | primitive Int; |
| Repr | repr A as R where { ... }; |
| Repr cast | value as R |
| Class | class C(fields) = { ... }; |
| Inheritance | class D extends C = { ... }; |
| Effect | effect E = { ... }; |
| Handler | handler H : E = { ... }; |
| Handle | handle expr with H |
| Handler return | return(value) = transformed |
| Handler finalizer | finally() = cleanup |
| Qualified operation | rowLabel.operation(args) |
| Action | action main() : Eff { console:Console } Unit = { ... }; |
| Action bind | x <- operation(); |
| Lazy expression | ~expr |
| Force | force(lazyValue) |
| Target overlay | target Profile { ... }; |
| Foreign declaration | extern function f(x:A) : B; inside a target block |
The standard library API is documented separately in StandardLibrary.md.