Native Type Mappings

This chapter defines how F# types map to native representations in Clef compilation.

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: Users write standard F# type names. CCS provides native semantics transparently.

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

Floating Point Types

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

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.

Why IL Infrastructure Is Removed from CCS

Clef Compiler Service (CCS) targets native compilation via MLIR (Multi-Level Intermediate Representation), not CLR bytecode. While CCS originated from the F# Compiler Services (FCS) codebase, its type universe, compilation passes, and concurrency primitives are independently defined. Consequently, all IL-based infrastructure has been removed from the typed tree operations.

The Architecture Boundary

┌─────────────────────────────────────────────────┐
│  CCS (Clef Compiler Services)             │
│  - Type checking, resolution, inference         │
│  - Produces typed tree with native types        │
│  - NO code generation, NO IL                    │
└─────────────────────────────────────────────────┘
                      │
                      ▼ Typed Tree (native types)
┌─────────────────────────────────────────────────┐
│  Alex (Code Generation)                         │
│  - PSG traversal via Zipper                     │
│  - Platform bindings for syscalls               │
│  - MLIR emission                                │
└─────────────────────────────────────────────────┘
                      │
                      ▼ MLIR
┌─────────────────────────────────────────────────┐
│  MLIR Optimization Passes                       │
│  - Loop optimization (SCF dialect)              │
│  - Arithmetic optimization (arith dialect)      │
│  - Memory optimization                          │
└─────────────────────────────────────────────────┘
                      │
                      ▼ Portable dialects
┌─────────────────────────────────────────────────┐
│  Target Pathway (target-committing)             │
│  - LLVM pathway: LLVM IR → CPU/MCU binary       │
│  - CIRCT pathway: HW dialects → bitstream       │
│  - JSIR pathway: → JavaScript module            │
└─────────────────────────────────────────────────┘

The MLIR optimization passes and everything above them stay portable; a target is committed only at the target pathway. LLVM is one pathway among several.

Why IL Operations Are Not Stubbed

The original FCS contains IL-based operations for loop optimization, null handling, and arithmetic. These were initially stubbed during the CCS fork, but stubs produce semantically wrong results:

Principle: “Delete, don’t stub” - Broken stubs hide defects and produce silent wrong behavior. Complete removal makes missing functionality explicit.

What Functionality Moves Downstream

Null Is Not Representable

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

• mkNull, mkNullTest, mkNonNullTest, mkNonNullCond - all removed
• 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.

Removed IL Infrastructure

The following were removed from TypedTreeOps.fs:

IL Instruction Stubs:

• ILDataType type
• AI_ldnull, AI_cgt_un, AI_clt_un, AI_add, AI_sub, AI_div_un, etc.
• ILInstr module
• mkAsmExpr function

Loop Optimization (vestigial - no callers):

• DetectAndOptimizeForEachExpression
• mkOptimizedRangeLoop, mkRangeCount
• mkFastForLoop
• Pattern matchers: Int32Expr, RangeInt32Step, CompiledForEachExpr, etc.
• IntegralConst module, IntegralRange, EmptyRange, ConstCount patterns

Null Operations:

• mkNull, mkNullTest, mkNonNullTest, mkNonNullCond

Broken Comparison Stubs:

• mkILAsmCeq, mkILAsmClt, mkDecr, mkGetStringLength

The Key Insight

IL-based loop optimization at the typed tree level was premature optimization at the wrong layer. Native loop optimization belongs in MLIR passes where the target architecture is known and appropriate loop transformations (vectorization, unrolling, tiling) can be applied.