Named Types, Contracts and Units

Sec allows programmers to define new types with the type keyword. A named type is not merely an alternative spelling for an existing type. It is a distinct semantic type that allows the compiler to distinguish values that have different meanings, even when those values use the same underlying representation.

Named types are a central part of Sec's type-safety model. They make it possible to represent concepts such as speed, money, percentages, identifiers, distances and durations as different types instead of treating all of them as interchangeable numbers.

Declaring a Named Type

A basic named type declaration consists of the type keyword, the new type name, and an existing underlying type.

type Speed int

This declaration creates a new type named Speed. Its underlying representation is int, but Speed and int are different types.

Named types may be created from any appropriate basic type:

type CustomerID uint64

type Temperature float64

type Price decimal

type Username string

type Initial rune

type StatusCode int32

The type name should describe the meaning of the value rather than only its storage format. A declaration such as type CustomerID uint64 communicates that the value is an identifier for a customer, not an arbitrary unsigned integer.

Underlying Type

Every basic named type has an underlying type. The underlying type determines the basic storage representation and which fundamental operations may potentially be available.

type Speed int

Here, int is the underlying type of Speed. A Speed value is represented using the same basic integer representation as int, but the compiler continues to treat it as Speed throughout semantic analysis.

The existence of an underlying type does not make the named type interchangeable with that type. Representation compatibility is not the same as semantic compatibility.

Named Type Identity

Every named type has its own identity. Two named types remain different even when they have the same underlying type and the same contracts.

type Speed int

type Money int

Both types use int as their underlying type. Nevertheless, a Speed value cannot be used where a Money value is required.

let speed: Speed := 80
let money: Money := speed // Compile-time error.

The compiler rejects this assignment because Speed and Money describe different concepts. The fact that both are represented by integers is irrelevant to their semantic identity.

The same rule applies to types with identical contracts:

type Percent int range 0..100

type BatteryLevel int range 0..100

let charge: BatteryLevel := 85
let discount: Percent := charge // Compile-time error.

A battery level is not a percentage discount merely because both values happen to be within the range from zero to one hundred.

Why Named Types Matter

Programs frequently contain values that share the same physical representation but have completely different meanings. Without named types, these differences exist only in variable names and programmer discipline.

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

This function signature does not tell the compiler what the two integers represent. The caller may accidentally reverse them or pass an unrelated integer.

A named-type version allows the compiler to enforce the intended meaning:

type AccountID uint64

type Money decimal

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

Named types convert domain knowledge into compile-time rules. The compiler can reject many category errors before the program is run.

Declaration with Untyped Literals

Untyped literals may be used directly when a named type is declared. The declaration provides the target context that gives the literal its type.

type Speed int

type Money decimal

let speed: Speed := 80
let price: Money := 49.90

In the first declaration, the integer literal 80 is checked as a possible Speed value. In the second declaration, the decimal literal 49.90 is checked as a possible Money value.

This rule applies to literals, not to variables. A variable already has a type and is never silently reshaped into another named type.

let raw := 80
let speed: Speed := raw // Compile-time error.

The variable raw has type int. It must be explicitly converted before it can be stored as Speed.

Explicit Conversion

Converting an existing value into a named type requires an explicit conversion. The target type is written like a function call around the source expression.

let raw := 80
let speed: Speed := Speed(raw)

The expression Speed(raw) explicitly requests conversion from the source value to Speed. This makes the change of semantic meaning visible in the source code.

Explicit conversion does not mean that every conversion must succeed. The source value must be representable by the underlying type and must satisfy every contract attached to the target type.

type Percent int range 0..100

let raw := 125
let percent: Percent := Percent(raw) // Contract violation.

When the source value is known during compilation, the compiler checks the conversion during compilation. A known-invalid conversion is rejected before the program can run.

When the source value is only known at runtime, conversion to a constrained type requires a runtime contract check. The exact error-handling form for failed runtime conversions is covered in the contracts and error-handling sections of the manual.

Assignment to Named Types

Assignment preserves the exact type of the target variable. After a named-type variable has been declared, later assignments must produce that named type.

type Speed int

let mut speed: Speed := 80
speed = Speed(90)

The following assignment is invalid:

speed = 90 // Compile-time error.

The literal was permitted in the original declaration because the declaration supplied target context. A later assignment does not weaken the identity of the variable. The programmer must explicitly construct or convert a Speed value.

This distinction is intentional:

let speed: Speed := 80       // Valid declaration.

let mut limit: Speed := 100  // Valid declaration.
limit = Speed(120)           // Valid assignment.
limit = 120                  // Invalid assignment.

Strict assignment rules make later code easier to audit because every change from an untyped or differently typed value into a named type remains explicit.

Compound Assignment

A compound assignment applies an operator and then assigns the result back to the left-hand variable.

speed += increase

Conceptually, this means:

speed = speed + increase

