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 %a{rigor:v1:hkt_register} time, defaulting to Rigor::Type::Dynamic[Rigor::Type::Top] 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) 


38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
 
# File 'lib/rigor/type/app.rb', line 38

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.



36
37
38
 
# File 'lib/rigor/type/app.rb', line 36

def args
  @args
end

#bound ⇒ Object (readonly)

Returns the value of attribute bound.



36
37
38
 
# File 'lib/rigor/type/app.rb', line 36

def bound
  @bound
end

#uri ⇒ Object (readonly)

Returns the value of attribute uri.



36
37
38
 
# File 'lib/rigor/type/app.rb', line 36

def uri
  @uri
end

Instance Method Details

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



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

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

#bot ⇒ Object 



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

def bot
  bound.bot
end

#describe(verbosity = :short) ⇒ Object 



54
55
56
57
 
# File 'lib/rigor/type/app.rb', line 54

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

#dynamic ⇒ Object 



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

def dynamic
  bound.dynamic
end

#erase_to_rbs ⇒ Object 



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

def erase_to_rbs
  bound.erase_to_rbs
end

#inspect ⇒ Object 



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

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



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

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

#top ⇒ Object 



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

def top
  bound.top
end