NTU Type Nomenclature Specification

Status: Draft Normative: Yes Last Updated: 2026-02-11

1. Overview

This chapter specifies the NTU (Native Type Universe) nomenclature used internally by CCS (Clef Compiler Service) for platform-generic types. NTU types resolve via quotation-based platform bindings, following the F* pattern where type WIDTH is an erased assumption.

Width is a first-class dimension in NTU. Numeric types are parameterized by NTUWidth, which can be Fixed (known at all times) or Resolved (platform-dependent, resolved by Alex via PlatformContext). This replaces 16 discrete integer/float variants with 3 parameterized kinds.

1.1 Core Principle

Platform awareness flows FROM THE TOP via quotation-based binding libraries, not from CCS type inference.

CCS validates type identity (e.g. NTUint (Resolved Register) vs NTUint (Fixed 64)). Alex witnesses platform quotations to determine type width (32-bit vs 64-bit).

2. NTU Type Categories

2.1 Width Dimensions

Width is parameterized, not baked into variant names. The WidthDimension type names are NTU-native; they are NOT named after C types.

/// Platform-resolved width dimensions
type WidthDimension =
    | Pointer    // Address width (64-bit on x86_64, 32-bit on ARM32)
    | Register   // Machine register / natural word width

/// How the width of a numeric type is determined
type NTUWidth =
    | Fixed of bits: int              // Known at all times: 8, 16, 32, 64
    | Resolved of WidthDimension      // Platform-dependent, resolved by Alex
 

2.2 Parameterized Numeric Types

2.3 Pointer and Semantic Types (Implicit Pointer Width)

3. Type Identity and Type Width

3.1 Type Identity (CCS Responsibility)

CCS enforces type identity constraints. With parameterized width, type identity includes the width dimension:

NTUint(Resolved Register) ≠ NTUint(Fixed 32)    // Different types
NTUint(Resolved Register) ≠ NTUint(Fixed 64)    // Different types
NTUint(Resolved Register) = NTUint(Resolved Register)  // Same type

// Valid
let add (x: int) (y: int) : int = x + y   // Both NTUint(Resolved Register)

// Type Error
let invalid (x: int) (y: int64) = x + y   // NTUint(Resolved Register) ≠ NTUint(Fixed 64)
 

3.2 Type Width (Alex Responsibility)

Alex resolves type width via platform quotations and the PlatformContext.Dimensions map:

Example resolutions:

3.3 Erased Width Assumptions

Following F*’s pattern, width is compile-time metadata only:

type NTULayout = {
    Kind: NTUKind
    /// Erased - not present at runtime
    AssumedSize: int option
    AssumedAlignment: int option
}

Width assumptions guide type checking but are erased before code generation. Alex makes final width decisions based on platform quotations.

4. Mapping to F# Source Types

4.1 Layered Type Abstraction

The architecture uses a three-tier exposure model:

NTUptr is the internal kind for a pointer-shaped value. The only user-denotable source that maps to it is the opaque handle Ptr<'T, Region, Access> returned across a C binding, together with the register handle Mmio for a fixed-address peripheral. nativeptr<'T> is not a Clef source type and never appears in user code; the compiler reaches NTUptr through its own internal plumbing, not through a written nativeptr<'T> annotation.

4.2 Developer Experience

Level 1 (Default): Developers use standard F# type names.

let x: int = 42  // CCS sees NTUint
let arr: array<int> = [| 1; 2; 3 |]

Level 2/3 (Explicit): Developers use semantic aliases for clarity. A byte buffer is a bounded stack array, not a raw pointer.

let write (fd: platformint) (buf: array<byte>) (count: platformsize) : platformint =
    Platform.Bindings.write fd buf count

5. NTUKind Implementation

5.1 Width and Kind Definitions

/// Platform-resolved width dimensions: NTU-native vocabulary.
[<RequireQualifiedAccess>]
type WidthDimension =
    | Pointer       // Address width (pointer-sized)
    | Register      // Machine register / natural word width

/// How the width of a numeric type is determined.
[<RequireQualifiedAccess>]
type NTUWidth =
    | Fixed of bits: int              // Known at all times: 8, 16, 32, 64
    | Resolved of WidthDimension      // Platform-dependent, resolved by Alex

/// NTU (Native Type Universe) type kinds.
/// Numeric types parameterized by width. 3 kinds replace 16 discrete variants.
[<RequireQualifiedAccess>]
type NTUKind =
    // Parameterized numeric types (width as dimension)
    | NTUint of NTUWidth      // Signed integer of any width
    | NTUuint of NTUWidth     // Unsigned integer of any width
    | NTUfloat of NTUWidth    // IEEE float of any width
    // Pointer types (width = Pointer, implicit)
    | NTUptr                  // Native pointer
    | NTUfnptr                // Function pointer
    | NTUsize                 // Size type (unsigned, pointer-width)
    | NTUdiff                 // Pointer difference (signed, pointer-width)
    // Special types
    | NTUstring | NTUbool | NTUchar | NTUunit | NTUdecimal
    | NTUlazy | NTUseq
    // Collection types
    | NTUarray | NTUlist | NTUmap | NTUset
    // Compound value types
    | NTUuuid | NTUdatetime | NTUtimespan

