Class: Rigor::Type::App

Inherits:
Object
  • Object
show all
Includes:
ValueSemantics
Defined in:
lib/rigor/type/app.rb

Overview

A defunctionalised higher-kinded type application — the abstract “apply type-constructor ‘uri` to argument list `args`” carrier.

‘uri` is a namespaced `Symbol` of the form `:author::name` (e.g. `:“json::value”`, `:“dry_monads::result”`); the `::` namespace separator is mandatory per ADR-20 WD1 to prevent cross-plugin tag collisions.

‘args` is an ordered, frozen `Array` of `Rigor::Type` values carrying the application’s argument list. At least one argument is required; arity-zero “HKT” forms are not modelled by this carrier (use a plain type alias instead).

‘bound` is a `Rigor::Type` representing the value Rigor MUST erase to when this `App` cannot be reduced — registered at `%arigor:v1:hkt_register` time, defaulting to `:Type::Dynamic` per ADR-20 D5 / WD2. It also drives the lattice probes (`top` / `bot` / `dynamic`) and the acceptance fallback while no reduction is wired (Slice 1).

Slice 1 ships the carrier as opaque: every operation delegates to ‘bound` since no reduction surface exists yet. Slice 2 introduces the conditional / indexed-access evaluator that reduces `App` to its registered body before delegating; the carrier shape stays identical.

Display form per ADR-20 OQ5: bare RBS-style ‘uri[arg1, arg2]`, not the wrapped `App[uri, [arg1, arg2]]` faithful form. Two `App` values are structurally equal iff their `uri`, `args`, AND `bound` match.

See docs/adr/20-lightweight-hkt.md.

Constant Summary collapse

URI_SEPARATOR = 
"::"

Instance Attribute Summary collapse

Instance Method Summary collapse

Methods included from ValueSemantics

included

Constructor Details

#initialize(uri, args, bound:) ⇒ App

Returns a new instance of App.

Raises:

  • (ArgumentError) 


45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
 
# File 'lib/rigor/type/app.rb', line 45

def initialize(uri, args, bound:)
  raise ArgumentError, "uri must be a Symbol, got #{uri.class}" unless uri.is_a?(Symbol)
  unless uri.to_s.include?(URI_SEPARATOR)
    raise ArgumentError,
          "uri must be namespaced as `:author#{URI_SEPARATOR}name` per ADR-20 WD1, got #{uri.inspect}"
  end
  raise ArgumentError, "args must be an Array, got #{args.class}" unless args.is_a?(Array)
  raise ArgumentError, "args must be non-empty (use a plain type alias for arity-0 forms)" if args.empty?
  raise ArgumentError, "bound must be a Rigor type, got #{bound.class}" if bound.nil?

  @uri = uri
  @args = args.dup.freeze
  @bound = bound
  freeze
end

Instance Attribute Details

#args ⇒ Object (readonly)

Returns the value of attribute args.



43
44
45
 
# File 'lib/rigor/type/app.rb', line 43

def args
  @args
end

#bound ⇒ Object (readonly)

Returns the value of attribute bound.



43
44
45
 
# File 'lib/rigor/type/app.rb', line 43

def bound
  @bound
end

#uri ⇒ Object (readonly)

Returns the value of attribute uri.



43
44
45
 
# File 'lib/rigor/type/app.rb', line 43

def uri
  @uri
end

Instance Method Details

#accepts(other, mode: :gradual) ⇒ Object 



82
83
84
 
# File 'lib/rigor/type/app.rb', line 82

def accepts(other, mode: :gradual)
  Inference::Acceptance.accepts(bound, other, mode: mode)
end

#bot ⇒ Object 



74
75
76
 
# File 'lib/rigor/type/app.rb', line 74

def bot
  bound.bot
end

#describe(verbosity = :short) ⇒ Object 



61
62
63
64
 
# File 'lib/rigor/type/app.rb', line 61

def describe(verbosity = :short)
  rendered = args.map { |t| t.describe(verbosity) }.join(", ")
  "#{uri}[#{rendered}]"
end

#dynamic ⇒ Object 



78
79
80
 
# File 'lib/rigor/type/app.rb', line 78

def dynamic
  bound.dynamic
end

#erase_to_rbs ⇒ Object 



66
67
68
 
# File 'lib/rigor/type/app.rb', line 66

def erase_to_rbs
  bound.erase_to_rbs
end

#inspect ⇒ Object 



90
91
92
 
# File 'lib/rigor/type/app.rb', line 90

def inspect
  "#<Rigor::Type::App #{describe(:short)} (bound=#{bound.describe(:short)})>"
end

#reduce(registry, fuel: nil) ⇒ Object

ADR-20 Slice 2a — reduce this application against a registry. Returns the reducer’s output (‘bound` when reduction is blocked or fuel exhausts).



97
98
99
100
 
# File 'lib/rigor/type/app.rb', line 97

def reduce(registry, fuel: nil)
  fuel ||= Inference::HktReducer::DEFAULT_FUEL
  registry.reduce(self, fuel: fuel)
end

#top ⇒ Object 



70
71
72
 
# File 'lib/rigor/type/app.rb', line 70

def top
  bound.top
end