The Type Séance

The Type Séance: this plan has no type annotations, but it HAD a run - and a run is a set of observations, and observations formalized are types. The séance sits with the departed execution, records the shape of every value that crossed every task seam, and transcribes what the spirits reveal as RBS. Then the strange part: the inferred signatures become a CONTRACT for the next run, and a poltergeist task - one that returns a different type the second time - is caught by the …

source on github

a real captured run

THE TYPE SEANCE (types are observations, formalized; the medium remembers)

  the sitting: one run observed at every seam, transcribed to RBS:
    def fetch: (void) -> Array[String]
    def parse: (Array[String]) -> Array[Hash[Symbol, untyped]]
    def score: (Array[Hash[Symbol, untyped]]) -> Array[Integer]
    def format: (Array[Integer]) -> String

  second honest run against the inferred contract: 4/4 seams conform

  then the poltergeist: a score task that was honest on its first
  visit (conformed) and changed its return type on the second:
    SEAM HAUNTED: score - promised (Array[Hash[Symbol, untyped]]) -> Array[Integer],
                  delivered (Array[Hash[Symbol, untyped]]) -> Array[Float]
    SEAM HAUNTED: format - promised (Array[Integer]) -> String,
                  delivered (Array[Float]) -> String

  gradual typing's whole wager, demonstrated seance-style: you do
  not have to WRITE the types - the program already knows them, at
  runtime, at every seam, and one observed run transcribes to RBS
  for free. what inference cannot give you is INTENT: the medium
  transcribed Integer because that's what score returned, not
  because score MEANT it - which is exactly why the poltergeist's
  Float is caught as a haunting rather than accepted as a wider
  union. note the contagion: score's lie condemned format's seam
  too (its INPUT shape changed) - type errors travel downstream
  wearing the caller's clothes, in seances as in Steep. observe
  first, formalize second, verify forever.

source

# frozen_string_literal: true

# The Type Séance: this plan has no type annotations, but it HAD a
# run - and a run is a set of observations, and observations
# formalized are types. The séance sits with the departed execution,
# records the shape of every value that crossed every task seam, and
# transcribes what the spirits reveal as RBS. Then the strange part:
# the inferred signatures become a CONTRACT for the next run, and a
# poltergeist task - one that returns a different type the second
# time - is caught by the ghost of its own first answer. You said
# Array[Integer] in life. The medium remembers.
#
#   bundle exec ruby examples/type_seance.rb
#
# Runs offline; exits 1 unless the séance transcribes correctly and
# the poltergeist is caught at exactly the lying seam.

require class="s">"bundler/setup"
require class="s">"agentic"

Agentic.logger.level = class="y">:fatal

# --- the medium: value shapes, transcribed to RBS-ish -------------------------------
def shape_of(value)
  case value
  when Array
    inner = value.map { |v| shape_of(v) }.uniq
    (inner.size == 1) ? class="s">"Array[#{inner.first}]" : class="s">"Array[untyped]"
  when Hash
    keys = value.keys.map { |k| shape_of(k) }.uniq
    vals = value.values.map { |v| shape_of(v) }.uniq
    class="s">"Hash[#{(keys.size == 1) ? keys.first : "untypedclass="s">"}, #{(vals.size == 1) ? vals.first : "untypedclass="s">"}]"
  else value.class.name
  end
end

# One sitting: run the plan, observe every seam, return the transcript
def hold_seance(score_agent)
  orchestrator = Agentic:class="y">:PlanOrchestrator.new(concurrency_limit: 1)
  observed = {}
  agents = {
    class="s">"fetch" => ->(_in) { [class="s">"7 lamps", class="s">"3 rugs", class="s">"9 clocks"] },
    class="s">"parse" => ->(lines) { lines.map { |l| {qty: l.to_i, item: l.split.last} } },
    class="s">"score" => score_agent,
    class="s">"format" => ->(scores) { class="s">"total: #{scores.sum}" }
  }
  previous = nil
  agents.each do |name, fn|
    task = Agentic:class="y">:Task.new(description: name, agent_spec: {class="s">"name" => name, class="s">"instructions" => class="s">"w"})
    orchestrator.add_task(task, previous ? [previous] : [], agent: ->(t) {
      input = t.previous_output
      output = fn.call(input)
      observed[name] = {in: input.nil? ? class="s">"void" : shape_of(input), out: shape_of(output)}
      output
    })
    previous = task
  end
  orchestrator.execute_plan
  observed