5.2 PlatformContext (Width Resolution)

type PlatformContext = {
    PlatformId: string
    /// Width dimension resolutions (bits)
    Dimensions: Map<WidthDimension, int>  // Pointer → 64, Register → 64, etc.
    PointerAlign: int
    PlatformLibraryPath: string option
    Predicates: Map<PlatformPredicate, bool>
    FreestandingStartup: FreestandingStartup option
}

module PlatformContext =
    /// Resolve an NTUWidth to concrete bits
    let resolveWidth (ctx: PlatformContext) (width: NTUWidth) : int =
        match width with
        | NTUWidth.Fixed bits -> bits
        | NTUWidth.Resolved dim -> ctx.Dimensions.[dim]

    let defaultLinux_x86_64 = {
        PlatformId = "Linux_x86_64"
        Dimensions = Map.ofList [ (WidthDimension.Pointer, 64); (WidthDimension.Register, 64) ]
        PointerAlign = 8
        PlatformLibraryPath = None
        Predicates = Map.ofList [ ... ]
        FreestandingStartup = None
    }

6. Unification Rules

6.1 NTU Types Unify Only with Themselves

// Valid unification: same kind and same width
unify(NTUint(Resolved Register), NTUint(Resolved Register)) = Success

// Invalid unification: same kind but different width
unify(NTUint(Resolved Register), NTUint(Fixed 64)) = Error(TypeMismatch)
unify(NTUint(Resolved Register), NTUint(Fixed 32)) = Error(TypeMismatch)

// Invalid unification: different kinds
unify(NTUint(Fixed 32), NTUuint(Fixed 32)) = Error(TypeMismatch)

// Pointer types: element types must unify
unify(NTUptr<int>, NTUptr<int>) = Success
unify(NTUptr<int>, NTUptr<float>) = Error(TypeMismatch)

6.2 No Implicit Width Coercion

NTU types never implicitly widen or narrow:

// These are TYPE ERRORS, not implicit conversions
let x: int64 = 42       // Error: int ≠ int64
let y: int = 42L        // Error: int64 ≠ int

// Explicit conversions required
let x: int64 = int64 42
let y: int = int 42L

7. Platform Quotation Resolution

7.1 Resolution Flow

F# Source (int)
    ↓
CCS: Maps to NTUint(Resolved Register)
    ↓
SemanticGraph: Carries NTUint(Resolved Register) annotation
    ↓
Alex: Resolves Register dimension via PlatformContext.Dimensions
    ↓
MLIR: i64 (on x86_64) or i32 (on ARM32)

7.2 Platform Quotation Structure

Width resolution is now dimension-based. Platform quotations provide the Dimensions map that PlatformContext.resolveWidth uses:

// From Fidelity.Platform library: dimension resolution map
type NTUResolutions = Map<WidthDimension, int>

let linux_x86_64: Expr<NTUResolutions> = <@
    Map.ofList [ (Pointer, 64); (Register, 64) ]
@>

let linux_arm32: Expr<NTUResolutions> = <@
    Map.ofList [ (Pointer, 32); (Register, 32) ]
@>

8. MLIR Mapping

8.1 NTU to MLIR Type Mapping

The middle end (Alex) emits only portable dialect types (func, cf, scf, arith, memref, index, builtin) and commits to no target. Pointer-shaped NTU kinds map to the platform-sized index type, not to any target dialect. NTUptr in particular maps to index at the NTU level (Composer TypeMapping.fs maps NTUptr/NTUfnptr -> TIndex, which serializes as index). Target realization is a backend-leg concern: the LLVM leg lowers index to !llvm.ptr where a raw address is needed, the CIRCT/FPGA leg realizes it as a target-appropriate carrier, and constructs with no portable form (a function address taken as data, a raw environment pointer) are carried across the tier boundary as builtin.unrealized_conversion_cast and realized per leg.

The index type is platform-sized: it resolves to a 64-bit value on x86_64 and a 32-bit value on ARM32 (and on thumbv8m/M33), so a single portable mapping carries the correct pointer width per target without the NTU level naming any concrete byte count. On a backend leg that needs a raw address rather than an index (the LLVM CPU/MCU leg), index is realized as !llvm.ptr during leg lowering. That realization is lossy and belongs to the leg, so it never appears in what the NTU or the middle end emits.

9. Conformance Requirements

9.1 CCS Requirements

1. MUST distinguish NTU type identity (NTUint (Resolved Register) vs NTUint (Fixed 64))
2. MUST NOT assume platform-dependent type widths
3. MUST propagate NTU annotations through SemanticGraph
4. MUST reject operations between incompatible NTU types

9.2 Alex Requirements

1. MUST resolve NTU types using platform quotations
2. MUST generate platform-appropriate MLIR types
3. MUST use consistent resolution across all occurrences

10. Related Specifications

• platform-predicates.md - Platform predicate semantics
• native-type-mappings.md - F# to native type mappings
• native-type-universe.md - Complete type universe specification