Option Operations Representation

Status: Normative Last Updated: 2026-01-22 Depends On: Native Type Universe § 5.1 Option

1. Overview

Clef implements option operations (Option.map, Option.bind, Option.defaultValue, etc.) as Baker-decomposed pattern matches. Options are stack-allocated tagged unions (voption semantics), and operations compile to simple conditional branches.

Key Insight: Option operations are structurally trivial: each is a single match expression with two branches (Some/None). Baker decomposes them to isSome checks and value extraction.

2. Memory Layout (Reference)

Options follow the layout specified in Native Type Universe § 5.1:

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

Note: Option has 2 cases, so the minimum tag is i8 (1 byte). Platform policy MAY use larger tags for alignment efficiency on word-aligned architectures. The tag is NEVER i1 (bit) because bits are not addressable and DU tags are case indices, not booleans.

2.1 JSIR-Pathway Realization

This section binds implementations claiming the JavaScript Substrate profile (Conformance §7).

The layout above is a commitment of layout-realizing pathways. On the JSIR pathway, under the carrier-realization rule of Backend Lowering Architecture §4.5, option<'T> is realized in one of two forms, selected per instantiation at compile time:

1. Erased: Some x is realized as the realization of x, and None as undefined. The erased form SHALL be selected only where the implementation proves that undefined cannot denote a Some payload: the payload type’s realization SHALL NOT include undefined among its values, and a nested option SHALL be reified at every nesting level the proof cannot discharge.
2. Reified: a host object carrying the §2 tag semantics (None = 0, Some = 1) and the payload. The reified form is always permitted.

The selection is a compile-time property of each instantiation, settled before emission and read at emission; it SHALL NOT vary at runtime. The observable semantics of §3 and §4 (operation results, lazy defaults, vacuous truth) bind unchanged under either form.

Erasure is an interior representation choice, not a boundary conversion. Absence crossing the JavaScript boundary is converted under JavaScript Boundary Semantics §5, and an erased None that reaches an outbound boundary position is emitted as that position’s selected representation, which need not be undefined.

3. Operation Classification

3.1 Primitive Operations (Alex Witnesses Directly)

3.2 Higher-Order Functions (Baker Decomposes)

4. HOF Decomposition Specifications

4.1 Option.map

Option.map : ('a -> 'b) -> 'a option -> 'b option

Decomposition:

let map f opt =
    match opt with
    | Some x -> Some (f x)
    | None -> None

Baker Recipe:

recipe {
    let! isSome = isSome optId
    let! someCase = recipe {
        let! value = getValue optId elemType
        let! mapped = app1 mapperNodeId value outputType
        return! some mapped outputType
    }
    let! noneCase = none outputType
    return! ifThenElse isSome someCase noneCase optionOutputType
}

4.2 Option.bind

Option.bind : ('a -> 'b option) -> 'a option -> 'b option

Decomposition:

let bind f opt =
    match opt with
    | Some x -> f x
    | None -> None

Baker Recipe: Similar to map, but f x returns an option directly (no wrapping).

4.3 Option.defaultValue

Option.defaultValue : 'a -> 'a option -> 'a

Decomposition:

let defaultValue def opt =
    match opt with
    | Some x -> x
    | None -> def

Baker Recipe:

recipe {
    let! isSome = isSome optId
    let! someValue = getValue optId elemType
    return! ifThenElse isSome someValue defaultValueId elemType
}

4.4 Option.defaultWith

