Class: Rigor::Inference::HktReducer

Inherits:
Object
  • Object
show all
Defined in:
lib/rigor/inference/hkt_reducer.rb

Overview

ADR-20 Slice 2a — reducer that walks a ‘Definition`’s ‘body_tree` against a concrete `Type::App` and returns a fully-typed `Rigor::Type`.

Reduction is the operational interpretation of ADR-20 § D4 (“Evaluation rules”):

  1. **Resolve ‘F`.** Look up the registered body via `registry.definition(uri)`.

  2. **Substitute arguments.** Walk the body tree, replacing ‘Rigor::Inference::HktBody::Param` nodes with the matching positional arg from the application.

  3. **Build types.** ‘Rigor::Inference::HktBody::TypeLeaf` returns its wrapped type as-is; `Rigor::Inference::HktBody::Union` and `Rigor::Inference::HktBody::NominalApp` route their reduced children through `Type::Combinator.union` / `.nominal_of` so normalization applies.

  4. **Recurse on ‘Rigor::Inference::HktBody::AppRef` nodes.** Reduce the args first; if the resulting `(uri, args)` matches an App already on the current reduction stack, return the in-progress `Type::App` carrier as-is (lazy self-reference handling — the standard “tying the knot” trick for recursive type aliases like `json::value`). Otherwise build a fresh `Type::App` and recursively reduce it against the same registry, sharing the fuel budget.

  5. **Fuel budget.** Each visited node consumes one unit. On exhaustion, reduction unwinds to ‘app.bound`.

The reducer is pure with respect to its inputs (the registry + the App) but uses a per-call mutable state bag for fuel + cycle tracking. Concurrent reductions MUST allocate fresh reducers (or fresh ‘_reduce` calls) — the per-call state is not shared.

Defined Under Namespace

Classes: FuelExhausted, State

Constant Summary collapse

DEFAULT_FUEL = 
64

Instance Method Summary collapse

Constructor Details

#initialize(registry) ⇒ HktReducer

Returns a new instance of HktReducer.

Raises:

  • (ArgumentError) 


46
47
48
49
50
 
# File 'lib/rigor/inference/hkt_reducer.rb', line 46

def initialize(registry)
  raise ArgumentError, "registry must be an HktRegistry" unless registry.is_a?(HktRegistry)

  @registry = registry
end

Instance Method Details

#reduce(app, fuel: DEFAULT_FUEL) ⇒ Rigor::Type

Reduce ‘app` against the registry.

Parameters:

  • app (Rigor::Type::App)
  • fuel (Integer) (defaults to: DEFAULT_FUEL) —

    reduction-step budget (default 64 per ADR-20 WD3). Each visited body node costs one unit. On exhaustion the reduction returns ‘app.bound`.

Returns:

  • (Rigor::Type) —

    the reduced type, or ‘app.bound` when reduction is impossible (URI not defined, arity mismatch, body_tree absent, fuel exhausted).

Raises:

  • (ArgumentError) 


61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
 
# File 'lib/rigor/inference/hkt_reducer.rb', line 61

def reduce(app, fuel: DEFAULT_FUEL)
  raise ArgumentError, "expected a Rigor::Type::App, got #{app.class}" unless app.is_a?(Type::App)

  definition = @registry.definition(app.uri)
  return app.bound if definition.nil? || definition.body_tree.nil?
  return app.bound if definition.params.size != app.args.size

  state = State.new(fuel: fuel)
  begin
    state.with_in_progress(app.uri, app.args, app) do
      walk(definition.body_tree, bindings: bindings_for(definition, app.args), state: state) || app.bound
    end
  rescue FuelExhausted
    app.bound
  end
end