Therefore all normal assignment rules still apply:

  • The left-hand variable must have been declared with let mut.
  • The operator must be valid for both operand types.
  • The result must have the exact type required by the left-hand variable.
  • All contracts of the target type must remain satisfied.
type Speed int

let mut speed: Speed := 80
let increase: Speed := 10

speed += increase // Valid.

A different named type is rejected:

type Money int

let amount: Money := 10
speed += amount // Compile-time error.

Raw literals are not implicitly converted during compound assignment:

speed += 10        // Compile-time error.
speed += Speed(10) // Valid.

Contracts

A contract restricts which values are valid for a named type. The underlying type determines how a value is represented, while contracts determine which values are allowed to exist as instances of that type.

A value that violates a type contract is not a valid value of that type. Contract checking is part of type safety, not merely optional validation performed by application code.

Range Contracts

A range contract restricts a numeric named type to a defined interval.

type Percent int range 0..100

The type Percent is distinct from int and accepts values from zero through one hundred.

let none: Percent := 0
let half: Percent := 50
let all: Percent := 100

Values outside the range are invalid:

let negative: Percent := -1 // Compile-time error.
let tooHigh: Percent := 101 // Compile-time error.

Inclusive Ranges

The .. range form includes both endpoints.

type Percent int range 0..100

Both 0 and 100 are valid values of Percent.

Exclusive Upper Bound

The ..< form excludes the upper endpoint.

type ArrayIndex int range 0..<100

Values from 0 through 99 are valid. The value 100 is not valid.

Open-ended Ranges

A range may omit either endpoint.

type Maximum int range ..100

type NonNegative int range 0..

Maximum accepts values up to and including one hundred. NonNegative accepts zero and every larger value representable by its underlying type.

Compile-time and Runtime Contract Checking

Sec checks contracts as early as possible. When a value is known during compilation, a contract violation is a compile-time error.

type Port int range 1..65535

let port: Port := 8080  // Valid.
let invalid: Port := 0  // Compile-time error.

An explicit conversion of a compile-time-known value is checked in the same way:

let raw := 70000
let port: Port := Port(raw) // Compile-time error.

Values obtained from input, files, databases, networks or other runtime sources cannot always be verified by the compiler. Explicit conversion of such a value must perform the appropriate contract check at runtime.

let raw := ReadPortFromConfiguration()
let port: Port := Port(raw) // Requires runtime validation.

A contract is never silently ignored merely because the value was not known during compilation.

Contracts and Default Values

A constrained type has an implicit default value only when the default value of its underlying type satisfies every contract.

type Percent int range 0..100

The default integer value is zero, and zero is valid for Percent. Therefore Percent may have a valid default value.

type Port int range 1..65535

The default integer value is zero, but zero is not a valid Port. Therefore Port cannot be implicitly default-initialized.

Units

Sec can attach units to decimal types. Units are part of the semantic type system and allow the compiler to distinguish quantities such as money, distance, duration, mass and speed.

A unit is written inside angle brackets after decimal.

decimal<m>
decimal<s>
decimal<kg>
decimal<m/s>
decimal<SEK>

Unit-aware values are not decorative annotations. Their dimensions affect assignment, arithmetic, type inference and compatibility checks.

Declaring Named Unit Types

A named unit type combines a normal named type with a decimal unit.

type Meter decimal<m>

type Second decimal<s>

type Speed decimal<m/s>

type Money decimal<SEK>

Each declaration creates a distinct named type. The unit describes the type's physical or semantic dimension, while the type name identifies the domain concept used by the program.

Values may be declared using numeric literals:

let distance: Meter := 100
let duration: Second := 9.58
let price: Money := 249.90

The target type supplies the unit context for each literal.

Units and Named Type Identity

Units and named types both participate in semantic typing. Matching units do not automatically erase named-type identity.

type Width decimal<m>

type Height decimal<m>

Width and Height have the same unit dimension, but they remain different named types.

let width: Width := 2.5
let height: Height := width // Compile-time error.

This strictness prevents accidental mixing of values that happen to use the same measurement unit but represent different roles in the program.

Addition and Subtraction

Addition and subtraction require compatible dimensions. Values with unrelated units cannot be added or subtracted.

type Meter decimal<m>

type Second decimal<s>

let a: Meter := 10
let b: Meter := 5
let total := a + b

Both operands represent the same dimension, so the addition is meaningful.

The following expression is invalid:

let distance: Meter := 100
let duration: Second := 10
let invalid := distance + duration // Compile-time error.

Metres and seconds describe different dimensions. There is no meaningful result type for their addition.

Sec normally also preserves named-type identity. Two unrelated named types are not automatically interchangeable merely because they carry the same unit.

Multiplication and Division

Multiplication and division use unit algebra. Multiplication adds unit exponents, while division subtracts them.

Meter / Second -> decimal<m/s>
Speed * Second -> decimal<m>

