Clef Type Universe Specification

Overview

This document specifies the native type universe for Clef, the F# native compiler. The design follows ML/OCaml foundations while preserving familiar F# developer experience.

Core Principles

1. Familiar Design-Time Experience: Use F# type names (string, option, int), not foreign alternatives
2. Absolute Null-Freedom: Everything is voption<'T> - no null values anywhere
3. Null-Freedom Cascades Through APIs: Magic return values (-1, null, a throw) become voption returns

Part 1: Foundational Principles

1.1 Type Universe Axioms

The native type universe is built on three primitive concepts from ML/OCaml:

1. Products (tuples, records) - Combine multiple values into one
2. Sums (discriminated unions) - Choose between alternatives
3. Functions - Transform values

Everything else is derived from these primitives.

1.2 Memory Guarantees

• No implicit boxing: Value types remain on stack unless explicitly requested
• Deterministic layout: Memory representation is predictable and specified
• No null: All types are non-nullable by construction

1.3 Type Equivalences

Part 2: Primitive Types

CCS Resolution: See the CCS specification for how CCS resolves these types at compile-time.

OCaml Provenance: Primitives follow OCaml’s value-oriented representation (unboxed by default) while eliminating GC-oriented overhead. See Appendix E for detailed provenance analysis.

2.1 Unit

type unit = ()

OCaml Provenance: Identical to OCaml’s unit - the canonical “no information” type. In OCaml, () shares representation with [] (empty list) as the integer 0. In Clef, unit is truly zero-sized - not even allocated.

Usage:

let doSideEffect () : unit = Console.WriteLine "Hello"
let ignoredResult = ignore 42  // : unit
 

2.2 Boolean

type bool = true | false

OCaml Provenance: OCaml represents booleans as unboxed integers (false = 0, true = 1). Clef preserves this representation but uses a full byte for alignment efficiency in arrays and structs.

Booleans occupy 1 byte rather than 1 bit because:

1. Sub-byte addressing is inefficient on modern hardware
2. Array indexing requires byte-addressable elements
3. Cache line efficiency favors byte alignment

No Boolean Coercion:

// ILLEGAL in Clef - no implicit int-to-bool
let x = if 1 then "yes" else "no"  // Error: expected bool, got int

// LEGAL - explicit comparison
let x = if 1 <> 0 then "yes" else "no"

2.3 Integer Kind

There is one integer kind, int, with a dimension (int<m>, Units of Measure). Its width is not a property of the type: it is derived from the value’s analysed range and selected from the integer representations the platform declares (Width Inference §3, NTU Types, Platform Bindings). Signedness is a fact of the range: a non-negative range spends no sign bit.

Representation rules:

1. No width-named integer type. int8, int16, int32, int64, their unsigned forms, byte, sbyte, uint, nativeint and unativeint are not Clef types. A width appears only in a declaration the compiler reads: the platform description and a boundary declaration (a wire-schema field, an MMIO register, a C ABI parameter in a binding descriptor, an endpoint contract). OCaml’s Int32.t and Int64.t have no counterpart; interop widths belong to the descriptor, and the Clef signature beside it says int.

2. No GC tagging overhead: Unlike OCaml’s 63-bit tagged integers (which reserve 1 bit for runtime GC discrimination), Clef integers use full precision. Compile-time type safety eliminates the need for runtime type tags.

   System	int precision	Tag overhead
   OCaml (64-bit)	63 bits	1 bit for GC
   F# (.NET)	32 bits	None (boxed separately)
   Clef	the width its range requires; the platform’s declared word at an ABI boundary	None

3. An address is not an integer. nativeint-as-pointer is not denotable (FFI Boundary §1); addresses live in Ptr<'T, Region, Access>, Mmio and CHandle<'T>, which realise as index. An integer of the platform’s pointer width (a size, an offset handed across a C ABI) is int at a boundary whose declared representation is the description’s Pointer width.

4. Overflow does not occur on analysed ranges. Arithmetic’s result has an analysed range and a representation selected to cover it. An intended reduction or saturation is written as arithmetic, x % 2^n or clamp lo hi x, with the range that arithmetic gives it (Width Inference §7). A range a boundary’s declared representation does not cover SHALL produce the hard coverage error CCS8012 at design time (Numeric Selection §5). Warning policy SHALL NOT authorize failed coverage.

Alignment: the alignment of an integer is that of the representation selected for it, declared by the platform description; arrays of narrow-range integers pack accordingly, per element range (Numeric Selection §5, per-coefficient selection).

JSIR pathway (JavaScript Substrate profile): the host number model is IEEE-754 binary64 with exact integers to 2⁵³. Integer realization on this pathway, including the wide-integer mechanism for widths above 53 bits, is specified in Width Inference §8.

2.4 Real Kind

There is one real kind, float, with a dimension (float<m>). Its representation, IEEE-754 binary32 or binary64, a posit, or a fixed-point format, is selected from the value’s analysed range among the real representations the platform declares (Numeric Selection §2); it is never fixed by a type name, and float32, single, double and float64 are not Clef types.

Representation rules:

