Named Types & Contracts

Declaring a Named Type

The basic declaration form is:

type Name BaseType

Examples:

type CustomerID uint64
type Temperature float64
type Price decimal
type UserName string
type StatusCode int32

The type name describes the semantic role of the value. The base type provides the underlying value domain on which the named type is defined.

Named and nominal user-defined types use uppercase names:

CustomerID
Temperature
UserName

Nominal Identity

Every named type has its own identity.

type CustomerID uint64
type ProductID uint64

let customer: CustomerID := 42
let product: ProductID := customer    // invalid

CustomerID and ProductID remain different types even though both are based on uint64.

The same rule applies when contracts are identical:

type Percentage int range 0..100
type BatteryLevel int range 0..100

let charge: BatteryLevel := 85
let discount: Percentage := charge    // invalid

Contract compatibility is not type identity. The compiler does not infer that two concepts are interchangeable merely because their valid value sets happen to overlap.

Why Named Types Matter

Many programming errors are category errors: the value has the right machine representation but the wrong meaning.

fn Transfer(from: uint64, to: uint64, amount: decimal) void {
}

The compiler cannot tell whether a caller accidentally swaps two unrelated uint64 values.

A semantic signature can make those mistakes visible:

type AccountID uint64
type Money decimal

fn Transfer(from: AccountID, to: AccountID, amount: Money) void {
}

Named types turn domain knowledge into compile-time information. They are useful even when no additional contract is needed.

Generic Named Types

Named types may be generic:

type ID[T] int
type Wrapped[T] T

Concrete instantiations preserve nominal identity:

ID[User]
ID[Product]

These are different concrete types even if their substituted representation is identical.

After substitution, ordinary named-type rules apply to the concrete type, including contracts, conversions, defaultability, copy and move behavior, layout and interface conformance.

Declaration with Untyped Literals

An untyped literal may be shaped directly by a named-type context.

type Percentage int range 0..100
type Money decimal

let percentage: Percentage := 90
let price: Money := 49.90

The literal is checked directly as a possible value of the target type. It does not first become int or decimal and then undergo an implicit conversion.

A literal that violates a contract is rejected at compile time:

let invalid: Percentage := 125

This behavior applies to untyped literals. An already typed value follows the normal conversion rules.

let raw: int := 90
let percentage: Percentage := raw    // invalid

Explicit Conversion

Converting an already typed value into a named type is explicit:

TargetType(value)

Example:

let raw: int := 90
let percentage := try Percentage(raw)

The conversion is checked. It must not silently truncate, wrap, discard precision or create a value that violates the target type's contracts.

When the compiler can prove the conversion valid from compile-time information, no runtime validation is needed.

let percentage := Percentage(50)

When the source value is known only at runtime and the conversion can fail, try is required.

let percentage := try Percentage(ReadPercentage())

Assignment

An already valid value of a named type may be assigned to another location of the same exact type.

let source: Percentage := 91
let mut target: Percentage := 10

target = source

The compiler does not revalidate the Percentage contract merely because the value moves to another storage location. source is already known to be a valid Percentage.

Assignment still follows normal mutability, ownership, copy and borrow rules.

A differently typed runtime value is not implicitly converted:

let raw: int := 50
target = raw    // invalid

Type Contracts

A contract restricts the set of semantic values that may exist as a named type. Contracts belong to the type declaration.

type Percentage int range 0..100
type Role string in ["admin", "user", "guest"]
type FiniteTemperature float finite

Every value of the type must satisfy its contracts.

let mut percentage: Percentage := 50
let mut role: Role := "user"
let mut temperature: FiniteTemperature := 20.0

Contracts do not belong to variables

These forms are not Sec:

let mut percentage: int range 0..100 := 50
let mut role: string in ["admin", "user"] := "user"

Struct fields also use named constrained types rather than attaching contracts directly to the field:

type Age int range 0..130

type User struct {
    age: Age,
}

Contract Composition

Multiple contracts are written sequentially:

type PositiveEven int range 1..100 even
type SmallStep int range 0..100 multipleOf 5

Sequential contracts form an implicit conjunction. Every contract must pass, in source order.

Sec does not add separate contract-composition keywords such as:

and
or
not

The compiler rejects contract combinations that are provably unsatisfiable.

type Impossible int odd even

This type has no valid integer values and is therefore invalid.

Range Contracts

range restricts a numeric named type to a compile-time-known interval.

type Percentage int range 0..100
type Port int range 1..<65536

The normal range operators determine inclusivity:

0..100      // includes 100
1..<65536   // excludes 65536

Range bounds must be compile-time constants compatible with the named type's base value domain.

Valid:

let complete: Percentage := 100
let port: Port := 443

Invalid:

let percentage: Percentage := 101
let port: Port := 65536

Ordered Membership

in [...] defines an ordered finite set of permitted values:

type Role string in ["admin", "user", "guest"]
type RetryCount int in [1, 3, 5]

The member list:

• must contain at least one value;
• contains compile-time constants;
• preserves source order;
• must not contain duplicates;
• must contain values compatible with the base type;
• must satisfy every other contract on the named type.

Invalid:

type EmptyRole string in []
type DuplicateRole string in ["admin", "admin"]
type InvalidEven int in [1, 2, 3] even

Invalid members are declaration errors. The compiler does not silently remove them.

Membership uses normal Sec semantic equality. It does not perform case folding, text coercion or numeric narrowing.

