Top > Design docs > Core design > Part 01
Sigmal is a pure, total, compiled programming language designed to combine:
Sigmal is not an interpreted scripting language. It is intended to compile to low-level targets (LLVM, WASM, native) while preserving strong logical guarantees.
At its logical core, Sigmal is based on the minimal Calculus of Inductive Constructions (CIC). which is an extension of Calculus of Constructions (CoC). The core type system is a stratified, total, dependent λ-calculus with inductive families, in which terms and types inhabit a unified hierarchy of universes.
The goal is to provide a language suitable for:
without sacrificing explicitness or determinism.
Sigmal’s core calculus is a stratified, minimal form of the Calculus of Inductive Constructions (CIC).
Specifically:
Pattern matching supports dependent elimination.
Sigmal adopts only the core computational aspects of CIC.
It does not include:
All reasoning beyond definitional equality must be expressed explicitly as values.
All well-typed programs (as in pure expressions) terminate.
There is no:
Termination is a semantic guarantee of the language.
This guarantee applies to the pure fragment of the language. Nontermination may occur only through explicit effect encodings and their interpreters, and is not part of the core normalization semantics.
Nontermination, if desired (e.g., event loops), must be expressed explicitly via library-defined effect encodings or control values, and must not be reachable by the compile-time normalization semantics.
The core language is pure.
There are no built-in side effects.
All effects must be modeled explicitly as values.
Effectful behavior, if provided by libraries, is expressed through:
There are no hidden runtime effects.
Sigmal has no nominal type identity. Type identity is determined structurally within the underlying minimal CIC framework.
Type equality is determined by:
There is no subtyping hierarchy.
Two types are equal if their normalized structures are equal.
Sigmal performs no implicit property resolution.
If a function depends on a property (equality, ordering, allocation capability, effect handling, etc.), it must receive a witness explicitly.
There is:
The only automatic reasoning mechanism is definitional equality.
This follows directly from the minimal CIC foundation: properties are represented as values (types or inductive families), and all reasoning beyond definitional equality must be carried explicitly as terms.
Sigmal uses symbols (Sym) as structural identity atoms.
Symbols serve as:
Symbol equality is structural.
There is no global registry of symbols.
The representation and construction of Sym values may be implementation-defined, but must be deterministic: identical inputs under the same implementation yield symbols with identical structural equality behavior.
Certain syntactic positions require compile-time normalization.
This normalization corresponds to conversion in the underlying minimal CIC and forms part of definitional equality.
Universe levels and symbol injection require const-normalizable expressions.
Compile-time evaluation:
Const evaluation is not an optimization; it is a semantic requirement.
Const evaluation applies only to const-normalizable expressions and must not evaluate library encodings that represent effectful execution or potentially non-terminating control behavior.
Only const-normalizable expressions participate in definitional equality.
Sigmal defines no global namespace.
All visibility arises from:
Modules are ordinary values.
There is no implicit visibility of definitions.
A compilation unit evaluates to a value.
If that value is a record, it may serve as a namespace.
Projection (.) is the only namespace mechanism.
There is no nominal module identity.
Module resolution is external to the core language.
The language makes no assumptions about:
A resolver may provide a top-level module record.
The resolver must be deterministic.
The core language does not define how resolution occurs.
The resolver provides a standardized .std.* namespace. Some modules (e.g. .std.core) have fully standardized semantics across all targets. Other modules (e.g. .std.abi) have standardized interfaces but may vary in their provided values and behavior across targets, subject to the interface contract.
For a fixed target triple and implementation, .std.* modules are deterministic: given the same inputs, they produce the same outputs and compiled artifacts.
Aside from the standardized .std.* modules, resolution is unconstrained and implementation-defined.
Sigmal avoids reserved alphanumeric keywords.
Core constructs are introduced using symbolic tokens.
This preserves:
Tokens have deterministic meaning given syntactic form.
Sigmal defines no infix operators. All function application is prefix and explicit. There is no user-defined operator precedence or associativity in v1.
Sigmal has:
A compilation unit evaluates to a value.
All constructs produce values.
A compilation unit is implicitly a block expression: a sequence of bindings followed by a final expression whose value is the unit’s value (or Unit if the unit ends with a semicolon).
Sigmal is a compiled language.
Programs are compiled ahead-of-time to low-level targets.
There is no required runtime interpreter.
The language is designed to support:
Sigmal aims to support:
wasm32-unknown-unknown (freestanding WebAssembly)Sigmal makes minimal runtime assumptions.
There is:
A default allocator may be provided by standard libraries.
Reference-counted types are permitted.
Memory management strategies are explicit and library-defined.
Sigmal is designed to feel suitable for systems programming while preserving:
This includes:
The language aims to provide logical guarantees without sacrificing practical systems use.
Sigmal is deterministic in:
There is no hidden search phase or implicit inference beyond definitional equality.
Sigmal is:
It aims to combine:
while remaining small, explicit, and structurally coherent.
Sigmal.org - the calculus we can build on