1. float carries no representation claim. A bare float with an unobservable range selects IEEE f64, the no-bet representation, without a diagnostic, and still carries range propagation; a dimensioned real with an unobservable range is a diagnostic at the dimensioning seam (Numeric Selection §6).

2. IEEE 754 compliance when IEEE is the selected representation: where the selected representation is f64/f32, all floating-point operations follow IEEE 754 semantics including NaN propagation, infinities, and signed zeros.

3. No implicit real-integer change of kind: float x takes an integer to a real, exactly where the selected real representation holds the range; floor, ceiling, round and truncate take a real to an integer, each with its range image (Width Inference §7).

   let x : float = 42    // Error: expected float, got int
   let x : float = 42.0  // OK
   let x : float = float 42  // OK, exact: [42, 42]

Special Values:

let inf = infinity        // Positive infinity
let ninf = -infinity      // Negative infinity
let nan = nan             // Not a Number
let isNan x = x <> x      // NaN property: NaN ≠ NaN

2.5 Character

type char = (* Unicode scalar value *)

Characters are UTF-32 codepoints (4 bytes), not UTF-16 code units.

Rationale:

1. String encoding is UTF-8: Clef strings are UTF-8 memref<?xi8> views (see Part 4.1)
2. Iteration yields codepoints: When iterating over a UTF-8 string, each char is a decoded Unicode scalar value
3. No surrogate pairs: Unlike UTF-16, a single char always represents a complete character
4. Consistency with Rust: Rust’s char is also a 32-bit Unicode scalar value

OCaml Divergence: OCaml’s char is a single byte (Latin-1 only, 0-255). Clef explicitly supports full Unicode.

String-Character Interaction:

let s = "Hello, 世界!"  // UTF-8 string

// Iteration yields Unicode codepoints
for c in String.chars s do
    printfn "U+%04X" (int c)  // U+0048, U+0065, ..., U+4E16, U+754C, U+0021

// Indexing by codepoint (not byte offset)
let c = String.charAt 7 s  // voption.Some '世' (U+4E16)

// Byte length vs character length
String.byteLength s   // 15 bytes (UTF-8 encoded)
String.charLength s   // 10 characters
 

Invalid Codepoints: Surrogate codepoints (U+D800 to U+DFFF) are not valid char values. Attempting to construct such values results in a compile-time or runtime error.

Part 3: Structural Types

Foundation: All composite types are built from products (tuples, records) and sums (discriminated unions). This follows ML/OCaml tradition.

OCaml Provenance: OCaml’s structural assembly semantics are preserved - products are contiguous, sums are tagged. However, OCaml’s runtime block headers (for GC) are eliminated. See Appendix E.

3.1 Tuples (Anonymous Products)

let pair : int * string = (42, "hello")
let triple : int * string * float = (1, "x", 3.14)

Memory Layout:

Tuple: int * string (64-bit platform)
┌─────────────┬─────────────────────────────────────┐
│ int (word)  │ string (memref<?xi8> view: 2 words) │
└─────────────┴─────────────────────────────────────┘
     8 bytes                 16 bytes                 = 24 bytes total

OCaml Comparison:

Tuples are unboxed - no heap allocation, no indirection, no headers. Fields are laid out contiguously with natural alignment.

Padding and Alignment Rules:

// This tuple has internal padding for alignment
let t : int8 * int64 * int8 = (1y, 100L, 2y)

Memory Layout (with padding):
┌────────┬─────────┬──────────┬────────┬─────────┐
│ int8   │ padding │ int64    │ int8   │ padding │
└────────┴─────────┴──────────┴────────┴─────────┘
  1 byte   7 bytes   8 bytes    1 byte   7 bytes  = 24 bytes

Cache Considerations:

3.2 Records (Named Products)

type Person = { Name: string; Age: int }
type Point = { X: float; Y: float }

Memory Layout:

Record: Person (64-bit platform)
┌─────────────────────────────┬─────────────┐
│ Name: string (2 words)      │ Age: int    │
└─────────────────────────────┴─────────────┘
           16 bytes               8 bytes    = 24 bytes total

Callable fields. A function field or FnPtr<'F> field holds a callable component, not a code address. Its data placement contains only the settled selector and environment view where needed. A single-alternative field without an environment needs no component storage; a captured closure still retains its environment. Formation, contract and lifetime dependencies survive field selection and copies. This is a Clef layout. A C structure crossing needs the separately admitted projection described by FFI Boundary §3.6.

OCaml Comparison:

Mutable Fields:

type MutablePoint = { mutable X: float; mutable Y: float }

Cache-Aware Record Design:

Field grouping can improve locality where an access profile justifies it. The following is an illustrative layout for a target with 64-byte cache lines and the displayed admitted field sizes; it is not a portable layout guarantee. Alignment, padding and actual field representations require target facts.

// HOT fields together - accessed frequently
type OptimizedActor = {
    // Hot path - first cache line (64 bytes)
    MessageCount: int64          // 8 bytes, offset 0
    LastProcessed: int64         // 8 bytes, offset 8
    State: ActorState            // 16 bytes, offset 16
    mutable Flags: uint32        // 4 bytes, offset 32
    // padding: 28 bytes to fill cache line
    
    // Cold path - second cache line
    Name: string                 // 16 bytes, offset 64
    CreatedAt: int64             // 8 bytes, offset 80
    Config: ActorConfig          // varies
}

