Class: Rigor::Type::App

Inherits:
Object
  • Object
show all
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

Constructor Details

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

Returns a new instance of App.

Raises:

  • (ArgumentError) 


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

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.



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

def args
  @args
end

#bound ⇒ Object (readonly)

Returns the value of attribute bound.



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

def bound
  @bound
end

#uri ⇒ Object (readonly)

Returns the value of attribute uri.



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

def uri
  @uri
end

Instance Method Details

#==(other) ⇒ Object Also known as: eql? 



85
86
87
 
# File 'lib/rigor/type/app.rb', line 85

def ==(other)
  other.is_a?(App) && uri == other.uri && args == other.args && bound == other.bound
end

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



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

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

#bot ⇒ Object 



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

def bot
  bound.bot
end

#describe(verbosity = :short) ⇒ Object 



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

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

#dynamic ⇒ Object 



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

def dynamic
  bound.dynamic
end

#erase_to_rbs ⇒ Object 



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

def erase_to_rbs
  bound.erase_to_rbs
end

#hash ⇒ Object 



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

def hash
  [App, uri, args, bound].hash
end

#inspect ⇒ Object 



94
95
96
 
# File 'lib/rigor/type/app.rb', line 94

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).



101
102
103
104
 
# File 'lib/rigor/type/app.rb', line 101

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

#top ⇒ Object 



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

def top
  bound.top
end