Native Type Mappings

This chapter defines how Clef source types map to native representations.

Overview

Clef uses familiar F# syntax with native semantics. The compiler (CCS) resolves types to native representations at compile time, not to BCL types.

Principle: Source types follow the NTU kind and dimension model. Familiar syntax does not import managed types or width-named numeric types.

The Universal Base Type obj Is Not Available

In managed F#, all types inherit from System.Object (aliased as obj). This enables:

• Boxing value types to heap-allocated objects
• Runtime type information and reflection
• Heterogeneous collections (obj list)
• Generic %A formatting via runtime inspection

Clef eliminates obj entirely. There is no universal base type. The compiler SHALL reject any code that references obj or System.Object.

The foreign pair of JavaScript Boundary Semantics (JsValue, JsRef<'T>) does not reintroduce a universal type, and this section’s prohibition stands unchanged wherever that chapter is in force. The universal type’s hazard is subsumption, the unmarked conversion that lets any value become the universal type silently; the pair participates in no subtyping relationship, its injection is explicit at declared boundary functions, and its only elimination is narrowing.

Rationale

Why obj Cannot Exist in Native Compilation

1. No runtime type information: Native binaries do not carry type metadata. There is no mechanism to inspect a value’s type at runtime.

2. No garbage collector: The obj type implies heap allocation with GC-managed lifetime. Clef uses deterministic, scope-based memory management.

3. Full static resolution: All types are resolved at compile time. Generic type parameters are monomorphized (specialized at each call site). Type erasure to obj is unnecessary and would lose type safety.

4. SRTP replaces runtime dispatch: Where managed F# uses obj and runtime dispatch (like printf "%A"), Clef uses statically resolved type parameters with compile-time method resolution.

Migrating Code That Uses obj

Code using obj must be refactored to use type-safe alternatives:

Heterogeneous collections:

// DOES NOT COMPILE in Clef
let values : obj list = [box 1; box "hello"; box 3.14]

// Use discriminated union instead
type Value = 
    | Int of int 
    | Str of string 
    | Float of float
let values : Value list = [Int 1; Str "hello"; Float 3.14]

Polymorphic formatting:

// DOES NOT COMPILE in Clef  
let show (x: obj) = sprintf "%A" x

// Use SRTP with operator overloading
type Showable = Showable
    with static member inline ($) (Showable, x: int) = intToString x
         static member inline ($) (Showable, x: string) = x
         // ... additional overloads

let inline show x = Showable $ x

Type-based dispatch:

// DOES NOT COMPILE in Clef
let process (x: obj) =
    match x with
    | :? int as i -> handleInt i
    | :? string as s -> handleString s
    | _ -> handleOther ()

// Use discriminated union with exhaustive matching
type Input = IntInput of int | StringInput of string
let process (x: Input) =
    match x with
    | IntInput i -> handleInt i
    | StringInput s -> handleString s

Compile-Time Metaprogramming

The absence of obj and System.Reflection does not leave Clef without metaprogramming capabilities. Three F# features provide typed, compile-time metaprogramming that surpasses what reflection-based approaches can offer:

Why This Matters

Other native-compiled ML-family languages lack typed metaprogramming:

F# quotations carry full type information through transformations. OCaml’s PPX system and Rust’s procedural macros operate on strings or token streams - they lack the type safety that quotations provide.

Quotations as Semantic Carriers

Quotations encode constraints and metadata as compile-time data that the compiler can inspect:

// Peripheral descriptor carried as typed quotation
let gpioDescriptor: Expr<PeripheralDescriptor> = <@
    { Name = "GPIO"
      BaseAddress = 0x48000000un
      MemoryRegion = Peripheral }
@>

The compiler extracts semantic information from quotations during PSG construction. No runtime reflection is needed - the information is available at compile time and can guide code generation (e.g., emitting volatile loads for peripheral access).

Active Patterns for Structural Recognition

Active patterns enable compositional matching without type discrimination hierarchies:

// Recognize SRTP dispatch in PSG nodes
let (|SRTPDispatch|_|) (node: PSGNode) =
    match node.TypeCorrelation with
    | Some { SRTPResolution = Some srtp } -> Some srtp
    | _ -> None

// Composable usage
match currentNode with
| SRTPDispatch srtp -> emitResolvedCall srtp
| PeripheralAccess info -> emitVolatileAccess info
| _ -> emitDefault node

Active patterns compose with & and |, can be tested in isolation, and encapsulate recognition logic - capabilities that runtime type inspection cannot match.

Computation Expressions as Continuation Capture

Every let! in a computation expression captures a continuation:

maybe {
    let! x = someOption    // Bind(someOption, fun x -> ...)
    let! y = otherOption   // Bind(otherOption, fun y -> ...)
    return x + y
}

This desugaring to nested lambdas provides continuation semantics as notation. The compilation strategy depends on the computation pattern:

Normative Requirements

NORMATIVE: System.Reflection and all reflection-based APIs SHALL NOT be available in Clef. The compiler SHALL reject any code that references reflection types or methods.

NORMATIVE: Quotations, active patterns, and computation expressions SHALL be fully supported. These features operate at compile time and impose no runtime overhead.

NORMATIVE: Quotation-based metaprogramming SHALL NOT require runtime evaluation. All quotation inspection and transformation occurs during compilation.

Primitive Types

Numeric Types

Signedness and width are storage facts. byte, uint8, uint, int64, nativeint and the other width-named spellings are not Clef source types. A byte-unit buffer is array<int>; its encoding or boundary contract supplies the cell range and representation evidence. An ordinary integer is not an address; addresses use the semantic types in NTU Types §2.3.

Floating Point Types

float32, single, double and other representation spellings do not select source types. The numeric selection rules govern any unobservable-range case.

Character and String Types

Composite Types

Tuples

Tuples are laid out as contiguous structs with natural alignment:

let pair : int * float = (42, 3.14)

Layout:

┌─────────┬─────────┬─────────┐
│ int (8) │ pad (0) │ float(8)│
└─────────┴─────────┴─────────┘
Total: 16 bytes

Records

Records are named product types with field-order layout:

type Point = { X: float; Y: float }

Layout: Same as tuple of fields in declaration order.

Discriminated Unions

A discriminated-union value is a memref<Exi8> view of its {tag, payload} storage block, with E settled at saturation (Discriminated Union Representation §3). A payload that is itself arena-resident (a recursive case, a collection) is linked by a bounded index, never by an address:

type Option<'T> = None | Some of 'T

Layout:

┌──────────┬────────────────────────┐
│ Tag (i8) │ Payload (size of 'T)   │
└──────────┴────────────────────────┘

Single-Case Unions (Newtypes)

Single-case unions have no tag overhead:

type UserId = UserId of int

Layout: Same as wrapped type (int).

Struct Alignment

Default Alignment

Structs use natural alignment based on their largest field:

Word alignment follows the Pointer width dimension of NTU Types §2.3; it is the platform word, not a fixed 8 bytes.

Explicit Alignment

The [<Align(n)>] attribute requests specific alignment:

[<Align(64)>]
[<Struct>]
type CacheAligned = { Value: int64 }

NORMATIVE: The compiler SHALL respect alignment requests that are:

• Powers of two
• Greater than or equal to natural alignment
• Less than or equal to platform page size (typically 4096)

NORMATIVE: Alignment requests that cannot be satisfied SHALL produce a compile-time error.

Alignment and SIMD

For SIMD operations, alignment affects performance significantly:

Misaligned vector loads may incur penalties or faults depending on the instruction.

Stack and Arena Allocation

NORMATIVE: Stack-allocated aligned types SHALL be placed at appropriately aligned addresses.

NORMATIVE: Arena allocators SHALL provide an alignment-aware allocation function:

Arena.allocAligned<'T> : Arena -> alignment:int -> count:int -> Ptr<'T, Arena, ReadWrite>

Intrinsic Operations

Certain operations have direct hardware support that F# loops cannot match. CCS intrinsics provide guaranteed-efficient implementations.

Bit Manipulation Intrinsics

The middle end emits each intrinsic as a target-agnostic operation. The LLVM-pathway realization is the LLVM intrinsic shown below; other target pathways (CIRCT for FPGA, JSIR for JS) realize the same operation with their own target primitives.

NORMATIVE: These functions SHALL lower to the target’s native bit-manipulation primitive, not loop-based implementations. On the LLVM pathway that primitive is the corresponding LLVM intrinsic shown above.

Arithmetic Intrinsics

NORMATIVE: Multi-word arithmetic operations SHALL use carry-propagating instructions where available.

Usage

let extractRegime (bits: uint32) =
    let shifted = bits <<< 1
    let leadingZeros = clz shifted  // Guaranteed 1-2 cycles, not a loop
    // ... regime extraction logic
 

Fallback Behavior

On targets without hardware support for specific intrinsics:

NORMATIVE: The compiler SHALL emit efficient software fallbacks that match the semantic behavior.

NORMATIVE: The compiler MAY emit warnings when intrinsics fall back to software implementation on performance-critical targets.

Reference Types

Arrays

An array is a memref<?xT> view: the element buffer is the value, and its length is the memref’s dimension. There is no header struct and no separate length word.

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

Layout (the buffer; memref<?xT> at saturation):

array<'T>   memref<?xT>
┌─────┬─────┬─────┐
│ [0] │ [1] │ [2] │   contiguous, naturally aligned; extent = length
└─────┴─────┴─────┘

The view’s descriptor (base, offset, extent, stride) is a lowering artifact of the target pathway, not a Clef value; no Clef operation observes it.

Strings

A string is a memref<?xi8> view of its UTF-8 byte buffer: the buffer is the value, and its byte length is the memref’s dimension. There is no separate length header.

Layout (the buffer; memref<?xi8> at saturation):

string   memref<?xi8>
┌────┬────┬────┬─────┐
│ b0 │ b1 │ b2 │ ... │   UTF-8 bytes; extent = byte length
└────┴────┴────┴─────┘

The view’s descriptor is a lowering artifact of the target pathway, not a Clef value; no Clef operation observes it. On the JSIR pathway string is a host string and this layout does not bind (Native Type Universe §4.1).

Integer byte-unit conversions

The source signatures use dimensionless integers:

String.fromBytes : array<int> -> string
String.toBytes : string -> array<int>

These array elements are encoded byte units, not Unicode scalar values. The string laws in Native Type Universe §4.1 remain authoritative: strings contain valid UTF-8, and character operations observe codepoints.

String.fromBytes requires evidence that its input elements fit the encoding’s byte units and that the resulting sequence is valid UTF-8. An integer array’s source type alone establishes neither property. Baker retains the particular allocation, aliases, slices, contributing writes and dependent reads in the PSG; representation selection applies to those buffer occurrences, never to every array with the same logical element type. The selected platform must offer the required unsigned byte representation.

Both conversions establish independent snapshots. Later writes through the input of fromBytes SHALL NOT change the constructed string. Mutating the array returned by toBytes SHALL NOT change its source string. toBytes preserves the UTF-8 byte sequence, order and length. Eliminating a copy requires ownership and preservation evidence that establishes these observable laws; a matching physical layout alone is insufficient.

Baker expresses the required storage, copy and final view relationships in the graph before Alex witnesses them. Alex consumes the settled storage and width adaptations. Its internal byte/string view requires matching physical carriers and cannot repair a wider integer buffer by relabeling its return type.

Byte-range evidence alone does not prove UTF-8 validity: a lone 255 or continuation unit 169 is not admitted as text.

The internal byte view carries the encoding’s eight-bit storage evidence. The public array’s representation follows its complete write range, including subsequent ordinary integer writes above 255; it is not restricted to the view’s carrier. The graph retains the selected representation declaration and copy dependencies, and normal range analysis settles the resulting reads and writes.

Parameterized Types

Option

Option types use voption (value option) semantics:

let maybe : int option = Some 42

Layout: Stack-allocated tagged union (see Discriminated Unions).

Result

Result types are stack-allocated tagged unions:

let result : Result<int, string> = Ok 42

Layout: Tag + max(sizeof Ok payload, sizeof Error payload).

List

A list value is the index of its first node in the arena that holds the list. A node is a flat aggregate with a settled layout, a memref<Exi8> view at saturation (List Operations Representation §5):

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

Layout (per node):

list<'T> node   memref<Exi8>
┌──────────────────────┬─────────────────┬──────────────────────────┐
│ tag: i8 (Empty|Cons) │ head: 'T        │ tail: index (arena link) │
└──────────────────────┴─────────────────┴──────────────────────────┘

Every tail is a valid node: operations read tail unconditionally and recursion terminates at the sentinel. Layout obligations (VC-LINK, VC-GUARD, sentinel residence and immutability) are quantifier-free at saturation over the graph’s literals; the list algebra is a schema lemma proven once per recipe shape, never a per-program fixpoint.

Function Types

Direct Functions

Known call sites compile to direct calls:

let add x y = x + y
add 1 2  // Direct call, no closure
 

Closures

Functions capturing environment use closure representation:

let makeAdder n = fun x -> x + n

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

fn:  func.constant @makeAdder_lambda : (memref<Exi8>, int) -> int
env: ┌─────────────────────┐
     │ n: captured value   │   memref<Exi8>, E literal at saturation
     └─────────────────────┘

MLIR Type Mappings

The middle end emits these portable forms; a target pathway lowers them (Backend Lowering Architecture). No row is a pointer: a buffer is a memref view, and a link between arena-resident nodes is a bounded index carrying VC-LINK.

Native Compilation Boundary

Clef Compiler Service (CCS) performs type checking, resolution, and inference over native types. CCS does not emit CLR bytecode or IL operations. Alex emits portable MLIR from the Program Semantic Graph, and target pathways realize those operations as specified in Backend Lowering Architecture.

The Architecture Boundary

CCS / Baker
  Source semantics, elaboration, saturation and numeric selection
  Declaration/ABI settlement and proof premises
  Nanopass ingredients/recipes, joint constraints, scope and rewrite record
    ↓ Settled PSG publication
Alex
  Passive Huet Element/Pattern/Witness composition
  Typed operands and admitted portable operations
    ↓ Witnessed form with required facts and proof correspondence
Composer backend
  Target-specific lowering and admitted preserving transformations
  LLVM → CPU/MCU binary; CIRCT → bitstream; JSIR → JavaScript module

Source analysis and semantic repair remain in CCS/Baker. Composer’s backend realizes the settled contracts and preserves or rechecks affected properties through its admitted transformations. Custom MLIR plugins and their compatibility dependencies are retired.

Native Operation Lowering

An admitted backend transformation SHALL preserve the source semantics and required proof correspondence. It SHALL NOT infer missing source premises.

Null Is Not Representable

Clef has no null values. The null keyword and null checking operations are not available.

• Option types (voption) replace nullable references
• Pattern matching replaces null checks

This is consistent with Clef’s safety guarantees: no null dereference is possible because null cannot be expressed.

On the JSIR pathway, null and undefined appear in the emitted JavaScript artifact only as boundary representations selected by generated code and as the proven Option erasure of Option Operations Representation §2.1, per the confinement rule of JavaScript Boundary Semantics §8. No Clef-typed value is null or undefined on any pathway.