False Sharing Prevention:

Independently written fields can benefit from separate cache lines when the actual sharing and target topology justify it. For each [<CacheLineAligned>] field, the implementation SHALL align the field to the selected target’s declared cache-line boundary. A false-sharing separation claim SHALL additionally establish object extent, adjacent allocation separation, alias behavior and ownership for the relevant accesses.

[<Struct>]
type ThreadCounters = {
    [<CacheLineAligned>]  // Align to the target's declared cache-line boundary
    mutable Counter1: int64
    
    [<CacheLineAligned>]  // Separate cache line
    mutable Counter2: int64
}

3.3 Discriminated Unions (Named Sums)

type Shape =
    | Circle of radius: float
    | Rectangle of width: float * height: float
    | Point  // No payload
 

Memory Layout:

Union: Shape (64-bit platform)
┌──────────┬─────────┬────────────────────────────────────┐
│ Tag (i8) │ padding │ Payload (size of largest variant)  │
└──────────┴─────────┴────────────────────────────────────┘
   1 byte    7 bytes              16 bytes                 = 24 bytes total

OCaml Comparison:

Tag Assignment (declaration order):

type Color = Red | Green | Blue
// Red = 0, Green = 1, Blue = 2

type Result<'T, 'E> = Ok of 'T | Error of 'E
// Ok = 0, Error = 1
 

Variant-Specific Layouts:

type Message =
    | Ping                              // Tag only: 1 byte + padding
    | Data of payload: array<byte>      // Tag + memref<?xi8> view: 24 bytes on x86-64 (1 tag + 7 pad + 2 platform words); 12 bytes on thumbv8m
    | Error of code: int * msg: string  // Tag + int + string: 1 + 7 + 8 + 16 = 32 bytes
 

Union: Message (largest variant determines size)
┌──────────┬─────────┬────────────────────────────────────┐
│ Tag (i8) │ padding │ 32 bytes (Error variant size)      │
└──────────┴─────────┴────────────────────────────────────┘
= 40 bytes total (all variants padded to this size)

Single-Case Unions (newtypes):

type UserId = UserId of int
type Email = Email of string

UserId = int (no wrapping, no tag)
┌─────────────┐
│ int (word)  │
└─────────────┘
    8 bytes

Recursive Unions:

type List<'T> = Nil | Cons of head: 'T * tail: List<'T>
type Tree<'T> = Leaf of 'T | Node of left: Tree<'T> * value: 'T * right: Tree<'T>

Cons cell: List<int>
┌──────────┬─────────┬──────────┬──────────────────────────┐
│ Tag (i8) │ padding │ head: T  │ tail: index (arena link) │
└──────────┴─────────┴──────────┴──────────────────────────┘
   1 byte    7 bytes   8 bytes            8 bytes           = 24 bytes

Layout obligations: VC-LINK on every link word, VC-GUARD (the discriminant test, tag = Cons or height ≠ 0, dominates every read of a payload slot on the saturated graph), and the sentinel’s residence and immutability are quantifier-free at saturation over the graph’s literals: QF_LIA plus a dominance check, no quantifiers. The AVL balance invariant of §5.4 and §5.5 and the list algebra of §5.3 are schema lemmas proven once per recipe shape, never a per-program fixpoint. Every link is always a valid node, so no algorithm over a recursive union has an absence branch: recursion terminates at the sentinel, and a link load is one memref.load of an index.

Pattern Matching Compilation:

Pattern matching on DUs compiles to efficient branch tables:

match shape with
| Circle r -> computeCircleArea r
| Rectangle (w, h) -> w * h
| Point -> 0.0

Compiles to:

switch (shape.tag) {
    case 0: goto circle_branch;   // Circle
    case 1: goto rect_branch;     // Rectangle
    case 2: goto point_branch;    // Point
}

Exhaustiveness: Pattern matching is verified exhaustive at compile time. Missing cases produce warnings/errors.

Part 4: Reference Types

Principle: Reference types are memref views: the buffer is the value and its length is the view’s dimension. No null; empty is a view of dimension 0.

CCS Resolution: See the CCS specification for compiler-level type resolution.

4.1 String

let greeting : string = "Hello, World!"
let empty : string = ""

Memory Layout (memref<?xi8>, UTF-8):

string = memref<?xi8>
┌────┬────┬────┬─────┬──────┐
│ b0 │ b1 │ b2 │  …  │ bn-1 │   the UTF-8 bytes: the buffer is the value
└────┴────┴────┴─────┴──────┘
  dimension n = byte length, carried by the view; there is no separate length field

Platform word: Inside an aggregate (a tuple slot, a record field, a union payload) the view occupies two platform words, its buffer and its dimension: 16 bytes on x86-64 (8-byte word), 8 bytes on thumbv8m/M33 (4-byte word). The bytes themselves are placed by the lifetime lattice of Closure Representation §3.3; a string literal is program-lifetime and immutable, so it resides in the platform’s declared immutable program-lifetime space (rodata on an ELF target, flash on an MCU).

Why UTF-8?

