00:00:10
It looks like it's time to start my presentation. My presentation is about type checking for Ruby programs.
00:00:26
Okay, let me introduce myself. I am Soutaro Matsumoto, and you can find me on Twitter or GitHub.
00:00:34
I work as the CTO at a startup company called Solution, located in Tokyo. Our product is called Debut Assistant, which automatically reviews requests and provides suggestions.
00:00:51
Technically, this involves program analysis. I have been working on program analysis for over ten years, analyzing properties of programs without executing them, including flow analysis and type checking.
00:01:12
In 2005, as a graduate student, I started studying program analysis and published some papers about type checking in Ruby programs. So yes, I have a decade of experience working on this problem.
00:01:39
So, what's the benefit of type checking? As you know, it helps you find more bugs without executing your tests.
00:01:54
If your program contains some erroneous code, type checking can identify those issues. If you pass an incorrect argument to some method calls, type checking will alert you.
00:02:26
It helps you identify more faults in your program. Additionally, it acts as verifiable documentation. When writing libraries or application code, you will see a lot of documentation.
00:02:43
This documentation indicates which methods are available in a class and how to pass arguments to them. Typically, this documentation is written using natural language in English or Japanese, which is understandable for humans but not for computers.
00:03:07
With types, a type checking tool can verify this instead of you. It also assists with refactoring. When you work on legacy code and change method signatures or names, you need to update all locations where these methods are called.
00:03:38
Instead of using grep or running tests to find all calls, a type checking tool can help you locate where you need to make changes. Another major benefit of type checking is optimization, but that discussion is beyond the scope of my talk.
00:04:02
This is a brief overview of type checking in Ruby. Humans have tried to type check Ruby programs for about ten years. I have listed four type checking tools developed by various researchers, including myself.
00:04:27
The first generation of type checking tools dates back to 2007 or 2009, which focused on typing objects in Ruby using duck typing. The second and third-generation tools, which are now available, support meta programming.
00:04:58
The challenges of type checking Ruby programs stem from at least three difficulties. The first difficulty is type inference. Ruby is a dynamically typed language, meaning that there are no type annotations included in Ruby code.
00:05:35
To check the consistency of types in your Ruby code, we must infer the types of expressions that are only known within your program. This type inference poses the first challenge.
00:06:02
The second challenge pertains to the semantics of duck typing. Duck typing signifies that the type of the receiver does not matter when you call methods. This differs from other popular statically typed languages like Java.
00:06:25
Let me clarify this with an example. The right method takes one argument called IO and uses the left shift operator to print a string. From our perspective using subtypes, any object that supports the left shift operator can work.
00:06:59
For instance, we can use this method for files, strings, and even arrays. They all support the left shift operator, so we can use them without issue.
00:07:31
To support duck typing semantics, I would like to introduce a paper titled 'Static Type Inference,' published in 2009 by Professor Foster and his students. This paper is based on structural subtyping and requires some annotations for better understanding.
00:08:07
I found that the implementation is still available on GitHub, called Diamondback Ruby, which demonstrates structural subtyping and its use in Ruby.
00:08:38
Now, let's go through an example. The right method's type will show that it takes one object as an argument, which must support the left shift operator and accept a string.
00:09:10
In our method, we can pass various types. For instance, if we pass a string, the type checker will recognize it as valid because the string class includes a left shift operator.
00:09:45
Similarly, if we pass a string IO, which also has a left shift operator, this will also be valid. However, if we pass a true class or an integer, we will get a type error because those do not have a compatible method.
00:10:09
This provides an easy explanation of the structural subtyping challenges. While Diamondback Ruby can infer some types of Ruby programs, it cannot handle polymorphic methods.
00:10:34
For example, the ID method takes an argument and returns that argument immediately. Calling ID 3 returns a number, while passing a string to ID will yield a valid result as well.
00:10:58
However, Diamondback Ruby struggles to infer types for polymorphic methods, resulting in type errors, which typically arise from its limitations on built-in types.
00:11:24
My paper discusses type inference for Ruby programs based on polymorphic type levels and was published in 2007. This approach seeks to infer polymorphic message types in Ruby, encoded in a manner akin to ML-root type inference.
00:11:47
However, there are limitations, as it struggles with certain Ruby routines like array, hash, and map.
00:12:02
In conclusion, we can assign types to Ruby objects using structural or polymorphic types, which offers a good approximation of Ruby's type semantics.
00:12:24
The subtyping relation is well-defined if that type has a method. However, the challenges in type inference persist.
00:12:47
We questioned whether we truly need type inference for Ruby. Thus, we introduced the concept of local typing points, which serves as a weaker version of type inference.
00:13:11
We focus on inferring the types of local elements, such as local variable types, instead of importing types across the entire program.
00:13:40
Using local type inference, programmers should write the types of method arguments and return types. An advantage of this is that it easily integrates with existing languages like Scala and Swift.
00:14:07
Here's an example of a Ruby program with no type annotations. To type check this program, we would need either complete type inference or some type annotations to indicate local variable types.
00:14:32
In this scenario, we should annotate method arguments and return types, as well as local variable types, which in turn derive their types from their right-hand sides.
00:15:08
With local type inference, we should specify type annotations for method parameters and return types, without needing to define types for local variables or block parameters.
00:15:45
Subsequently, I believe we should explore a mixture of structural subtyping and local type inference. Through this combination, we can effectively support Ruby's duck typing semantics while minimizing the number of annotations required.
00:16:15
The need for type checking difficulty can now be addressed locally. Instead of requiring complete type inference, we can adopt local type inference, using type annotations as needed.
00:17:07
We can address the difficulties of dynamically typed objects with structural subtyping and local type inference to minimize problems related to duck typing.
00:17:50
However, the challenges associated with meta programming remain. Meta programming involves modifying classes or method definitions at runtime, creating complexity in type checking.
00:18:25
Common meta programming features in Ruby, such as method creation and class modifications at runtime, make it challenging to infer the structures and types without executing the code.
00:19:06
For instance, defining an attribute reader dynamically obfuscates the path of the method and can create ambiguity during type checks.
00:19:41
Another example involves using Liqui, which can dynamically define methods during execution, further complicating type inference.
00:20:02
The execution flow impacts method presence, making it unclear if a method is available in a given context. This poses difficulties in establishing actual type structures without executing the program.
00:20:39
One possible solution is to provide special support for common meta programming patterns, such as attribute readers, to facilitate type checking.
00:21:05
However, this also brings challenges if a method is overridden or not properly implemented, leading to potential issues during type checks.
00:21:35
In conclusion, while we can address some of the type checking difficulties through structural or local type inference, certain dynamic programming constructs may remain challenging.
00:22:04
Static type checking may not yield good results with all Ruby programs because some properties cannot be statically inferred.
00:22:35
While various type checkers have been developed over the years, there is still much work needed in this area to achieve comprehensive type checking in Ruby.
00:22:51
This exploration of type integration has led to multiple findings and advancements, such as gradual typing, but it remains an open problem that needs further exploration.
