Clef Type Universe Specification

Status: Draft Phase: A (Type Universe) - Part of Clef principled type system redesign Last Updated: 2024-12-30

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
4. Leverage Existing F# Machinery: Reuse FSharp.Core where possible
5. Spec Before Scaffold: Document before implementing

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.

Design Decision: 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.

Design Decisions:

1. No width-named integer type. int8, int16, int32, int64, their unsigned forms, byte, sbyte, uint, nativeint and unativeint are not Clef types (D10, Dimensional_Range_Design.md). “There is only int that happens to be 8 wide.” 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 is CCS8012 at design time, a warning promoted under --warnaserror. There is no Checked module and no debug-build trap, because there is no undefined case for either to catch.

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 (D10).

Design Decisions:

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 *)

Design Decision (RESOLVED): 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:

Design Decision: 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

OCaml Comparison:

Mutable Fields:

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

Cache-Aware Record Design:

For high-performance scenarios, consider field ordering for cache efficiency:

// 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:

When mutable fields are accessed from multiple threads, place them on separate cache lines:

[<Struct>]
type ThreadCounters = {
    [<CacheLineAligned>]  // Attribute hint to compiler
    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.

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 (never inline-by-default, which was tried and reverted because it multiplied bodies at every call site and exploded the PSG) 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. Inline-by-default (every function transparent, the model absorbed from an earlier library) was tried and reverted: it multiplied bodies at every call site and exploded the PSG.

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
 

Escape Prevention: Mutable bindings cannot be captured by closures (use ref instead). This restriction enables guaranteed stack allocation.

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:

The entire point of Fidelity is that the F# compiler controls memory layout, not MLIR, not LLVM. Memory region types:

1. Carry semantic meaning through the entire compilation pipeline
2. Guide Alex’s code generation - Peripheral → volatile LLVM instructions
3. Determine allocation strategy - Stack vs Arena vs explicit
4. Enable compile-time safety - region mismatches are type errors
5. Erase at final lowering - only after ALL decisions are made by Fidelity

This is fundamentally different from letting MLIR/LLVM “figure out” memory layout. Fidelity dictates; LLVM implements.

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

Status (January 2026): Arena is implemented as an CCS intrinsic type.

Type Definition:

Arena<[<Measure>] 'lifetime>

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).

Lifetime Inference Principle: Arena demonstrates the three-level approach:

• Level 3 (Explicit): Current - full manual control
• Level 2 (Hints): Future - arena { } computation expressions
• Level 1 (Inferred): Future - compiler escape analysis

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

DEFERRED TO PHASE B: This section will be completed after QuantumCredential PoC.

9.1 Pure vs Effectful Classification

TBD - Continuation-based RAII model

9.2 Resource Coeffects

TBD - ResourceCoeffect type integration

Part 10: Interactive Development (clefx)

Spec Reference: See interactive-development.md for full specification.

The type universe must account for interactive development scenarios where types are defined and evaluated incrementally.

10.1 Interactive Session Types

In clefx (Clef Interactive), types are resolved in an evolving environment:

> type Point = { x: int; y: int };;
type Point

> let origin = { x = 0; y = 0 };;
val origin : Point

Type Resolution in Interactive Mode:

• Types defined in the session are immediately available
• Types from #require directives are loaded into the type environment
• CCS resolves types against both session-local and loaded definitions

10.2 Arena Semantics in Interactive Mode

Interactive sessions use arena-based allocation:

Type Implications:

> let data = [1..1000000];;
val data : int list  // Allocated in session arena

> #arena reset;;
// data is no longer valid - type checker knows this
 

10.3 Interpretation vs Compilation Type Semantics

All modes use identical type semantics. The difference is only in execution:

> #mode compile;;
> let rec fib n = if n < 2 then n else fib (n-1) + fib (n-2);;
val fib : int -> int  // Same type in all modes
 

10.4 Script File Type Semantics

Script files (.clefx) follow the same type semantics as compiled modules:

// script.clefx
let greeting : string = "Hello"  // string as a UTF-8 memref<?xi8> view
let maybe : int option = Some 42  // voption<int>, non-null
 

10.5 Cross-Compilation Type Considerations

When targeting a different platform:

> #target linux-arm64;;
Target: linux-arm64 (cross-compiling from linux-x64)

> sizeof<nativeint>;;
val it : int = 8  // Reflects target, not host
 

Platform-Specific Types:

• nativeint/unativeint size reflects target platform
• index width and the Ptr<'T, 'Region, 'Access> handle width reflect the target architecture
• Type layouts follow target ABI

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 (KEEP)

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 (SET ASIDE)

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 (ADAPT)

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 doctrine extends beyond both OCaml and Rust:

Cache Hierarchy Awareness

Memory Hierarchy Management

// Fidelity-specific: Cache-conscious arena configuration
let configureArena (profile: ActorProfile) =
    match profile.WorkingSetSize with
    | size when size <= 32<KB> -> L1Resident    // Fits in L1
    | size when size <= 256<KB> -> L2Optimized  // Fits in L2
    | size when size <= 8<MB> -> L3Optimized    // Fits in L3
    | _ -> StreamingMode                         // Bypass cache
 

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

This synthesis provides provenance (we didn’t start from scratch) while forging a path suited to native compilation across the full hardware spectrum - from embedded microcontrollers to GPU clusters.

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

Changelog

• 2024-12-30: Session 1 (Unit, Bool, Integers) - Comprehensive primitive type specification with OCaml provenance, cache alignment considerations, resolved char design decision (UTF-32 codepoints)
• 2024-12-30: Added Appendix E (OCaml Provenance and Fidelity Extensions) documenting design heritage and extensions
• 2024-12-30: Initial skeleton created from plan