1. Native interop - Rust, C, and most systems APIs use UTF-8
2. Compact - 1 byte per ASCII character
3. Web/JSON native - no transcoding overhead
4. Embedded-friendly - no UTF-16 surrogate handling

Character Iteration (codepoints, not bytes):

// Iterating over Unicode scalar values
for c in String.chars s do
    printfn "%c" c  // c : char (UTF-32 codepoint, 4 bytes)
 

Zero-Copy Slicing: A substring is a memref.subview of the same buffer with an adjusted offset and dimension; no bytes are copied.

Byte-unit conversions: String.fromBytes : array<int> -> string requires byte-range and UTF-8-validity evidence. It constructs an immutable snapshot; String.toBytes : string -> array<int> returns an independent mutable snapshot of those UTF-8 bytes. Neither direction exposes a mutable alias of string storage. See the conversion contract.

JSIR pathway (JavaScript Substrate profile): string is realized as a host string, whose internal encoding is UTF-16 code units. The observable semantics of this section bind unchanged: String.byteLength SHALL return the UTF-8 byte count, String.chars SHALL yield Unicode scalar values, and indexing SHALL be by codepoint. The memref<?xi8> layout and its cost figures are properties of layout-realizing pathways and do not bind on this pathway (Backend Lowering Architecture §4.5).

See: Appendix E for encoding comparison with OCaml (Latin-1) and .NET (UTF-16).

API Changes (Null-Freedom Cascades):

4.2 Array

let numbers : array<int> = [| 1; 2; 3; 4; 5 |]
let empty : array<int> = [| |]

Memory Layout (memref<?xT>):

array<'T> = memref<?xT>
┌──────┬──────┬──────┬─────┬────────┐
│ e0   │ e1   │ e2   │  …  │ en-1   │   the elements: the buffer is the value, n * sizeof<'T> bytes, contiguous
└──────┴──────┴──────┴─────┴────────┘
  dimension n = length, carried by the view; there is no separate length field

Platform word: Inside an aggregate the view occupies two platform words, its buffer and its dimension: 16 bytes on x86-64, 8 bytes on thumbv8m/M33 (4-byte word). The elements reside in the buffer, placed by the lifetime lattice of Closure Representation §3.3.

Monomorphized Layout: Unlike uniform representations that box generic elements, Clef arrays are monomorphized - array<int> stores unboxed integers contiguously. Sequential access is cache-optimal (8 int64 or 16 int32 values per 64-byte cache line).

Fixed Size After Creation:

let arr = Array.create 10 0  // 10 elements, all 0
// arr.Length is immutable - no resizing
 

API Changes (Null-Freedom Cascades):

Array Module Intrinsics (CCS Layer 1):

These operations are fundamental to the array type and are emitted directly by CCS. They cannot be expressed in pure F# because they require memory allocation and element size knowledge.

Allocation Semantics: Arrays are allocated in the current memory region (stack arena or actor arena). The allocation strategy is determined by the memory region context, not by the Array function.

4.3 Span and ReadOnlySpan

let span : Span<int> = Span(arr, 2, 3)  // View into arr[2..4]
let roSpan : ReadOnlySpan<byte> = ReadOnlySpan(bytes)

Memory Layout (borrowed view):

Span<'T> = memref<?xT> view with a dynamic offset
┌──────────┬──────────┬─────┬────────────┐
│ e[off]   │ e[off+1] │  …  │ e[off+n-1] │   a window into the source buffer: nothing owned, nothing copied
└──────────┴──────────┴─────┴────────────┘
  offset off and dimension n carried by the view

Zero-Copy Views: Spans provide borrowed views into arrays, strings, and memory regions without allocation. The stack-only constraint prevents lifetime escape (similar to Rust’s slice borrowing). Maps directly to MLIR memref with dynamic offset.

Note: Leverage FSharp.Core Span types - already stack-allocated and native-friendly.

Part 5: Parameterized Types

Principle: Parameterized types follow familiar F# syntax. CCS resolves native semantics at compile-time.

CCS Resolution: See the CCS specification for option type resolution and null-free guarantees.

5.1 Option

let maybeValue : int option = Some 42
let nothing : string option = None

Memory Layout (stack-allocated tagged union):

option<'T>  (voption semantics)
┌──────────┬────────────────────┐
│ Tag (i8) │ Payload: 'T        │
└──────────┴────────────────────┘
   1 byte     sizeof<'T>         + padding

Stack-Only Guarantee: Unlike heap-allocated options (cf. OCaml blocks, .NET reference types), Clef options are always stack-allocated with no GC involvement. This enables predictable memory layout for embedded targets and eliminates heap fragmentation from frequent option use.

JSIR pathway (JavaScript Substrate profile): the stack layout above is a property of layout-realizing pathways. On the JSIR pathway, option<'T> is realized erased or reified under a proof discipline, specified in Option Operations Representation §2.1.

See: Appendix E for detailed OCaml/Rust comparison.

CCS Resolution:

// User writes familiar F# syntax:
let x : int option = Some 42
let y : int option = None

// CCS compiles with voption<int> semantics:
// - Stack allocated
// - Tag-based discrimination
// - No null anywhere
 

API (Null-Freedom Cascades):

Note: CCS provides native option semantics directly - option<'T> maps to stack-allocated voption at compile time.

