Data and functions

Primitive data constraints

The standard library exposes compiler-provided primitive declarations through std::primitive. The current set includes:

Constraint	Description
int	Default signed integer type
i8, i16, i32, i64	Signed integer types
u8, u16, u32, u64	Unsigned integer types
c_int, c_uint	C-compatible integer types
bool	Boolean data
str	String data
IO A	An effectful computation producing A
ptr A	A pointer to A

The standard library also defines data structures such as Nat, Option, Result, List, and Vec. See the standard-library reference.

Functions

Functions are ordinary terms. Lambda expressions use fun, and named definitions use def:

def add (left right : int) : int := left + right

def increment : int -> int := fun value => value + 1

Parameter lists are curried:

def add_one := add 1

Dependent arrows and parameter constraints can mention earlier parameters:

def increase (value : int) : int where (result => result >= value) :=
  value + 1

Generic and implicit parameters

Parameters in braces are inferred from context. A generic parameter is still a term constrained by prop:

def identity {A : prop} (value : A) : A := value

#check identity 42 : int

An explicit parameter such as A : prop can be used when callers need to choose the constraint directly.

Refinement constraints

Refinements describe a base constraint together with a predicate:

def NonZero : prop := int where (value => value /= 0)

def divide (left : int) (right : NonZero) : int := left / right

The compiler checks the predicate at each construction or call site. Proof arguments do not become runtime parameters.

Effects and do blocks

An IO A value is consumed in a do block. The standard library's I/O functions can be combined without exposing C details:

use std::io::print_line

pub def main : IO () :=
  do
    print_line 42

Calling an effectful value as pure data is rejected. FFI declarations use extern def; crossing the unsafe boundary is explicit with unsafe { ... }.