Top > Design docs > Core design > Part 02
Sigmal is a pure, total, structurally typed language.
At its logical core, Sigmal is based on a minimal Calculus of Inductive Constructions (CIC).
Terms and types inhabit a unified dependent λ-calculus with:
Sigmal includes only the computational core of CIC. It does not include:
There is:
Universes are indexed by natural numbers.
$ { e }
Where:
e : Nate must be const-normalizableSyntactic sugar:
$0 ≡ $ { 0 }
$1 ≡ $ { 1 }
$2 ≡ $ { 2 }
Universe equality is determined by equality of normalized Nat values.
Example:
$ { + 1 1 } ≡ $ { 2 }
if both expressions normalize to the same Nat.
Universes are stratified:
If A : $ { n }, then:
$ { n } : $ { + n 1 }
There is no Type : Type.
There is no impredicativity.
This stratification enforces logical consistency of the minimal CIC core.
Sigmal uses a single abstraction form:
\ (x : A) -> T = B
This form represents both:
Types are ordinary terms living in universes.
If:
A : $ { n }B : $ { m } under x : Athen:
\ (x : A) -> B : $ { max n m }
Non-dependent arrow sugar:
A -> B
is equivalent to:
\ (_ : A) -> B
Application uses whitespace and is left-associative:
f x y ≡ (f x) y
Parentheses are only for grouping:
f (g x)
Sigmal defines no infix operators.
Record types are finite maps from symbol keys to types:
&{
K1 : T1;
K2 : T2;
}
Record types are:
Two record types are definitionally equal iff:
Record values:
&{
K1 = v1;
K2 = v2;
}
Record types in Sigmal are non-dependent labeled product types. Field types do not depend on other fields.
Dependent product types (Σ-types) are not primitive record types. Instead, they are expressed using inductive families in the minimal CIC core.
A dependent pair type (Σ-type) can be defined as:
Sigma =
\ (A : $ { u })
(B : A -> $ { v })
-> $ { max u v }
= #{
Pack :
\ (a : A)
(b : B a)
-> Sigma A B;
};
Sigma A B represents a pair:
a : Ab : B awhere the type of the second component depends on the first.
A dependent pair is constructed using Pack:
Pack a b
where:
a : Ab : B aDependent pairs are eliminated using pattern matching:
^ p {
Pack(a, b) => ...
}
The types of a and b are refined in the match branch:
a : Ab : B aDependent elimination follows the general rules for inductive families (see Section 4).
Non-dependent record types:
&{
x : A;
y : B;
}
are equivalent to ordinary (non-dependent) product types.
Dependent pairs (Sigma) serve the role of dependent products (Σ-types) and should be used when later components depend on earlier ones.
Records remain:
Dependent pairs are a logical construct provided by the inductive core and are erased at runtime unless explicitly preserved.
Keeping records non-dependent preserves:
All dependent data relationships are expressed via inductive families in the minimal CIC core.
This keeps the calculus:
Inductive types may be indexed by values.
General form:
Ind =
\ (params...)
(indices...)
-> $ { u }
= #{
C1 : T1;
C2 : T2;
};
Constructors may specify explicit result types.
Example (length-indexed vector):
Vec =
\ (A : $0)
(n : Nat)
-> $0
= #{
Nil : Vec A 0;
Cons : \ (k : Nat) -> A -> Vec A k -> Vec A (S k);
};
Inductive definitions must satisfy:
Two inductive families are definitionally equal iff:
Pattern matching supports dependent elimination.
General form:
^ x : Motive {
C1(args...) => e1;
C2(args...) => e2;
}
Where:
Motive is a type family describing the result typeWhen non-dependent, motive may be omitted:
^ x {
...
}
Pattern matching must be exhaustive.
Propositional equality is an inductive family:
Eq =
\ (A : $0)
(x : A)
(y : A)
-> $0
= #{
Refl : Eq A x x;
};
No rewriting is performed automatically.
Transport across equality is defined via dependent elimination.
Equality reasoning is explicit.
Sym)Sym : $0
Symbols are structural identity atoms used as:
Symbol equality is structural.
There is no global registry.
Symbol representation is implementation-defined but must be deterministic.
@{ e }
Where:
e : Syme must be const-normalizableValid only in symbol-key positions.
Bare identifiers in key positions are sugar for:
@{ TextSym "identifier" }
Symbol construction utilities are provided by .std.core.
An expression e is const-normalizable if:
e typechecks in the pure fragmente is effect-freee terminatese reduces to a valueWe write:
Γ ⊢const e ⇓ v
Const-required positions include:
$ { e }@{ e }Const evaluation is:
Const evaluation does not execute effect interpreters.
Definitional equality corresponds to conversion in minimal CIC.
Definitional equality includes:
Only const-normalizable expressions participate in definitional equality.
No symbolic rewriting is performed.
Example:
Vec A (+ 3 0) may reduce if (+ 3 0) is const-normalizable.Vec A (+ n 0) is not definitionally equal to Vec A n; a proof via Eq is required.No automatic extensional reasoning is performed.
Runtime values cannot influence type structure unless they appear in const-normalizable positions.
There is:
Sym -> Type mappingType structure depends only on:
Sigmal performs no implicit property resolution.
If a function requires a property, it must receive a witness explicitly.
The only automatic reasoning mechanism is definitional equality.
All non-definitional reasoning must be expressed via values (e.g., Eq).
Typeclasses are ordinary record types.
There is:
Instances are explicit values.
Literal interpretation does not depend on implicit resolution.
Conversions must be explicit.
The Sigmal core type system is:
Type identity is structural and determined by normalized form.
All non-definitional properties must be passed explicitly as values.
Sigmal.org - the calculus we can build on