Static Analysis

Summarized using AI

Softly, Softly Typing

John Cinnamond • November 15, 2015 • San Antonio, TX

The video titled "Softly, Softly Typing" features John Cinnamond's keynote, presented at RubyConf 2015, focusing on the concept of soft typing in Ruby. Soft typing combines the advantages of static typing with the dynamic flexibility that Ruby offers. Cinnamond discusses how Ruby currently lacks mechanisms for type checking, which can lead to runtime errors when methods are called on objects that do not support them.

Key points discussed include:
- Definition of Soft Typing: It includes static type checking benefits while maintaining the flexibility of dynamic typing. This represents a philosophical shift regarding how correctness is perceived in Ruby.
- Lack of Discussion in the Community: Cinnamond notes that despite Matz's mention of static typing for Ruby 3, the community has not widely discussed soft typing, with only a few references made at events like RubyConf Australia.
- Introduction of Static Type Analyzer: The talk includes a plan to create a static type analyzer designed to better understand how soft typing can improve Ruby. By simplifying Ruby’s complexities, Cinnamond aims to make type theory more accessible.
- Building a Simple Language: To illustrate the principles, Cinnamond introduces creating a basic programming language (named "Trump") and designs a parser for it, discussing how to interpret and process expressions.
- Interaction with Dynamic Typing: Throughout the presentation, Cinnamond explains how implementing type checking while retaining Ruby’s dynamic nature is crucial, emphasizing that it should enhance the language rather than change its core principles.
- Encouraging Exploration: He encourages Ruby developers to engage with soft typing, emphasizing that understanding types can lead to improved coding practices and better program structures in Ruby.

In conclusion, Cinnamond highlights the potential benefits of integrating soft typing into the Ruby programming landscape. He conveys excitement about type systems, urging developers to consider how adopting such constructs could improve their development experience. He also encourages attendees to explore the code related to his talk on GitHub and invites discussions on the topic after the presentation.

Softly, Softly Typing
John Cinnamond • November 15, 2015 • San Antonio, TX

Softly, softly typing by John Cinnamond

The ruby community is large and varied but, for the most part, we haven't rushed to engage with type theory. Static typing - whatever that is - is for the slow moving world of Java developers. Type theory is for Haskell weirdos.

All that could be about to change.

In his keynote at Rubyconf 2014 Matz spoke about some ideas for Ruby 3, including the idea of adding static typing - or more specifically soft typing - to the language. So what is soft typing? How do we understand more about it? And what does it mean for us mere developers?

Help us caption & translate this video!

http://amara.org/v/H0zo/

RubyConf 2015