Unlike addition and subtraction, multiplication and division may produce a different dimension from either operand.

type Meter decimal<m>
type Second decimal<s>
type Speed decimal<m/s>

let distance: Meter := 100
let duration: Second := 10
let speed := distance / duration

Dividing distance by duration derives the dimension m/s. If a matching named type is available, the compiler may infer that type for the result.

Unit Cancellation

Equal dimensions in the numerator and denominator cancel each other.

Meter / Meter -> decimal
Second / Second -> decimal
Money / Money -> decimal

The result is dimensionless because the unit exponents become zero.

let travelled: Meter := 50
let planned: Meter := 100
let completion := travelled / planned

completion is a plain dimensionless decimal, not a Meter.

Matching Derived Unit Types

When an arithmetic expression derives a unit dimension, Sec may resolve the result to an existing named type with that dimension.

type Meter decimal<m>
type Second decimal<s>
type Speed decimal<m/s>

let distance: Meter := 100
let duration: Second := 10
let speed := distance / duration

The derived dimension is m/s. Because Speed is declared with that dimension, the compiler may infer Speed as the result type.

This allows unit-aware arithmetic to remain concise without discarding semantic type information.

Anonymous Unit Values

An operation may derive a unit dimension for which no named type has been declared. In that case, the result can remain an anonymous unit-aware decimal type.

type Meter decimal<m>
type Second decimal<s>

let distance: Meter := 100
let duration: Second := 10
let value := distance / duration

If no named decimal<m/s> type exists, value may have the anonymous semantic type decimal<m/s>.

Anonymous unit types preserve dimensional correctness even when the programmer has not assigned a domain-specific name to every possible result.

Scalars and Unit Values

Multiplication or division by a dimensionless scalar preserves the unit dimension.

Money * int -> Money
Money / int -> Money
Meter * decimal -> Meter
Meter / decimal -> Meter

Example:

type Money decimal<SEK>

let unitPrice: Money := 49.90
let quantity: int := 3
let total := unitPrice * quantity

Multiplying by the dimensionless quantity does not change the currency dimension. The result may therefore remain Money.

Currently Unsupported Unit Algebra

Sec initially supports the unit operations needed for common linear calculations. Some mathematically possible dimensions are intentionally rejected until their syntax and use cases are fully defined.

Multiplying a currency by itself is currently invalid:

type Money decimal<SEK>

let a: Money := 10
let b: Money := 20
let invalid := a * b // Compile-time error.

The result would have the dimension SEK², which is not currently accepted as a useful currency type.

Explicit exponent notation such as m^2 or is not part of the current language version. Area and other exponent-based units will be documented when that syntax is finalized.

Complete Unit Example

type Meter decimal<m>
type Second decimal<s>
type Speed decimal<m/s>

fn CalculateSpeed(distance: Meter, duration: Second) Speed {
    return distance / duration
}

fn main() void {
    let distance: Meter := 100
    let duration: Second := 9.58
    let speed: Speed := CalculateSpeed(distance, duration)

    println(speed)
}

The function signature states exactly which dimensions are accepted and returned. Passing a Money value as the distance or a Meter value as the duration is rejected during compilation.

Numeric Type Inference

Numeric literals do not necessarily have a final concrete type by themselves. Their type may be determined by the declaration context. When no target type is present, Sec uses safe default types.

Integer Literals

An integer literal without target context is inferred as int.

let count := 10

The inferred type of count is int.

A target declaration may instead shape the literal into a named type:

type Speed int

let speed: Speed := 10

Decimal Literals

A decimal literal without target context is inferred as decimal, not float64.

let price := 3.14

The inferred type of price is decimal. This is the safe default because decimal arithmetic is exact within the supported decimal model and avoids accidental binary floating-point approximation.

Floating-point use must be explicit:

let measurement: float64 := 3.14

A decimal literal may also be shaped by a named decimal or unit type:

type Money decimal<SEK>

let price: Money := 3.14

Summary of Rules

  • A declaration such as type Speed int creates a new semantic type.
  • A named type is distinct from its underlying type.
  • Two named types remain distinct even when their underlying types are identical.
  • Untyped literals may initialize named types in declaration context.
  • Variables are never implicitly converted into named types.
  • Conversion from an expression or variable must be explicit, such as Speed(value).
  • Assignment to an existing named-type variable requires the exact named type.
  • Compound assignment follows the same identity and contract rules as normal assignment.
  • Contracts restrict which values may exist as a named type.
  • Compile-time-known contract violations are compile-time errors.
  • Runtime values require contract checking when explicitly converted.
  • Units are part of type semantics.
  • Addition and subtraction require compatible units.
  • Multiplication and division derive new dimensions algebraically.
  • Matching dimensions may resolve to a declared named type.
  • An unmatched derived dimension may remain an anonymous unit-aware decimal type.
  • Integer literals infer as int when no target context exists.
  • Decimal literals infer as decimal when no target context exists.