5.2 Result

let success : Result<int, string> = Ok 42
let failure : Result<int, string> = Error "not found"

Memory Layout (tagged union):

Result<'T, 'E>
┌──────────┬────────────────────────────────────┐
│ Tag (i8) │ Payload: max(sizeof<'T>, sizeof<'E>)│
└──────────┴────────────────────────────────────┘

Stack Allocation: Like option, Result is always stack-allocated with zero heap overhead.

Why Result Over Exceptions: Result makes error handling explicit in type signatures, enables compile-time exhaustiveness checking, has zero runtime overhead, and can cross FFI boundaries via BAREWire. Exceptions are not supported for control flow in Clef.

Preferred Error Handling: Result is the idiomatic error handling pattern in Clef. Exceptions are not supported for control flow.

// Idiomatic error handling
let divide x y : Result<int, string> =
    if y = 0 then Error "division by zero"
    else Ok (x / y)

// Chaining with Result.map, Result.bind
divide 10 2
|> Result.map (fun x -> x * 2)
|> Result.defaultValue 0

5.3 List

let numbers : int list = [1; 2; 3; 4; 5]
let empty : int list = []

Memory Layout (cons cells):

list<'T>  (tagged node: Empty | Cons)
┌──────────┬─────────┬────────────────────┬──────────────────────────┐
│ tag: i8  │ padding │ head: 'T           │ tail: index (arena link) │
└──────────┴─────────┴────────────────────┴──────────────────────────┘
  1 byte   to align       sizeof<'T>             platform word
                                                (8 bytes x86-64,
                                                 4 bytes thumbv8m)

Platform word: tail is an index (arena link), an arena-relative offset into the arena buffer the list lives in: one platform word, 8 bytes on x86-64 and 4 bytes on thumbv8m/M33. It carries VC-LINK, 0 <= i < extent(arena), with i = 0 the sentinel at offset 0 of that arena, discharged at saturation before witnessing. A link load is one memref.load of an index.

Arena Allocation: List cons cells are allocated in arenas, or in the platform’s declared program-lifetime space for program-lifetime values, cited by name from the platform description (rodata/data on an ELF target, flash/SRAM on an MCU, constant memory on a GPU, initialised BRAM on an FPGA; not GC heap), providing better cache locality and batch deallocation at scope end. The immutable structure enables structural sharing as in OCaml. On a heap-free target a cons cell whose lifetime classifies as genuinely dynamic is a compile-time lifetime error, not a silent heap allocation.

When to Use:

• Pattern matching on head/tail
• Recursive algorithms
• Functional transformations (map, filter, fold)

When NOT to Use (prefer array):

• Random access by index
• Performance-critical loops
• Large collections with mutations

5.4 Map

let lookup : Map<string, int> = Map.ofList [("a", 1); ("b", 2)]
let empty : Map<int, string> = Map.empty

Memory Layout (AVL tree nodes):

Map<'K, 'V>  (AVL tree node)
┌────────────────────┬────────────────────┬───────────────────────────┬───────────────────────────┬────────────┐
│ key: 'K            │ value: 'V          │ left: index (arena link)  │ right: index (arena link) │ height: i8 │
└────────────────────┴────────────────────┴───────────────────────────┴───────────────────────────┴────────────┘
     sizeof<'K>           sizeof<'V>             platform word               platform word            1 byte

Platform word: left and right are each an index (arena link), an arena-relative offset into the arena buffer the tree lives in: one platform word each, 8 bytes on x86-64 and 4 bytes on thumbv8m/M33. Each carries VC-LINK, 0 <= i < extent(arena), with i = 0 the sentinel at offset 0 of that arena, discharged at saturation before witnessing. A link load is one memref.load of an index.

AVL Balance Property: Height difference between left and right subtrees is at most 1. Rebalancing occurs on Map.add when this property would be violated.

When to Use:

• Key-value associations with O(log n) lookup
• Ordered iteration by key
• Immutable dictionary semantics

When NOT to Use (prefer Dictionary or array):

• Frequent updates (mutable dictionary better)
• Small fixed key sets (array with enum index)
• Hash-based O(1) lookup needed

See: Map Representation for detailed AVL algorithms and HOF specifications.

5.5 Set

let numbers : Set<int> = Set.ofList [1; 2; 3]
let empty : Set<string> = Set.empty

Memory Layout (AVL tree nodes):

Set<'T>  (AVL tree node)
┌────────────────────┬───────────────────────────┬───────────────────────────┬────────────┐
│ value: 'T          │ left: index (arena link)  │ right: index (arena link) │ height: i8 │
└────────────────────┴───────────────────────────┴───────────────────────────┴────────────┘
     sizeof<'T>             platform word               platform word            1 byte

Platform word: left and right are each an index (arena link), an arena-relative offset into the arena buffer the tree lives in: one platform word each, 8 bytes on x86-64 and 4 bytes on thumbv8m/M33. Each carries VC-LINK, 0 <= i < extent(arena), with i = 0 the sentinel at offset 0 of that arena, discharged at saturation before witnessing. A link load is one memref.load of an index.

Relationship to Map: Set<'T> is structurally equivalent to Map<'T, unit> but with optimized layout (no value field).