Integer Contracts

odd and even

type OddNumber int odd
type EvenNumber int even
type PositiveEven int range 1..100 even

odd and even apply to integer-like named types. They cannot both appear on the same type.

multipleOf

type PageOffset int multipleOf 4096
type SmallStep int range 0..100 multipleOf 5

The divisor must be a non-zero compile-time integer.

Integer contracts participate together in consistency checking and default resolution.

Finite Values

finite applies to floating-point and decimal named types.

type FiniteTemperature float finite
type FiniteAmount decimal finite

The contract excludes NaN and infinity where the representation supports them.

A range contract does not replace finite. Code must not depend on special NaN comparison behavior as a substitute for validation.

String Contracts

String-like named types may use text and length contracts.

regex

type Identifier string regex "^[A-Z][A-Z0-9_]*$"

The pattern is a compile-time string. The regular-expression syntax used by the language is defined by the contract implementation rules.

Length contracts

type UserName string minLen 3 maxLen 32
type CountryCode string exactLen 2
type NonEmptyText string notEmpty

minLen, maxLen and exactLen take non-negative compile-time integer values.

notEmpty requires a length greater than zero.

Collection Contracts

Supported collection-shaped named types may use the same length contracts:

type Labels list[string] minLen 1 maxLen 16
type RequiredValues int[] notEmpty

unique

type UniqueIDs list[CustomerID] unique

unique requires direct elements to be semantically unequal. It does not recursively inspect nested elements.

The element type must support equality.

Default Values

A named type may be defaultable. A default is always a valid semantic value of the named type.

Inherited primitive defaults

An unconstrained named type based on a defaultable primitive normally inherits the primitive default:

type UserName string
type Counter uint64

The corresponding defaults are conceptually:

UserName("")
Counter(0)

Nominal identity is preserved.

Constraint-derived defaults

A constrained numeric type chooses a valid default according to its complete contract set.

type Percentage int range 0..100       // default: Percentage(0)
type Port int range 1..65535           // default: Port(1)
type PositiveEven int range 1..100 even // default: PositiveEven(2)

For an ordered in [...] contract, the first listed value is the implicit default:

type Role string in ["admin", "user", "guest"]

The default is Role("admin").

If the rules cannot select one unique valid default, the type is non-defaultable unless an explicit default is declared.

Explicit default

The canonical syntax is:

type Port int range 1..65535 default 8080
type Role string in ["admin", "user", "guest"] default "user"

The explicit default:

• is written after all contracts;
• must be a compile-time constant;
• must be representable by the named type;
• must satisfy every contract;
• must not depend on runtime state or allocation.

An invalid default makes the type declaration invalid:

type Port int range 1..65535 default 0

Runtime Validation

A compile-time-known value can be validated when the source is compiled:

let percentage: Percentage := 50

A runtime value may require a fallible conversion:

let raw := ReadPercentage()
let percentage := try Percentage(raw)

The conversion establishes the named-type invariant. Once the value is known to be a valid Percentage, ordinary same-type use does not repeatedly recreate the validation obligation.

When static analysis proves that failure is impossible, the compiler may remove the runtime check while preserving the same language semantics.

Value-Producing Mutation

A plain same-type assignment transfers an already valid value. A compound assignment is different because it computes a new value.

let mut percentage: Percentage := 91
let additional: Percentage := 10

The mathematical result of:

percentage += additional

would be 101, which violates the type's contract.

Value-producing mutation of constrained storage is therefore fallible and uses try assignment:

try percentage += additional {
    Err(error) => {
        Handle(error)
    }
}

The same principle applies to other operations that compute a new constrained value for the destination.

Common Errors

Treating equal representation as equal type

type CustomerID uint64
type ProductID uint64

let customer: CustomerID := 42
let product: ProductID := customer

CustomerID is not ProductID.

Attaching a contract to a variable

let mut percentage: int range 0..100 := 50

Declare a named type instead.

Implicit conversion from a typed value

let raw: int := 90
let percentage: Percentage := raw

Use an explicit checked conversion.

Empty membership set

type Role string in []

A type contract must permit at least one value.

Duplicate membership value

type Role string in ["admin", "admin"]

Contradictory contracts

type Impossible int odd even

Invalid explicit default

type Port int range 1..65535 default 0

Unchecked value-producing mutation

let mut percentage: Percentage := 91
let additional: Percentage := 10

percentage += additional

When the resulting value may violate the contract, the mutation requires the canonical fallible assignment form.

Summary

• A named type is a new nominal type.
• Equal representation does not imply type compatibility.
• Named types may be generic.
• Concrete generic named-type instantiations preserve nominal identity.
• Untyped literals may be shaped directly by a named-type context.
• Already typed values require explicit conversion into a different named type.
• Fallible conversion uses try.
• Contracts belong only to named types.
• Multiple contracts form an implicit conjunction.
• range restricts a numeric value interval.
• in [...] defines an ordered finite value set.
• odd, even and multipleOf constrain integer-like named types.
• finite constrains floating-point and decimal values.
• regex and length contracts constrain string-like named types.
• Length and unique contracts may apply to supported collection-shaped named types.
• Provably contradictory contracts make the type declaration invalid.
• A named type may have an explicit compile-time default.
• Every default must satisfy every contract.
• Same-type assignment does not revalidate an already valid value.
• Value-producing mutation of a constrained type is fallible when the new value may violate the contract.