Types
7 pages
Constructors
Type constructors: Record, ListOf, Maybe, Either, Variant.
Either
Tagged union of two types. Accepts { _tag =...
Dependent
Dependent contracts: Pi (Π), Sigma (Σ), Certified, Vector, DepRecord.
Grounded in Martin-Löf (1984)...
Foundation
Type system foundation: Type constructor, check, validate, make, refine.
check
Check whether a value inhabits a type....
Linear
Linear type constructors: structural guards for capability tokens.
Pure type predicates that check token structure...
Primitives
Primitive types: String, Int, Bool, Float, Attrs, Path, Function, Null, Unit, Any.
Any
Top type. Every value inhabits...
Refinement
Refinement types and predicate combinators.
Grounded in Freeman & Pfenning (1991) and Rondon et al....
Universe
Universe hierarchy: Type_0 : Type_1 : Type_2 : ... Lazy infinite tower.
level
Get the universe level of a...