When to Use:

• Membership testing with O(log n) lookup
• Ordered unique elements
• Set operations (union, intersect, difference)

When NOT to Use (prefer HashSet or array):

• Very frequent membership tests (hash-based O(1) better)
• When order doesn’t matter and hash is cheaper

See: Set Representation for detailed AVL algorithms and HOF specifications.

Part 6: Function Types

Principle: Functions are first-class values. Explicit inline lifts a scope-bounded buffer into the caller’s frame so a returned view stays valid.

6.1 Pure Functions

let add : int -> int -> int = fun x y -> x + y
let apply : ('a -> 'b) -> 'a -> 'b = fun f x -> f x

Representation Strategies:

6.2 Closure Representation

When a function captures variables from its environment:

let makeAdder n =
    fun x -> x + n  // Captures 'n'
 

Form — two SSA values, never packed (Closure Representation §6.3):

Closure = (fn, env)
fn:  a function value (func.constant), not stored as data
env: ┌─────────────────────┐
     │ captured values     │   memref<Exi8>, E = sizeof<env>, literal at saturation
     └─────────────────────┘

Closure Allocation: The environment is allocated on stack or in an arena, or in the platform’s declared program-lifetime space for program-lifetime values, cited by name from the platform description (rodata/data on an ELF target, flash/SRAM on an MCU, constant memory on a GPU, initialised BRAM on an FPGA; not GC heap); fn is a func.constant and is never stored as data. Small closures (<64 bytes) fit within one cache line for efficient invocation. On a heap-free target a closure whose lifetime classifies as genuinely dynamic is a compile-time lifetime error, not a silent heap allocation.

6.3 Inline Semantics

Functions are real functions unless marked inline, and inline is a semantic tool, not an optimization hint. CCS expands a body at its call sites only when the definition is explicitly marked inline, and the keyword is mandatory in exactly two cases:

Everywhere else inline is discouraged, and platform-library code stays real functions: Clef targets many substrates through MLIR, and the optimizer decides inlining with whole-program context that a source-level inline binds away early.

let inline dot (a: ^V) (b: ^V) = ...        // required: SRTP generalization
let inline readln () : string = ...         // required: returns a view over a stack buffer it fills
let double x = x * 2                        // a real function; the optimizer may inline it

6.4 Partial Application

let add x y = x + y
let add5 = add 5  // Partial application
 

Representation: Creates a closure capturing applied arguments:

add5 = (fn, env)
fn:  func.constant @add_impl
env: { x = 5 } : memref<Exi8>

Currying Optimization: Fully-applied curried calls compile to direct multi-argument calls (no intermediate closures). Partial application creates flat closures capturing applied arguments. Higher-order uses like List.map f are typically inlined at call sites.

See: ClefExpr § 5.2 Curried Call Flattening for the normative specification of how the SemanticGraph represents curried applications.

Part 7: Mutable State

Principle: Mutable state is explicit and controlled. All mutation is visible in the type system or syntax.

7.1 Ref Cells

let counter : int ref = ref 0
counter := !counter + 1  // Mutation
let value = !counter     // Dereference
 

Memory Layout:

ref<'T>
┌────────────────────┐
│ contents: 'T       │
└────────────────────┘
    sizeof<'T>

Stack/Arena Allocation: Refs are allocated on stack or in arenas, or in the platform’s declared mutable program-lifetime space for program-lifetime values (data on an ELF target, SRAM on an MCU; not GC heap), eliminating allocation pressure in loops and providing predictable memory behavior for embedded targets. On a heap-free target a ref whose lifetime classifies as genuinely dynamic is a compile-time lifetime error, not a silent heap allocation.

7.2 Mutable Bindings

let mutable x = 0
x <- x + 1  // Direct mutation
 

All references and capturing closures SHALL retain the same mutable cell identity. Capture SHALL NOT read the cell to substitute a snapshot of its current contents. The cell’s storage SHALL outlive every admitted reference, including references held by closures. Placement SHALL follow the lifetime classification and the selected target’s declared storage; an uncovered lifetime SHALL produce a compile-time lifetime diagnostic.

7.3 Mutable Record Fields

type Counter = { mutable Value: int }

let c = { Value = 0 }
c.Value <- c.Value + 1

Cache Line Isolation: For concurrent access, isolate frequently-written mutable fields using [<CacheLinePadded>] to prevent false sharing.

Part 8: Memory Region Types (UMX Integration)

Core Fidelity Principle: Memory region types are intrinsic to Clef - as fundamental as voption. They carry semantic meaning through the entire compilation pipeline, guiding every memory layout decision. Fidelity makes ALL memory layout decisions - MLIR/LLVM never determine layout.

Erasure at Last Lowering: These types ARE erased - but at the last possible lowering stage, after Fidelity has made all memory layout decisions. By the time code reaches LLVM, “the type information that guided every transformation has done its job and compiled away to nothing.” This is the entire point of “Fidelity” - preserving type fidelity through compilation so the F# compiler controls memory layout.

CCS Enforcement: See the CCS specification for region constraint enforcement and diagnostic codes.

8.1 Memory Regions

