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 {HktBody::Param} nodes with the matching positional arg from the application.
  3. Build types. {HktBody::TypeLeaf} returns its wrapped type as-is; {HktBody::Union} and {HktBody::NominalApp} route their reduced children through Type::Combinator.union / .nominal_of so normalization applies.
  4. Recurse on {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) 


36
37
38
39
40
 
# File 'lib/rigor/inference/hkt_reducer.rb', line 36

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) 


49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
 
# File 'lib/rigor/inference/hkt_reducer.rb', line 49

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
    BudgetTrace.hit(BudgetTrace::HKT_FUEL_EXHAUSTED)
    app.bound
  end
end