The checker runs ordinary Ship through the same interpreter that runs programs. Constant validations are proven before the program exists, quoted code is transformed and inserted as checked code, and a named type's description is baked in where a program asks for it. Compile-time evaluation is pure: effects, services, and unbounded loops stop it.
Proven validation
An ensure on a constant input runs while checking. A construction that passes drops its error tag; the same construction over a runtime value keeps it and validates when it runs.
type Natural = new Int #{
ensure = fn(valuevalue: Int) {
if valuevalue: Int < 00: Int {
error :negative(valuevalue: Int);
}
};
}
Constant Validation
let fourfour: fn() -> Book.LanguageReference.CompileTime.Natural = () => Natural(44: Int);
✓fourfour: fn() -> Book.LanguageReference.CompileTime.Natural: pure fn!() -> Natural;
let naturalnatural: fn(n: Int) -> Book.LanguageReference.CompileTime.Natural, exn [ :negative(Int) ] = (nn: Int: Int) => Natural(nn: Int);
✓naturalnatural: fn(n: Int) -> Book.LanguageReference.CompileTime.Natural, exn [ :negative(Int) ]: fn(Int) -> Natural, exn [ :negative(Int) ];
expect ✓"${fourfour: fn() -> Book.LanguageReference.CompileTime.Natural()}" == "4""4": String;A constant that fails its ensure is a compile error naming the tag.
ensure! makes the compile-time half a requirement. The checker follows every helper the validation reaches, so a step that could never run while checking (an effect, a service, a non-pure builtin) is rejected at the declaration, and a constant input whose evaluation cannot finish is a compile error instead of a silent fallback to runtime. Runtime inputs still validate when they run.
type Percent = new Int #{
ensure! = fn(valuevalue: Int) {
if valuevalue: Int < 00: Int || valuevalue: Int > 100100: Int {
error :out_of_range(valuevalue: Int);
}
};
}
Required Compile-Time Validation
let halfhalf: fn() -> Book.LanguageReference.CompileTime.Percent = () => Percent(5050: Int);
✓halfhalf: fn() -> Book.LanguageReference.CompileTime.Percent: pure fn!() -> Percent;
let percentpercent: fn(n: Int) -> Book.LanguageReference.CompileTime.Percent, exn [ :out_of_range(Int) ] = (nn: Int: Int) => Percent(nn: Int);
✓percentpercent: fn(n: Int) -> Book.LanguageReference.CompileTime.Percent, exn [ :out_of_range(Int) ]: fn(Int) -> Percent, exn [ :out_of_range(Int) ];
expect ✓"${halfhalf: fn() -> Book.LanguageReference.CompileTime.Percent()}" == "50""50": String;Quoting and inserting code
#code(expr) quotes an expression without running it. The quote is a Code(T, 'scope) value: typed by what the expression produces and tied to the scope it was written in, so its names, control targets, and error channels keep their meaning wherever it lands. Transformers are ordinary functions over Code. #insert(code) runs its argument while checking, splices the result in place, and checks the inserted expression there.
let twicetwice: fn(scope 'scope)(code: Code(Int, 'scope)) -> Code(Int, 'scope) = (scope 'scope)(codecode: Code(Int, 'a): Code(Int, 'scope)) -> Code(Int, 'scope) =>
#code(#insert(codecode: Code(Int, 'a)) + #insert(codecode: Code(Int, 'a)));
let sixsix: Int = #insert(twicetwice: fn(scope 'scope)(code: Code(Int, 'scope)) -> Code(Int, 'scope)(#code(33: Int)));
Inserted Code
expect ✓sixsix: Int == 66: Int;Fallback ?> expands through the same path: source ?> fallback inserts the canonical OrElse expansion for the source's type. See Blocks and control flow.
Type descriptors
Type.of(T) is the Meta.Type the compiler hands to derivers for T: fields with their metadata, variant cases with their payloads. Code names the type statically, the checker builds the description, and the value exists at runtime only where the program uses it. There is no lookup from an arbitrary value back to its type.
type Account = {
name: String;
active: Bool;
}
Type Descriptors
let fieldsfields: Vector(String) = match Type.ofof: pure fn!('t)(target: Struct(Book.LanguageReference.CompileTime.Account)) -> Meta.Type(Account) {
| Product { productproduct: Meta.ProductDesc; } -> Vector.mapmap: pure fn!('a, 'b)(items: Vector(Meta.FieldDesc) @ 'm, ~f: fn(value: Meta.FieldDesc @ 'm) -> String) -> Vector(String)(productproduct: Meta.ProductDesc.fieldsfields: Vector(Meta.FieldDesc), f = (fieldfield: Meta.FieldDesc) => fieldfield: Meta.FieldDesc.namename: String)
| _ -> []
};
expect ✓fieldsfields: Vector(String) == ["name""name": String, "active""active": String];
expect ✓Json.schemaschema: pure fn!(target: Meta.Type) -> String(Type.ofof: pure fn!('t)(target: Struct(Book.LanguageReference.CompileTime.Account)) -> Meta.Type(Account)) == "Account {\n name: String\n active: Bool\n}""Account {\n name: String\n active: Bool\n}": String;A generic witness has no static type to describe, so Type.of(target) inside fn('t)(target: Struct('t)) is a compile error. Derivers receive the same descriptors and return Meta.Expr code built with #code quotes. Rejected programs collects the failures.