00:00:15.039 Okay, this is a talk about soft typing. Soft typing is something that might spook a lot of people. Matz spoke about it at RubyConf last year as one of the possibilities for Ruby 3.
00:00:20.660 So, what is soft typing? In essence, it combines the benefits of static typing with the flexibility of dynamic typing. Let me give an example of what this might mean.
00:00:33.140 Here’s a simple piece of Ruby code: it’s just a method that takes an argument and calls `x * 2` on it. Now, because this is Ruby, we don't need to tell it anything about the types. However, this also means we don't know much about the types. But there are some things we can work out just by looking at the code.
00:00:50.449 For example, we can say that whatever this thing is, it has to respond to `x * 2`. If we call this method while passing in some kind of object, that object also has to respond to `x * 2`. If it doesn’t respond, our code is going to throw a runtime error.
00:01:12.159 The important point here is that static type checking allows us to work out issues without having to run the code. This is a huge idea for Ruby, as previously there was no way to think about correctness without executing the code. This represents a significant philosophical shift in how we think about correctness in Ruby.
00:01:30.829 Given that this is a potential candidate for Ruby 3 and considering the significance of these ideas, you would think a lot of people would discuss soft typing. However, nobody really seems to be talking about it.
00:01:50.310 There was one talk by Tom Stuart at RubyConf Australia titled 'Consider Static Typing', which served as a primer on types and their usefulness. At the end, he mentions a bit about soft typing in Ruby, but aside from that, I've heard nothing. Even at conferences, speaking with people, it seems that nobody is thinking about it or discussing it.
00:02:08.630 So, I’d like to address that today. I thought it would be a good idea to give a talk about what soft typing is, how it works, and what it really means. This involves talking about type reconstruction for a late-binding, structurally typed language like Ruby and then working out how we deal with inevitable failures.
00:02:26.480 I started with a bigger idea for this talk, but then I wrote it, and it turns out that it was really boring. There wasn't a lot of heavy academic theory in there, and I thought a lot of you would just get up and leave.
00:02:37.430 Not only is it boring, but it's also really difficult. I'm not sure I could talk to you about how soft typing works; it's too hard for me. Additionally, if that weren't bad enough, it's really impractical. Even if I could teach it to you, by the end you would probably only know some mathematics about type systems in functional languages like ML, which has never left academia.
00:02:44.569 You couldn't really apply that knowledge to your everyday Ruby work. Boring, difficult, and impractical—this is going to be like the best talk you've ever seen! No, I think this is the way a lot of people think about type theory in general, and certainly if you've read the soft typing paper, these are terms you might use to describe it.
00:03:08.000 But this isn't how I feel about type theory, and it's not how I feel about type theory in Ruby. I think it's an exciting area. I believe it's something we can engage with as Rubyists, and I think it can improve our Ruby code.
00:03:30.769 What I want to do today is make this more accessible. I can't tell you everything you need to know about soft typing, but I might be able to give you an idea of where to start or how to explore this topic.
00:03:49.549 I'm going to do this by writing a static type analyzer. So, what does that actually mean, and how do you write one? There's a talk by Matt Might, a professor at the University of Utah, called 'What is Static Analysis'.
00:04:08.569 In that talk, he gives a general formula for how to write a static analysis tool, such as a static type analyzer. Imagine you've written a program and feed it into the interpreter, which is designed to run the code and produce the resultant value.
00:04:27.919 For example, you might run your program and get the value 42. To make this more abstract, instead of saying the answer is 42, you'd say the answer is just a number or that it’s something more abstract about the value. It could be more generally described, for example, as 'a number greater than ten'.
00:05:14.570 To simplify, I'm going to write a static type analyzer by constructing a more abstract interpreter. Ruby is quite complicated, so rather than using it directly, we’ll create a very simple programming language, which I will then write an interpreter for in Ruby.
00:05:38.840 This simple language will allow us to assign numbers to variables and later retrieve those variables. To build an interpreter for this language, we need to consider how we interpret the code as human beings. We see this as a series of expressions that can be classified into different types.
00:06:23.080 The first challenge is to impose structure on the raw code. We can do this using a parser, which will take the string of characters and produce some structured data. In Ruby, there are a variety of gems available for parsing, and today, I’ll use one called Parsley, which I find quite easy to work with.
00:06:43.260 Before we proceed, I need to name my programming language for practical reasons—specifically naming classes and defining the structure. Let's consider an appropriate name. One option could be 'Simple', but that might limit the complexity we could later introduce.
00:07:06.890 So, for no particular reason, I'm going to call it 'Trump'. Let's start developing a parser for it. I’ll define a class titled 'TrumpParser' which will inherit from Parsley. When creating this parser, I will start by identifying the root of the language as a series of expressions, which we can later define.
00:07:32.990 We will set rules that identify what constitutes an expression. We’ll assume it starts simply with a number. A number would be defined as one or more digits. As a result, we will build the language around this basic structure and create a sample source program that represents a valid number.
00:09:03.230 Initially, if we pass the input string with just a number, the parser accepts it. However, if we introduce invalid characters (like letters) that we haven’t defined rules for, the parser throws an error, indicating it doesn’t understand how to parse the input.
00:09:37.900 To improve our parser, we need to handle spaces gracefully. We’ll create rules for them, defining what constitutes a space character and enabling our parser to accept expressions with spaces both before and after them.
00:10:58.500 In doing so, our parser will return structured output rather than just strings, transforming basic identifiers and their values into a more complex structure that interpreters can eval.
00:11:56.540 Now we can extend our language to include assignments, where we can store a variable with a value. For example, we’ll say that identifications are simple lowercase sequences of characters. We’ll develop rules that will not only identify assignments but also refine our value classifications.
00:12:45.310 We can iterate on our structure by allowing more complex expressions. We will explore how to represent assignments and variables while dealing with their interactions in our created language.
00:14:33.230 Now that we have compiled our basic structure, I want to evolve this into actual Ruby objects. Once expressed in these objects, we’ll be able to write interpreters to evaluate each expression in a manageable and coherent way.
00:15:34.750 This process also involves creating an environment that can encapsulate variable states and allow us to efficiently track changes and values as they are evaluated through each expression in our structure.
00:17:00.140 Eventually, as we set evaluation methods, we'll begin inspecting how to interpret our newly formatted code while maintaining an association with the values established in our environment.
00:18:13.990 With our framework established and sufficient evaluations in place, we can develop the type-checking algorithm, allowing us to examine if our dynamic language can accurately depict its types.
00:19:04.590 Through our type-checking system, we can determine and potentially infer types from complex expressions and provide context-sensitive insights about validity and structure in Ruby.
00:20:00.430 I’ll further extend this language to include function declarations, allowing us to pass arguments and manage function calls. This addition will enable a richer set of operations while maintaining the existing dynamic typing foundations.
00:23:04.650 Finally, I want to expand the language to allow expressing errors and handling unexpected behavior through 'maybe' constructs, simulating runtime uncertainties.
00:25:20.800 In essence, our goal is to clarify how soft typing can aid in reducing the ambiguity of Ruby's nature and provide beneficial insights across various expressions and dynamic types.
00:27:20.100 Throughout this process, we’ve discussed how soft typing presents a refreshing way to enhance our development experience in Ruby. The interplay between types and semantic expressions can lead us to better-structured programs that adhere to our expectations.
00:29:48.070 It’s crucial to recognize how the integration of typing doesn't necessitate a huge shift in Ruby's syntax and semantics, while still preserving what developers love about the language.
00:30:30.650 As audience members, I encourage you to think openly about type systems and how engaging with them can yield significant benefits in your Ruby experience. Developing an interest in types could promote better practices and understanding as Ruby evolves.
00:31:48.190 I presented a lot of ideas today, and I hope at least some of you found them compelling or accessible in a way that prompts you to further explore soft typing. The entire code used in this talk is available on GitHub, and I encourage you to engage with it.
00:33:48.139 Thank you very much for listening.
00:34:05.000 Now, I will take some questions. I'm generally not a big fan of questions at the end, but I’ll be hanging around over the next three days. If you have anything to say, please come up and discuss it with me. Even if it’s just to say you find it boring, I would be interested to know.
00:39:58.360 As I answer your questions, be aware that non-determinism in Ruby is a significant aspect of the language's appeal. However, as we consider type-checking and static types, such non-deterministic behavior can complicate the predictability of our type system.
00:42:14.170 With this thought in mind, I'm keen to explore how we might balance dynamic flexibility against structured typing in Ruby without compromising the expressiveness that we cherish.
00:43:59.740 If anyone has any remaining inquiries or feedback regarding the talk, let’s engage in that discussion. Thank you once again!
Explore all talks recorded at RubyConf 2015
+76