Memory region types define where memory lives and how it behaves. They guide Fidelity’s code generation decisions throughout the pipeline:

// These types guide memory layout decisions through compilation
type Stack      // Thread-local, automatic lifetime
type Arena      // Compiler-managed bulk allocation
type Peripheral // Memory-mapped I/O (volatile semantics)
type Sram       // General-purpose RAM
type Flash      // Read-only storage
 

Why This Matters - The “Fidelity” in Fidelity Framework:

CCS/Baker settles memory layout and its proof premises on the PSG. Memory region types:

1. Carry semantic meaning through the entire compilation pipeline
2. Carry settled access contracts to Alex — Composer’s backend realizes Peripheral access as the target’s volatile operations
3. Determine allocation strategy - Stack vs Arena vs explicit
4. Enable compile-time safety - region mismatches are type errors
5. Preserve their required consequences through lowering — every consumed fact retains its proof correspondence

Alex passively witnesses the settled storage and access forms. Composer’s backend realizes those forms without reconstructing source layout or ownership.

8.2 Access Kinds

Access kinds are also intrinsic - they determine what operations are legal AND affect code generation:

// Intrinsic access kind types
type ReadOnly   // Input registers, flash, const data
type WriteOnly  // Output registers, write-only buffers
type ReadWrite  // General mutable access
 

8.3 Region-Typed Pointers

Pointers carry region and access information as part of their type:

type Ptr<'T, 'Region, 'Access>

// Examples - region and access are part of the type, not annotations
let gpioReg : Ptr<uint32, Peripheral, ReadWrite> = ...
let flashData : Ptr<byte, Flash, ReadOnly> = ...
let stackBuffer : Ptr<int, Stack, ReadWrite> = ...

Compile-Time Safety:

// ERROR: Cannot write to readOnly pointer
let writeFlash (p: Ptr<byte, Flash, ReadOnly>) =
    Ptr.write p 0uy  // Compile error!

// OK: Can read from readOnly
let readFlash (p: Ptr<byte, Flash, ReadOnly>) =
    Ptr.read p  // OK
 

Cache Behavior: Stack, Arena, Sram, and Flash regions are cacheable with normal load/store semantics. Peripheral access bypasses cache and uses memory barriers - essential for hardware registers where timing and order matter.

8.4 Arena as CCS Intrinsic Type

Arena is a CCS intrinsic type.

Schematic Type Notation:

Arena<'lifetime>

Here 'lifetime denotes the arena’s inferred lifetime identity in the coeffect domain. This notation states the relationship used by the operation signatures below; it does not declare source lifetime-parameter syntax. Lifetime orderings SHALL follow Memory Regions, independently of the physical-dimension algebra.

Memory Layout (NTUCompound 3):

Arena<'lifetime>
┌─────────────────┬─────────────────┬─────────────────┐
│ Base: index     │ Capacity: index │ Position: index │
└─────────────────┴─────────────────┴─────────────────┘
     8 bytes           8 bytes           8 bytes       = 24 bytes (64-bit)

Platform word: Each field is one platform word, so the struct is 3 words. The 24-byte total is the x86-64 instance; on thumbv8m/M33 (4-byte word) the struct is 12 bytes. Base here is an internal compiler field, never user-denotable.

CCS Intrinsic Operations:

Usage Pattern:

// Arena backed by a bounded stack array
let arenaMem : array<byte> = Array.zeroCreate 4096
let mutable arena = Arena.fromBuffer arenaMem

// Allocate from arena
let buffer = Arena.alloc &arena 256

// Arena freed when stack frame exits
 

Byref Parameter: Operations that mutate arena state (alloc, reset) take Arena<'lifetime> byref to enable in-place position updates without copying the three-word struct (24 bytes on x86-64, 12 bytes on thumbv8m/M33).

See: memory-regions.md for detailed Arena semantics.

8.5 Hardware Peripheral Descriptors

See: Farscape documentation for peripheral binding generation.

[<PeripheralDescriptor("GPIO", 0x48000000UL)>]
type GPIO_TypeDef = {
    [<Register("MODER", 0x00u, "rw")>]
    MODER: Ptr<uint32, peripheral, readWrite>
    
    [<Register("IDR", 0x10u, "r")>]
    IDR: Ptr<uint32, peripheral, readOnly>
    
    [<Register("ODR", 0x14u, "rw")>]
    ODR: Ptr<uint32, peripheral, readWrite>
}

Part 9: Coeffects and Resource Tracking

Coeffects record the context required by a computation. Their carriage and preservation are specified in Program Semantic Graph. Resource ownership and cleanup follow the Memory Regions and Closure Representation contracts.

Part 10: Interactive Development (clefx)

Interactive Development specifies the native session contract. The interactive CLI is named clefx, matching the .clefx script extension.

10.1 Interactive Session Types

Session-local and dependency definitions must be checked by CCS under the same native type rules as project source. A session must retain the revision, compiler-generation and target identities of those judgments.

10.2 Lifetimes in Interactive Mode

The ordinary lifetime and memory-region contracts apply to retained interactive values. A session must establish storage and code lifetimes before admitting retained values, reset or unloading.

10.3 Native Execution and the Compiler Host

