Option Operations Representation

Depends On: Native Type Universe § 5.1 Option

1. Overview

Operand-demand rules in this chapter describe ordinary deferred arguments. Direct explicit eager operands are demanded at their activated application/formation frontier, even where the selected Option case would not otherwise need them. Their completed values are shared, not replayed at a later partial stage or callback invocation.

Clef implements option operations (Option.map, Option.bind, Option.defaultValue, etc.) as Baker-decomposed pattern matches. On layout-realizing pathways, options are inline tagged values; any materialized storage follows the owning lifetime contract. Their operations elaborate to selected-case control flow without requiring a separately allocated managed option object.

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: Retain the input’s shared identity, test its case, and place payload projection inside the selected Some body. The None body retains the fallback’s shared computation. The payload read is not unconditional setup for the decision, and neither a tag test nor the unselected arm forces a payload.

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

4.16 Option.fold

Option.fold : ('State -> 'T -> 'State) -> 'State -> 'T option -> 'State

let fold folder state opt =
    match opt with
    | Some value -> folder state value
    | None -> state

The state and payload are independently quantified NTU types. Their dimensional and resource relationships SHALL be retained at the folder’s two argument edges and its result edge. The result has the supplied state’s type; there is no implicit widening or dimensional conversion between state and payload. Explicit type arguments use Option.fold<'State, 'T>.

4.17 Option.foldBack

Option.foldBack : ('T -> 'State -> 'State) -> 'T option -> 'State -> 'State

let foldBack folder opt state =
    match opt with
    | Some value -> folder value state
    | None -> state

Explicit type arguments use Option.foldBack<'State, 'T> in the same state, payload order as fold.

Both folds follow default demand and sharing. Demanding the fold result requires the option’s case. For Some, demand the folder’s result with the argument order shown; the folder determines demand for the state and payload. For None, return the supplied state’s shared computation without demanding or invoking the folder. A demanded state result is evaluated once through that shared identity. Supplying ordinary operands or forming a partial application SHALL NOT force unused folder, state or payload expressions. Partial applications retain already supplied values or deferred identities; captured storage retains its existing identity and lifetime obligations.

The declared three-argument operation boundary SHALL remain distinct from any subsequent application of a function-valued state result. Bare aliases SHALL instantiate the state and payload types independently at each admitted use. Baker SHALL elaborate these relationships into the graph before Alex witnesses the resulting conditional and calls; neither fold introduces an Alex intrinsic or relaxes admission requirements for its state, payload or folder.

5. SSA Cost Formulas

The following counts illustrate one fully demanded scalar lowering using undef, insertvalue and extractvalue notation. Baker SHALL settle demand, case guards and typed storage; Alex SHALL create the actual SSA operands through Elements, Patterns and Witnesses in the admitted portable dialects. Cost accounting SHALL use the operations and storage of the selected realization, including deferred payloads, aggregate layouts and target lowering.

6. Normative Requirements

1. Inline Value Representation: On a pathway that realizes memory layouts, option values SHALL use their admitted tagged value representation without requiring a separately allocated managed option object. Materialized values and retained payloads SHALL follow the containing value’s proved lifetime and storage authority under Discriminated Union Representation §8.2; a returned, captured or cached option SHALL NOT retain storage that expires before its uses.
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