end

honest_score = ->(rows) { rows.map { |r| r[class="y">:qty] * 10 } }
poltergeist_visits = 0
poltergeist_score = ->(rows) {
  poltergeist_visits += 1
  (poltergeist_visits == 1) ? rows.map { |r| r[class="y">:qty] * 10 } : rows.map { |r| r[class="y">:qty] * 10.0 } # honest in life...
}

puts class="s">"THE TYPE SEANCE (types are observations, formalized; the medium remembers)"
puts

# --- sitting one: infer RBS from the honest run --------------------------------------
transcript = hold_seance(honest_score)
puts class="s">"  the sitting: one run observed at every seam, transcribed to RBS:"
transcript.each { |name, sig| puts class="s">"    def #{name}: (#{sig[class="y">:in]}) -> #{sig[class="y">:out]}" }
puts

# --- sitting two: the contract holds the honest, catches the poltergeist -------------
honest_again = hold_seance(honest_score)
conform = transcript.keys.select { |k| honest_again[k] == transcript[k] }
puts class="s">"  second honest run against the inferred contract: #{conform.size}/#{transcript.size} seams conform"

haunted_first = hold_seance(poltergeist_score) # visit 1: behaves
haunted_second = hold_seance(poltergeist_score) # visit 2: lies
violations = transcript.keys.reject { |k| haunted_second[k] == transcript[k] }
puts
puts class="s">"  then the poltergeist: a score task that was honest on its first"
puts class="s">"  visit (#{(haunted_first["scoreclass="s">"] == transcript["scoreclass="s">"]) ? "conformedclass="s">" : "?!class="s">"}) and changed its return type on the second:"
violations.each do |name|
  puts class="s">"    SEAM HAUNTED: #{name} - promised (#{transcript[name][class="y">:in]}) -> #{transcript[name][class="y">:out]},"
  puts class="s">"                  delivered (#{haunted_second[name][class="y">:in]}) -> #{haunted_second[name][class="y">:out]}"
end
puts

failures = []
failures << class="s">"inference wrong" unless transcript[class="s">"parse"] == {in: class="s">"Array[String]", out: class="s">"Array[Hash[Symbol, untyped]]"}
failures << class="s">"honest run failed its own ghost" unless conform.size == transcript.size
failures << class="s">"poltergeist not caught, or caught wrongly" unless violations.include?(class="s">"score") && violations.include?(class="s">"format")
failures << class="s">"score's lie mislabeled" unless haunted_second[class="s">"score"][class="y">:out] == class="s">"Array[Float]" && transcript[class="s">"score"][class="y">:out] == class="s">"Array[Integer]"

puts class="s">"  gradual typing's whole wager, demonstrated seance-style: you do"
puts class="s">"  not have to WRITE the types - the program already knows them, at"
puts class="s">"  runtime, at every seam, and one observed run transcribes to RBS"
puts class="s">"  for free. what inference cannot give you is INTENT: the medium"
puts class="s">"  transcribed Integer because that's what score returned, not"
puts class="s">"  because score MEANT it - which is exactly why the poltergeist's"
puts class="s">"  Float is caught as a haunting rather than accepted as a wider"
puts class="s">"  union. note the contagion: score's lie condemned format's seam"
puts class="s">"  too (its INPUT shape changed) - type errors travel downstream"
puts class="s">"  wearing the caller's clothes, in seances as in Steep. observe"
puts class="s">"  first, formalize second, verify forever."
exit(failures.empty? ? 0 : 1)