TypeProf: Abductive Reasoning for Abstract Interpretation

Ruby News 23 August, 2021 | 10:20:00 UTC (+0000)
Tweet
Copy Link

When I see a bird that walks like a duck and swims like a duck and quacks like a duck, I call that bird a duck - Heim, Michael. Exploring Indiana Highways

TypeProf is a Ruby interpreter that abstractly executes Ruby programs at the type level. It executes a given program and observes what types are passed to and returned from methods and what types are assigned to instance variables. All values are, in principle, abstracted to the class to which the object belongs, not the object itself.

class User
  def initialize(name:, age:)
    @name, @age = name, age
  end
  attr_reader :name, :age
end

# A test case to tell TypeProf what types are expected by the class and methods
User.new(name: "John", age: 20)

Result:

$ typeprof -v test.rb
# Classes
class User
  attr_reader name : String
  attr_reader age : Integer
  def initialize : (name: String, age: Integer) -> [String, Integer]
end
Abstract values

TypeProf abstracts almost all Ruby values to the type level, with some exceptions like class objects. To avoid confusion with normal Ruby values, we use the word “abstract value” to refer the values that TypeProf handles.

TypeProf handles the following abstract values.

  • Instance of a class
  • Class object
  • Symbol
  • untyped
  • Union of abstract values
  • Instance of a container class
  • Proc object

Instances of classes are the most common values. A Ruby code Foo.new returns an instance of the class Foo. This abstract value is represented as Foo in the RBS format, though it is a bit confusing. The integer literal 42 generates an instance of Integer and the string literal ”str” generates an instance of String.

Limitations

Some Ruby language features cannot be handled because they abstract values.

Basically, it ignores language features whose object identity is important, such as singleton methods for general objects. Note that class method definitions are handled correctly; class objects are not abstracted for the sake. Currently, TypeProf only handles instance methods and class methods; it has no general concept of metaclasses (a class of a class). Meta programming is only partially supported.

  • Module#attr_reader and Object#send handle correctly only when symbol abstract value is passed (for example, when written in a symbol literal).
  • Kernel#instance_eval only supports the function to replace the receiver object when a block is passed (the contents of the string are not tracked).
  • Class.new is not supported; it always returns untyped.
  • Kernel#require has a dedicated support only when the argument string is a literal.

Read more by the Link to Github

Please Let us know your thoughts below!

Interested in earlier pieces of news?

Dig into our archived posts! We’ve got some awesome gems for you there!

Browse Archives