Types

Type constructors: Record, ListOf, Maybe, Either, Variant. Either Tagged union of two types. Accepts { _tag =...

Dependent contracts: Pi (Π), Sigma (Σ), Certified, Vector, DepRecord. Grounded in Martin-Löf (1984)...

Type system foundation: Type constructor, check, validate, make, refine. check Check whether a value inhabits a type....

Linear type constructors: structural guards for capability tokens. Pure type predicates that check token structure...

Primitive types: String, Int, Bool, Float, Attrs, Path, Function, Null, Unit, Any. Any Top type. Every value inhabits...

Refinement types and predicate combinators. Grounded in Freeman & Pfenning (1991) and Rondon et al....

Universe hierarchy: Type_0 : Type_1 : Type_2 : ... Lazy infinite tower. level Get the universe level of a...