Option.defaultWith : (unit -> 'a) -> 'a option -> 'a

Decomposition:

let defaultWith defThunk opt =
    match opt with
    | Some x -> x
    | None -> defThunk ()

Note: The thunk is only evaluated if opt is None (lazy evaluation).

4.5 Option.orElse

Option.orElse : 'a option -> 'a option -> 'a option

Decomposition:

let orElse ifNone opt =
    match opt with
    | Some _ -> opt
    | None -> ifNone

4.6 Option.orElseWith

Option.orElseWith : (unit -> 'a option) -> 'a option -> 'a option

Decomposition:

let orElseWith ifNoneThunk opt =
    match opt with
    | Some _ -> opt
    | None -> ifNoneThunk ()

4.7 Option.filter

Option.filter : ('a -> bool) -> 'a option -> 'a option

Decomposition:

let filter predicate opt =
    match opt with
    | Some x -> if predicate x then Some x else None
    | None -> None

Baker Recipe:

recipe {
    let! isSome = isSome optId
    let! filteredSome = recipe {
        let! value = getValue optId elemType
        let! passes = app1 predicateId value boolType
        let! keepSome = some value elemType
        let! discardNone = none elemType
        return! ifThenElse passes keepSome discardNone optionType
    }
    let! noneCase = none elemType
    return! ifThenElse isSome filteredSome noneCase optionType
}

4.8 Option.exists

Option.exists : ('a -> bool) -> 'a option -> bool

Decomposition:

let exists predicate opt =
    match opt with
    | Some x -> predicate x
    | None -> false

4.9 Option.forall

Option.forall : ('a -> bool) -> 'a option -> bool

Decomposition:

let forall predicate opt =
    match opt with
    | Some x -> predicate x
    | None -> true  // Vacuously true
 

4.10 Option.iter

Option.iter : ('a -> unit) -> 'a option -> unit

Decomposition:

let iter action opt =
    match opt with
    | Some x -> action x
    | None -> ()

4.11 Option.toList

Option.toList : 'a option -> 'a list

Decomposition:

let toList opt =
    match opt with
    | Some x -> [x]
    | None -> []

4.12 Option.toArray

Option.toArray : 'a option -> 'a array

Decomposition:

let toArray opt =
    match opt with
    | Some x -> [| x |]
    | None -> [| |]

4.13 Option.flatten

Option.flatten : 'a option option -> 'a option

Decomposition:

let flatten opt =
    match opt with
    | Some inner -> inner
    | None -> None

4.14 Option.map2

Option.map2 : ('a -> 'b -> 'c) -> 'a option -> 'b option -> 'c option

Decomposition:

let map2 f opt1 opt2 =
    match opt1, opt2 with
    | Some x, Some y -> Some (f x y)
    | _ -> None

4.15 Option.map3

Option.map3 : ('a -> 'b -> 'c -> 'd) -> 'a option -> 'b option -> 'c option -> 'd option

Decomposition:

let map3 f opt1 opt2 opt3 =
    match opt1, opt2, opt3 with
    | Some x, Some y, Some z -> Some (f x y z)
    | _ -> None

5. SSA Cost Formulas

Option operations are extremely lightweight:

6. Normative Requirements

1. Stack Allocation: On a pathway that realizes memory layouts, option values SHALL always be stack-allocated (voption semantics)
2. Tag Encoding: On a pathway that realizes memory layouts, None = 0, Some = 1; tag width per platform policy (minimum i8)
3. No Null: None SHALL NOT be represented as a null pointer; on a layout-realizing pathway it is a valid struct with tag=0, and on the JSIR pathway an erased None is undefined per §2.1, never null
4. Decomposition: Option HOFs SHALL be decomposed by Baker to primitive operations
5. Lazy Defaults: defaultWith and orElseWith SHALL only evaluate thunk when needed
6. Vacuous Truth: Option.forall on None SHALL return true
7. Tag Is Not Boolean: On a pathway that realizes memory layouts, tag MUST be at least i8, NEVER i1, because tags are case indices, not truth values
8. JSIR-Pathway Realization: On the JSIR pathway, option<'T> SHALL be realized erased or reified per §2.1, with the erased form selected only under the §2.1 proof; requirements 4, 5, and 6 bind on every pathway

7. Relationship to Result

Option and Result are both sum types with similar operation patterns:

When to use Option: Absence of value (lookup miss, empty input).

When to use Result: Failure with explanation (validation error, IO failure).

8. References

• Native Type Universe § 5.1 Option - Option memory layout
• Baker OptionRecipes.fs - Implementation reference