Native interactive execution follows CCS/Baker construction, the versioned semantic graph, Alex witnessing, admitted MLIR and LLVM JIT invocation. There is no separate interpreter or hybrid execution mode. A .NET or FSI bootstrap host may execute the compiler implementation and inspect its data; FSI never supplies Clef evaluation or native value representation.

10.4 Script File Type Semantics

.clefx scripts use the same native type universe as .clef modules. The extension does not introduce managed string, option or object types.

10.5 Cross-Compilation Type Considerations

Type layouts, numeric widths, index width and pointer-handle representation follow the selected target’s declarations and ABI. They do not inherit the compiler host’s layout. Checking or inspecting a target-dependent type is separate from executing code for that target; native invocation requires a compatible execution environment. Target changes invalidate dependent session judgments and execution products.

Appendix A: Type Mapping to MLIR

Appendix B: OCaml Type System Reference

Source: OCaml Basic Data Types, Memory Representation, Real World OCaml

B.1 OCaml Uniform Memory Representation

OCaml uses a “uniform memory representation” where every variable is a single word containing either an immediate integer or a pointer. The runtime distinguishes them using the lowest bit:

• Bit = 1: Integer value (unboxed)
• Bit = 0: Pointer to heap-allocated data

This tagging allows integers to remain “unboxed” (stored directly without heap allocation), making them fast and register-friendly. The tradeoff is losing one bit of precision in integer values.

B.2 OCaml Primitive Types

B.3 OCaml Composite Types

B.4 Key OCaml Design Decisions Clef Diverges From

Appendix C: Comparison with OCaml/F#/Rust

Appendix D: Migration from Shadow Types

Note: CCS provides native type resolution directly. No shadow types or library workarounds are needed.

FSharp.Core Types Leveraged

CCS Type Resolution

CCS (Clef Compiler Service) resolves types to native representations at the source:

• string → UTF-8 memref<?xi8>
• option<'T> → voption (stack-allocated)
• array<'T> → memref<?xT> with native element layout
• int → platform word

Appendix E: OCaml Provenance and Fidelity Extensions

Design Philosophy: Clef draws provenance from OCaml’s direct memory layout idioms - concepts that F#/.NET lacks entirely because the CLR abstracts memory away. However, OCaml is desktop-centric and non-cache-aware. Fidelity extends OCaml’s foundation with modern hardware realities while incorporating Rust’s RAII principles.

E.1 What OCaml Provides

OCaml contemplates direct memory layout in ways F#/.NET never does:

These concepts form the bedrock of Clef’s type universe. The structural assembly semantics, deterministic tag assignment, and explicit-length model are adopted with minimal modification.

E.2 What OCaml Lacks

OCaml’s desktop-centric, non-cache-aware limitations that Clef explicitly diverges from:

OCaml assumes a desktop environment with ample RAM and a garbage collector managing memory. Clef targets the full spectrum from microcontrollers to GPU clusters.

E.3 Rust RAII Guideposts

Rust’s ownership model provides valuable guideposts, adapted to F#’s functional idioms:

Rust’s insight that ownership can be tracked statically is preserved, but expressed through F#’s type system rather than explicit lifetime annotations.

E.4 Fidelity Extensions Beyond Both

Fidelity’s cache-aware compilation uses source demand, admitted layout and target topology together. Implementations SHALL satisfy the following realization and evidence obligations for the optimizations they apply:

Cache Hierarchy Awareness

Memory Hierarchy Management

An assessment can compare a bounded active footprint with capacities declared by the selected CPU profile. It SHALL distinguish an established layout/extent fact from a profile-dependent performance estimate. A report such as “fits the declared L1 capacity under these live-instance assumptions” does not mean “L1-resident,” and exceeding a capacity does not by itself authorize cache-bypass instructions. Capacity constants and estimated strategies belong to the target profile and selected realization, not universal source-language thresholds.

Call-by-need can reduce work and the active footprint by avoiding undemanded computations; sharing can also retain data longer. Eager evaluation, fusion, prefetch and batching require demand/effect/lifetime preservation, followed by target-specific evidence for the claimed performance improvement. Informational advice should identify the target/profile and assumptions. A missing performance estimate is not a language error; a violated admission or correctness obligation retains its required diagnostic.

Processor-Specific Optimization

Hardware Memory Regions

Clef introduces memory regions unknown to both OCaml and Rust:

E.5 The Synthesis

Clef’s type universe represents a synthesis:

1. From OCaml: Products, sums, functions as primitives; value-oriented assembly; explicit-length views; no null
2. Set Aside from OCaml: GC tagging overhead; desktop assumptions; runtime discrimination
3. From Rust: Deterministic cleanup; ownership tracking (adapted to coeffects); RAII semantics
4. Fidelity Original: Memory regions; access kinds; cache hierarchy awareness; processor-specific optimization

E.6 References

• OCaml Memory Representation: https://ocaml.org/docs/memory-representation
• Real World OCaml, Runtime Memory Layout: https://dev.realworldocaml.org/runtime-memory-layout.html
• Rust Ownership: https://doc.rust-lang.org/book/ch04-00-understanding-ownership.html
• Fidelity Cache-Aware Compilation: See SpeakEZ blog posts on cache-conscious memory management