TypeProf Documentation

To avoid confusion with standard Ruby values, TypeProf uses the term abstract values to describe the entities it handles during type-level execution.

TypeProf supports the following abstract values:

• Instance of a class: Represents an object of a specific class (e.g., Foo.new returns the abstract value Foo). Note that literals like 42 are treated as instances of Integer.
• Class object: Represents the class itself (e.g., the constant Integer). TypeProf does not abstract these to the Class type to ensure constant references and class methods are handled correctly.
• Symbol: Represents symbol literals (e.g., :foo). Unlike other objects, symbols are often handled by their concrete value to support use cases like keyword arguments or JSON keys.
• untyped: An abstract value used when TypeProf cannot trace a value due to analysis limits. Operations on untyped result in untyped.
• Union of abstract values: Represents multiple possibilities for a value (e.g., Integer | String).
• Instance of a container class: Represents objects that contain other abstract values. Currently supported: Array, Hash, and Enumerator.
• Proc object: Represents closures from lambda expressions (-> {... }) or block parameters (&blk). These are treated as concrete pieces of code and represented in RBS using anonymous proc types.

To avoid losing precision, TypeProf uses "abstract values" instead of actual Ruby objects. Most values are abstracted to their class.

Supported abstract values include:

• Class instances: The most common value (e.g., 42 is an Integer instance). In RBS output, these are represented by the class name (e.g., Foo).
• Class objects: Represents the classes themselves (e.g., the constant Integer). These are not abstracted to Class to preserve constant references and class methods.
• Symbols: Literal symbols (e.g., :foo) are kept concrete. However, symbols generated via String#to_sym or interpolated symbols (e.g., :"foo_#{x}") are treated as the Symbol class.
• untyped: Used when TypeProf cannot track a value due to analysis limits. Operations on untyped result in untyped.
• Unions: Represents multiple possibilities (e.g., Integer | String).
• Container class instances: Currently supports Array, Hash, and Enumerator.
• Proc objects: Closures (lambdas or block arguments) are treated as concrete values tied to code fragments to track arguments and return values.

TypeProf is an interpreter that executes Ruby programs at a type level. Instead of tracking actual object values, it tracks "abstract values" (primarily the classes the objects belong to).

Key behaviors:

• Method Analysis: It observes what types are passed to methods and what types are returned, then generates RBS definitions.
• Revealed Types: It outputs observations of values (e.g., arguments to p) under a # Revealed types section.
• Instance Variables: Unlike standard Ruby where instance variables are unique to each object, TypeProf aggregates them at the class level. If different instances assign different types to the same instance variable, TypeProf represents this as a Union type (e.g., Integer | String).

def foo(n)
  p n      #=> Integer
  n.to_s
end

p foo(42)  #=> String

Analysis Output Example:

# Revealed types
#  test.rb:2 #=> Integer
#  test.rb:6 #=> String

# Classes
class Object
  def foo : (Integer) -> String
end

TypeProf is a Ruby interpreter that performs abstract interpretation. Instead of executing code with concrete values (like the number 42), it executes the program at the type level using abstract values.

The Analysis Process

1. Observation: As TypeProf executes the code, it observes what types are passed to methods, what types are returned from methods, and what types are assigned to instance variables.
2. Aggregation: While Ruby stores instance variables per object, TypeProf aggregates these values at the class level. If different instances of a class assign different types to the same instance variable, TypeProf represents that variable as a union type.
3. Output: TypeProf produces two main types of output:
   • Revealed types: A log showing the types observed at specific lines of code (e.g., test.rb:2 #=> Integer).
   • RBS format: A structured representation of the discovered class hierarchies and method signatures.

Example: Union Types in Instance Variables

If a class Foo has an accessor a, and one instance sets a to an Integer while another sets it to a String, TypeProf reveals the type as a union:

class Foo
  def initialize
    @a = 42
  end
  attr_accessor :a
end

Foo.new.a = "str"
p Foo.new.a #=> Integer | String

Output:

# Revealed types
#  test.rb:11 #=> Integer | String

# Classes
class Foo
  attr_accessor a : Integer | String
  def initialize : -> Integer
end

Scenario files use specific section headers to define input, expectations, and diagnostic requirements.

Basic Pattern

A minimal file requires two sections:

• ## update: Contains the input Ruby code.
• ## assert: Contains the expected type signatures written in RBS syntax.

Multiple Updates

You can chain multiple ## update and ## assert pairs within a single file to test how TypeProf handles sequential code changes or different implementation variations.

Diagnostics

To verify that TypeProf correctly identifies type errors, use the ## diagnostics section. This section should contain the expected error messages and their locations in the format (line,column)-(line,column): error_message.

## update
def foo(n)
  n.to_s
end

foo(42)

## assert
class Object
  def foo: (Integer) -> String
end

## diagnostics
(5,0)-(5,3): wrong number of arguments (2 for 1)