Danny Yang and Sam Goldman, both software engineers at Meta, speak with host Gregory M. Kapfhammer about the Rust-based Pyrefly type checker for Python. After a look at the foundational concepts for annotating and checking types for Python programs, Danny and Sam present a deep dive of the implementation of Pyrefly. While comparing and contrasting against various type checkers, they also describe how Pyrefly implements the language server protocol (LSP) for Python. The episode explores a range of other topics, including how to balance the features, performance, and language integrations of a type checker.
Brought to you by IEEE Computer Society and IEEE Software magazine.
Related Episodes
- SE Radio 622: Wolf Vollprecht on Python Tooling in Rust
- SE Radio 589: Zac Hatfield-Dodds on Property-Based Testing in Pytho
- SE Radio 516: Brian Okken on Testing in Python with pytest
- SE Radio 676: Samuel Colvin on the Pydantic Ecosystem
Other References
- Pyrefly Web: Pyrefly: A Fast Python Type Checker and Language Server
- Blog Post: Introducing Pyrefly: A new type checker and IDE experience for Python
- Github – pyrefly: A fast type checker and language server for Python
- Conformance of Type Checkers: How Well Do New Python Type Checkers Conform? A Deep Dive into Ty, Pyrefly, and Zuban — Rob’s Blog | Python • Rust • Ramblings?
- Python Type Checker Comparison: Empty Container Inference
- Making Pyrefly Diagnostics 18x Faster
- Lessons from Pyre that Shaped Pyrefly
Transcript
Transcript brought to you by IEEE Software magazine.
This transcript was automatically generated. To suggest improvements in the text, please contact [email protected] and include the episode number and URL.
Gregory Kapfhammer 00:00:18 Welcome to Software Engineering Radio. I’m your host Gregory Kapfhammer. Today’s guests are Sam Goldman and Danny Yang. Both Sam and Danny are software engineers at Meta Platforms, and they work on the Pyrefly Project. Hey, welcome to the show.
Sam Goldman 00:00:34 Hey Gregory, happy to be here.
Danny Yang 00:00:36 Thanks for having us.
Gregory Kapfhammer 00:00:37 No problem. Glad to chat with both of you today. Our topic is Pyrefly. Pyrefly is a Type checker and it’s a language server for Python and it was built at Meta and you’ve developed it and open-sourced it. And so, we’re going to dive into some details. Now to make sure that we’re on the firm footing at the very start of the episode, Sam, if I could turn to you at a high level, what’s a Type checker?
Sam Goldman 00:01:01 So a Type checker is a part of the software development process. Programmer is writing computer code. Their computer code might be written correctly or incorrectly, and a Type checker is one tool that programmers can use to find errors in the code that they’ve written.
Gregory Kapfhammer 00:01:19 Okay. Now many of our listeners may be familiar with programming in Rust or in Java and in those programming languages there is Type checking that goes on, but it doesn’t happen in an external tool. So Sam, can you develop that a little bit further?
Sam Goldman 00:01:35 Yeah, so in the context of Python specifically, a Type checker is a tool that someone needs to bring on separately. So, Python does not come with its own well static Type checker. And so a tool like Mypy or a Pyrefly is something extra that you would bring on and use to find bugs in your code.
Gregory Kapfhammer 00:01:57 Okay, that’s really helpful. Now you mentioned Mypy and we’ll talk about Mypy later in the episode. But Danny, if I could turn briefly to you, I also mentioned that Pyrefly is a language server. So, can you say a little bit about what it means for it to be a language server?
Danny Yang 00:02:12 Yeah, a language server is a piece of software that understands and conforms to the language server protocol, which allows it to communicate with various different editors to provide IDE features, for example, go to definition, hover, code actions, things like that. It’s a common protocol so that you can just implement one language server that conforms to the specification and you can have it work in VS code, Neovim and other editors like that.
Gregory Kapfhammer 00:02:41 Okay. So, if I’m understanding you two correctly, Pyrefly is both a Type checker and an LSP. Is that the right way to think about it? Yes. Okay, good. So, what we’re going to do at the beginning is talk a little bit about some of the basics of Python Type checking and then we’re going to talk about the design and implementation of Pyrefly, focusing on how you perform Type checking from an internal perspective. We’ll also talk about details related to the performance of Pyrefly, but in order to get started since Pyrefly is an add-on to the Python programming language, when do I use it? Where does it fit into my overall workflow as a Python programmer?
Sam Goldman 00:03:21 So you would use it while you are writing code. So, a great way to use it is say you use VS code as your main IDE, you can go right to the extension marketplace, search for Pyrefly and install it and it will start working right away. You’ll see the language server behavior, you can get syntax highlighting, you can jump to definitions and in the diagnostics pane Type errors would appear as a list and you can navigate to the location of the Type error in your code. So that’s one time where you would use it. Another place where it’s really, really common and a good idea to use Type checking is during CI continuous integration testing that you would perform for every change that goes into your code base.
Gregory Kapfhammer 00:04:09 Okay. So, I want to talk quickly about a few different terms that we often hear people mention when we talk about typing and Type systems. I know that typing started in PEP 484 and that was many years ago, and that Python has something that’s called a Type annotation. Can you tell us a little bit, Danny, what is a Type annotation in the Python programming language and how does it fit into the workflow that Sam mentioned a moment ago?
Danny Yang 00:04:33 So a Type annotation is some special syntax that you write into your Python program that lets you mark the Type of variables or functions, inputs and outputs, attributes of classes, things like that. So, when you run a Python program, normally the Python interpreter ignores the Type annotations and they don’t really matter for runtime, but the Type checker will read those annotations and check your code based on that. So, the element of standardization here is that Python has standardized this way of providing optional Type annotations in your code if you choose to do so and Type checkers should be able to understand those annotations.
Gregory Kapfhammer 00:05:14 Okay. So as a Python programmer, I don’t have to put the Types in my code, but if I put the Types there as annotations or hints, they help Pyrefly to do a better job. Is that the right way to understand it Danny?
Danny Yang 00:05:27 Yes. Even without annotations, a Type checker or a language server will try its best to analyze the code and do various levels of Type inference to guess the Types. But with concrete annotations typically the Type checker performs better.
Gregory Kapfhammer 00:05:41 Okay, that’s really helpful. You mentioned the word inference and often when I learn about Type checkers, I remember reading about inference and refinement. Can you briefly say what those two terms mean Danny?
Danny Yang 00:05:52 So Sam can correct me if he believes differently, but in my mind inference is where we are guessing a Type when the Type is not explicitly specified or annotated and refinement is a form of inference because we are guessing a narrower Type based on the structure of the code. So, for example, in a language like Java you might explicitly cast things, but in Python it’s much more common to assert some like structural properties of the code for example, like this variable has you use has attribute or you check the length of a two or something like that. And these Type checkers can understand to get more information about the Type and that’s refinement.
Gregory Kapfhammer 00:06:39 Sam, do you want to dive in and share any more details?
Sam Goldman 00:06:41 Yeah, I mean Danny was absolutely right. I think I want to add one more thing on refinement and why it’s so interesting in the context of Python is that Python by itself as a language is not statically Typed. So, the way that people write Python code is a little bit different from how you might write Rust or C++. And as a result, the code that we see and then we have to analyze includes a lot of runtime Type tests. So, you might write a function that can be called in a flexible way, maybe a caller can pass a string or a number to your function and the function will internally check say, hey is the argument that I receive a string? If it’s a string I’ll do one thing and if it’s a number I’ll do something else. And so, it’s really important for Pyrefly to be able to follow that logic in people’s code, which is why you see this refinement logic in Type checkers for dynamic languages like Python and TypeScript where it’s much less common or doesn’t exist at all in languages like Rust.
Gregory Kapfhammer 00:07:46 Okay, that’s helpful. Now I’ve heard both of you mention the word static and then also the word dynamic. And I know in the context of programming languages or software testing, we often talk about static analysis and dynamic analysis. So where does Type checking fit into static analysis versus dynamic analysis?
Sam Goldman 00:08:04 So well Type checking can appear in both places, but for Pyrefly is a static Type checker which means that we don’t run any code so we don’t get to see what’s happening when your program runs. We are looking at the source code before anything has happened.
Gregory Kapfhammer 00:08:23 Okay, so static analysis means you don’t run the program, you just study the source code. Is that the right way to think about it? Yeah. Okay, awesome. So obviously one of the key goals of a Type checker is that we want to be able to find bugs in our programs before we deploy them to production. And I don’t know who would want to jump in here, but could one of you share a concrete example or tell a story of how Type checking can actually find a bug in a program?
Danny Yang 00:08:53 So I can give an example of like an everyday thing that you would do in your code base and how Type checking can help. So for example, if you have a function and you want to refactor it to remove an argument, the Type checker would be able to give you an error at every single call site of that function and say, hey, you have to remove the argument at all of those places. And without it you would have to grab through the code base and find all the call sites, but you might not find everything because Python is pretty dynamic, right? You can alias functions, you can pass them around, it could be a function that has a common name and there’s like other functions across the code base that aren’t actually the same thing but have the same name. So, the Type checker just makes that process a lot easier and less error prone.
Gregory Kapfhammer 00:09:40 Okay, I get it. Now, one of the things I noticed is that there’s many different Type checkers or LSP implementations in the broader python landscape. So, for example, Mypy is a well-known Type checker and then there are other things that are LSPs like PyRIT, and then there’s something else called zon, which seems to be both a Type checker and a language server. So, I’m wondering if both of you could work together to give our listeners maybe a broad overview of the Python Type checking and LSP ecosystem. Can you help us out?
Sam Goldman 00:10:12 Yeah, I can give a high-level overview here. So, you mentioned PEP 484, which is the PEP, which introduced Type annotations to Python and this came from Mypy. Mypy is really the originator of typing in Python. So Mypy is a great piece of software. It’s been around for a long time. It is just a Type checker, it is not also a language server, it’s written in Python and pioneered a lot of the ideas in this space. So later on, I don’t know exactly when, but out of Microsoft there was the PyRIT project and PyRIT is a language server and Type checker. And I think that the reason why Pyre became so popular is that the language server features provide so much value that it’s really I think makes the value of Type checking connect with people in a really big way.
Sam Goldman 00:11:16 So for a long time the situation was that you had Mypy as the Type checker. It had been around for years, people were used to using it, but then people also started using PyRIT in the IDE because the language services are so powerful and useful but it’s a little bit awkward because then you have one Type checker doing analysis for language services, one Type checker giving you Type errors, they might not always agree and it’s a little bit of a unfortunate situation. So, there’s now a new school of Type Checker that’s coming out, Zavanti, Pyrefly, that all aim to be both highly efficient and highly compatible. And so now it’s a bit of a, I think inflection point in Python typing because there’s so many new entries into the space that are all trying to become the all in one solution.
Gregory Kapfhammer 00:12:08 Okay, that makes sense. I know many of our listeners may have used a Type checker before and they have worked on it in certain cases where it found a bug and then other cases where it flagged up a problem and then it wasn’t really a problem. So Danny, this leads me to my next question. What are false positives and false negatives and true positives and true negatives in the context of a program like Pyrefly?
Danny Yang 00:12:35 Yeah, so since Pyrefly is a static Type checker, it doesn’t have access to the information at runtime and runtime values. And to a certain extent it’s essentially like reading the code and trying to guess the programmer’s intent, especially when there are no annotations. So, there are cases when you can guess wrong. So, I would say a true positive is when Pyrefly flagged an error and it was actually a bug. A true negative is when there’s no error and there’s no bug. A false positive is if Pyrefly got confused somehow by the program and flagged an error when there was actually no bug and this code is actually fine and then a false negative would be like if there actually is a bug, but somehow it was not caught.
Gregory Kapfhammer 00:13:20 Thank you. So now my next question is perhaps deceptively simple, but I’m hoping you can tackle it as well. What does it mean if a program passes a Type checker? So, if I run Pyrefly check in my terminal window and it doesn’t give me anything to look at, what do I know about my program?
Danny Yang 00:13:37 It means that from Pyrefly’s perspective, the program and the Type annotations are consistent with each other.
Gregory Kapfhammer 00:13:45 Okay, I get it. Now the next thing I wanted to develop, and I’m hoping perhaps Sam, you can help me here, is that I’ve used multiple Type checkers on the same project and oftentimes but not always, they will actually flag up different Types of messages. Can you help our listeners understand why different Type checkers might actually flag different concerns about the same Python program?
Sam Goldman 00:14:09 Yeah, that’s a great question. So there are a lot of different reasons why that might happen, but I think the biggest difference would be choices that the Type checkers have made about how much to infer, how much to leave un Typed and then also just how complete of an implementation the Type checker has of the typing specification.
Gregory Kapfhammer 00:14:34 Okay, so they might disagree and then I’m going to have to do my diligence in order to discover which one seems to line up best with the pep specification for typing and then maybe look at both of them and as a developer make an educated decision on what to do next. Is that the kind of workflow?
Sam Goldman 00:14:52 Yeah, and I would say that it’s not a great workflow, so I don’t think it’s really a good place to be for the ecosystem to have multiple Type checkers that all disagree in significant ways. Hopefully if you have an experience like this where you’re using two or more Type checkers and they don’t give you the same exact advice, then at least all the advice you get will be useful. Okay. But it’s possible that maybe you’re using multiple different Type checkers, and you get some Type checkers have false positive, which is really not useful. Or a Type checker has a false negative where like, hey Mypy caught this but PyRIT didn’t. Why not?
Gregory Kapfhammer 00:15:32 Okay, I see what you’re getting at. So, to summarize really quickly, I think you’re saying that both false positives and false negatives are things that we would like to avoid when we’re building a Type checker and that true positives and true negatives are both good things when we’re building a Type checker. Did I catch that the right way?
Sam Goldman 00:15:51 Yeah, absolutely. And when we are working on Pyrefly, we really look closely at false negatives and false positives. It’s one of the main things that we track from release to release. Did we increase the amount of false positives or false negatives? If so, we have to follow up and investigate that. So, we look at a corpus of real-world code as we develop to see how we’re performing.
Gregory Kapfhammer 00:16:16 Okay, that makes sense. Now, one of the things I wanted to talk about next is the idea of gradual typing. And additionally, I know that the Python programming language supports something that’s called the Anytype. Danny, can you help the listeners to understand gradual typing and the use of something called any?
Danny Yang 00:16:33 Yeah, so I guess the Anytype is a Type that says the value can literally be anything in a very permissive way. If you have something that’s Anytype, you can pass it into a function regardless of whatever Type it takes. You can do whatever operations you want with it and it’s just signals. So, the Type tracker that we have no good information about this Type, so the Type tracker will treat it as compatible with anything. And that allows us to not give a lot of false positive errors when we actually don’t know anything about the Type.
Gregory Kapfhammer 00:17:05 Okay. If
Danny Yang 00:17:06 You use it as an explicit annotation, you can view it as like a backdoor, like, oh, this thing is too hard to Type, let’s give it an any. That’s one way to use it. But also, internally the Type checker will infer any in places where it doesn’t know. Like for example, if you annotate something with just list with no Type arguments, then it’ll has to guess a list of Anys.
Gregory Kapfhammer 00:17:27 Okay, I see what you’re getting at now I wanted to take a little bit of time to read one quotation, and I saw this on the Pyrefly website. And then I’d like to develop the idea of performance after I read the quotation. So Pyrefly’s website says that it can Type check over 1.85 million lines of code per second on META’S infrastructure. And I have to say Sam, that’s an incredible number. It’s nearly 2 million lines of code per second. So, can you tell our listeners why is performance so critical for Type checkers?
Sam Goldman 00:17:57 Well, I would say the performance is critical for all of our developer tools. I think everyone enjoys it when their tools are fast and then not just fast, but there’s a moment when a tool responds instantaneously. And I think at that moment a tool can really transform where you don’t think about using it, you can integrate it on every keystroke, and it becomes very conversational. And so that was one of our goals for Pyrefly.
Gregory Kapfhammer 00:18:25 That makes a lot of sense. And in fact, you used the word conversational and it makes me think about using a tool like Claude Code or Open Code. I’m guessing that performance is also really critical in the context of agent software engineering. Sam, can you develop that a little bit further?
Sam Goldman 00:18:41 Yeah, so for the last several months the industry has changed significantly, and we have been trying to adapt with those changes ourself. So it’s really interesting and I think the story is not quite told, but it’s true that if an agent can use a Type checker like Pyrefly as a tool and get better information, then it can help the trajectory of that agent interaction be better, tend towards success because the agent can verify it every step and that the more it can verify and the more cheaply it can verify the fewer tokens you use and the faster your interaction is with that agent.
Gregory Kapfhammer 00:19:18 Okay. So, in a way, Pyrefly can guide the agent towards a correct Python implementation because it’s flagging Type checking errors, giving that directly back to the agent, which passes it along to the LLM and then in a tight loop you can find bugs more rapidly because of the fact Pyrefly is so efficient. Did I summarize that workflow in the right way, Danny?
Danny Yang 00:19:40 Yeah, it’s very similar to how a human programmer would use a Type checker too, right? It tightens the feedback loop; it shifts errors left. You can see both a human and an AI in absence of a Type checker. Maybe they would run the full test suite of the program to verify that their change is correct and sit around for several minutes waiting for the test to run. But instead with the Type checker, they would be able to get updated signals on every keystroke or every file save. And that’s like a very powerful thing.
Gregory Kapfhammer 00:20:07 Okay, I’ve got it now what I want to do next is talk about how you actually built Pyrefly and I know Pyrefly was built in Rust, so I’d like to talk briefly about your decision to use Rust over other programming languages. Could both of you help our listeners out? Why did you pick Rust for Pyrefly?
Sam Goldman 00:20:24 So we chose Rust for a few reasons. I think it helps to get into a little bit of the history of our team because this team had previously built software called Pyre. So Pyrefly is the successor to Pyre, and Pyre was written in OCaml, which is a pretty niche functional programming language that’s popular with academics and also popular with programming language enthusiasts. And I love OCaml, so I love writing in OCaml and I’ve done it for the last decade, but Rust was really a great choice for us because we wanted to build a big open community and OCaml has a much smaller developer population, whereas Rust is very popular. People who don’t already know Rust are interested in learning Rust and a lot of people know Rust. Another big reason for our choice is the just sheer quantity of high-quality third-party code that we can pull it and use.
Gregory Kapfhammer 00:21:24 Okay, that’s really helpful. Now since we know a little bit about why you picked Rust, I know that it’s connected to Pyre, but you didn’t actually reuse any of the code from Pyre inside of your implementation of Pyrefly. Did I remember that correctly?
Danny Yang 00:21:38 Yes. Pyrefly is a spiritual successor. It doesn’t reuse any of the implementation of Pyre, but a lot of the lessons and designs from Pyre sort of influenced how we designed Pyrefly. So, we took some of the things that were good from it and also things that Pyre couldn’t do that we wanted to make sure Pyrefly could do and tried to learn lessons from where Pyre really couldn’t scale as well performance wise and things like that.
Gregory Kapfhammer 00:22:04 Okay. Now my next question is going to paint with a very broad brush, but with that initial comment out of the way, I’m going to say what I would call the three phases of pyre fly. So, in phase one you have to figure out what each module exports or imports and you have to solve imports transitively. In phase two you have to convert modules to bindings, and you have to take into account something called scope. And then in phase three you essentially have to solve those bindings. Now I recognize it’s much more complicated than that, but if I summarize it in terms of those three phases, could the two of you now work together and talk to our listeners through those three phases in greater detail?
Sam Goldman 00:22:45 Yeah, I think that the way you described it is definitely correct, but the first place I would maybe zoom out to is going from one file to many files. So, if we’re just talking about one file, then yeah, we parse into an AST, we turn the AST into an intermediate representation that we call bindings, which represents the AST after scope resolution has been done. So, if you use a variable name, where’s the definition of that name? And then we go through this process of solving the bindings and the bindings form a graph and the solution step is walking that graph doing analysis along the way. The reason it’s built that way is for laziness. So, this is when we zoom out from a single file where in maybe a large project with hundreds or thousands of files, Pyrefly is different from other tools in that it’s designed as a language service first.
Sam Goldman 00:23:45 If we were just building a Type checker, we would build it very differently where we would find all the files we would do for all the files in this batch processing mode. But when you build uh LSP first, you have to turn that whole process inside out. And this is where a lot of the key design decisions come in having this graph that can be lazily elaborated. So, you start where someone opens a file in the IDE and you want to be able to give them useful information within milliseconds. So, you can’t even spend time walking the whole file tree to discover what all the files are. You need to start from an entry point and expand out incrementally.
Gregory Kapfhammer 00:24:25 Thanks, that was both helpful and compelling. Now, a moment ago I mentioned the idea of solving imports in a transitive fashion. Danny, could you define the meaning of transitivity in the context of Pyrefly and Type checking?
Danny Yang 00:24:38 So when one file depends on another, it can be direct, which is like, okay, module A imports module B, but it can also be like a transitive thing. For example, module A imports a class for module B and that class has a field that’s Typed using a class defined in module C. So, then module A has a transitive dependency on a Module C.
Gregory Kapfhammer 00:25:03 Okay, that’s helpful. And then Sam, I remember a moment ago you were talking about how you turn it inside out when you look at it from an LSP perspective. So, can you tell us maybe from an LSP perspective, what’s the scope information that Pyrefly uses and in particular, what is scope in the context of a programming language?
Sam Goldman 00:25:23 Yeah, so scope in the context of a programming language is really a simple idea and it’s mapping of from names to definitions, which I think the easiest way to think about it and it’s something that developers have in their head at any given time, but when we talk about analysis and the algorithms to perform that analysis, we make scope specific concept. So, if you’re in a function and the function takes two parameters, X and Y and you add them together, you have this expression in your function X plus Y what does X mean? What does Y mean? The fact that those names map to the parameters, that’s what we would include in scope.
Gregory Kapfhammer 00:26:03 Okay, I got it. Now I’m wondering if you could tell our listeners maybe a key technical challenge you faced when it came to building Pyrefly or perhaps a story you could talk about improving the performance or the correctness of the tool. Does anything jump to mind?
Sam Goldman 00:26:19 I can think of one and it gets to this core idea of laziness. So, when you open a file, we will analyze that file, but we also might need to get information from the files that you import and then transitively from the files that those files import and so on and so on. So early in the design of Pyrefly we knew that we had to support this kind of laziness, but we didn’t always get it right all the time. So one of the bugs that we fixed early on was that whenever you imported a file we would eagerly analyze that entire file, which meant that if you had a project with a lot of third party code, sometimes you had a project that had maybe two or three files in it, but through its dependencies, third party libraries would have millions of lines of code and to Type check those files, it took sometimes over a minute when it should have taken just a few milliseconds. So, we had to increase the laziness in key places so that we didn’t end up analyzing all of the third-party dependencies.
Gregory Kapfhammer 00:27:26 Aha, I get it. So, if I’m a programmer and I’m using Django or I’m using FastAPI, you have to be careful from the perspective of laziness. If I import FastAPI, maybe you are not going to check everything inside a FastAPI right away. Do you just check the parts that it looks like I’m most likely to use? How do you decide when you have to overcome your laziness and start to analyze my imports?
Danny Yang 00:27:52 So we have an indexing job that runs when the language server first starts. So in addition to this fully lazy initial load that gets you information in the first file that you open, we also have something running in the background that indexes your project and sort of all the third party dependencies that it includes and that happens in the background and takes, several seconds. But once that’s done then everything fully works. But initially when it first loads you already have something working while Pyrefly is working in the background to solve the rest.
Gregory Kapfhammer 00:28:25 Okay, that makes a lot of sense. Now, when I was doing some research about Type checking for Python, I remember coming across something that was called Typeshed. Does Pyrefly use Typeshed and ultimately how does this idea of a third-party stub play into the idea of Type checking?
Danny Yang 00:28:41 Typeshed is a repository of Type stubs for various third-party packages that don’t have inline Type annotations. This can be for historical backwards compatibility reasons like oh maybe the package needs to work with like older versions of Python that don’t have typing. But sometimes maintainers just don’t want the trouble of maintaining Type annotations either. But for whatever reason, Typeshed is a sort of centralized place that stores these Type stuffs for third party packages and Pyrefly uses them by bundling some of the Type stubs to provide better IDE behavior out of the box. But if you’re writing a Python project, you can also add these Type Stub from PyPi as one of your dependencies and that way no matter which Type checker or language server you use, they will know about the Types.
Gregory Kapfhammer 00:29:32 Okay, so the way that I’m thinking about is that Typeshed is providing Type annotations if a project doesn’t natively provide the annotations, is that the right idea?
Sam Goldman 00:29:43 Yeah, that’s right.
Gregory Kapfhammer 00:29:44 Okay, awesome. So, I know a while ago you mentioned the idea of hovering and you talked about Goto definition and my understanding is that those are all things that happen inside of the IDE. So, could one of you tell me overall what are the things that would happen in my IDE and then what are the Types of things that would happen in a CLI or in an agent coding harness or in CICD? Can you walk us through that whole landscape?
Sam Goldman 00:30:11 Yeah, so in an IDE it’s very common to you’re reading code, you’re writing code, you’re navigating, you might Type class and then dot and from the dot you want to access a method or a field from that class. So, what Pyrefly and other language servers can do is give you a list of here are all the things that you can access from that class. So that’s something that you would do while you’re writing code, it’s an authoring action. We would say other actions are less about authoring and more about navigation. So maybe you say you’re reading some code, and you see a reference to a class, and you say well what is this class? What does it do? Or a function call. What you can do is you can command click or control click on that name in the code and Pyrefly will navigate, will open the file and navigate to the line where that definition exists in the code so then you can go and read it. So those are actions that you would do with navigating or authoring code in the IDE. In the CLI, the dominant interface is give me the list of all the Type errors at this moment. So, you would run Pyrefly check and it would read the code and just give you a list of Type errors that you could then, look at and decide which one you want to fix first.
Gregory Kapfhammer 00:31:33 Okay, I see what you’re getting at now just briefly to make sure our listeners are clear. So, this means that you can use it in VS code or Neovim or Zed and then you can also run it in your terminal window or in an agent harness. I think that you can just do something like PIP install Pyrefly or UVX Pyrefly check, am I understanding that the right way?
Danny Yang 00:31:55 Yes, that’s how you would run it on the command line. In VS code you would go to I guess the VS code extension marketplace and just download the Pyrefly extension which automatically launches a Pyrefly as a language server when you open a Python file and for the unofficial VS code forks, you would go to the open VSX marketplace which is similar.
Gregory Kapfhammer 00:32:16 Okay. Now many of our listeners may already be using Mypy or PyRIT, like they may have PyRIT running in their IDE and maybe they’re running Mypy on the command line. So, can you give them some advice if they want to migrate from Mypy or PyRIT to start using Pyrefly, what should they do?
Danny Yang 00:32:35 So Pyrefly actually provides some migration utilities that help when you’re trying to switch Type checkers. So, I guess at its core it just looks at any existing Mypy or PyRIT configuration file for your project and it tries to generate a Pyrefly configuration file that has roughly the same settings. So, the error codes are not like one-to-one, but we try our best to like provide mappings between Mypy and PyRIT’s error codes and ours like different levels of inference like Pyrefly has a bit more inference than PyRIT has for example. So, in our migration from PyRIT we actually turn off some of that inference to make it more compatible and then if you want to sort of increase the strictness later on you can. And another aspect of migration is because these Type checkers have sort of different behaviors for the non-standardized parts of the Type system.
Danny Yang 00:33:28 Sometimes it’s going to be rare when you’re switching from one Type checker to another and you get a completely clean check for your first time. So, another utility that we provide is called Pyrefly Suppress, which suppresses all of the existing errors in your code base and that makes the initial migration process easier. And then you would just clean up the suppression comments later on. Or if you didn’t want the suppression comments in your code base, you could set it aside in a baseline file which is what we provide. So, it’s just a text file that on the side that lists all of the Type errors that Pyrefly currently emits and all of those Pyrefly can read that and suppress them without needing to insert a bunch of comments one by one.
Gregory Kapfhammer 00:34:06 Okay, thanks for sharing that about the suppress approach. I wasn’t aware of it, but I can definitely see how it would be useful. Now I know many Python programmers actually put lots of configuration for their project inside of the PI project Tomo file. Can you configure your Pyrefly using PI project Tomo? Yes. Okay, that’s helpful. Now a moment ago and also quite a bit earlier in the show we talked about the idea of inference, and I know in addition to Pyrefly check and Pyrefly Suppress there’s also something called Pyrefly infer. Can you develop that a little bit further and then say in a practical way, how does Pyrefly infer help me as a Python programmer?
Sam Goldman 00:34:45 So Pyrefly Infer is a tool that fills in a gap that Pyrefly check has by design. So, part of the design of Pyrefly is that the inputs to functions are not inferred. So, if you have a function which takes some number of parameters and those parameters have no Type annotation on them, Pyrefly treats them like the Anytype that we discussed earlier. So, Any use is not checked for errors, and it is a really important part of Pyrefly design because inferring the Type of a parameter is quite difficult. It requires looking everywhere that that function is called, which could be anywhere in the program and for libraries it might not even be in your code repository at all. It could be some dependent library in another repo. So, we make the choice following existing Type checkers to not infer those Types. What Pyrefly Infer does is a slower kind of one time or kind of occasionally run analysis that looks at all the uses of functions, both parameters both within a function and from callers and says you probably want to have this annotation. So, it’s a way to bootstrap typing for an un Typed project where you have functions with un Typed parameters. Pyrefly infer will suggest what those probably should be.
Gregory Kapfhammer 00:36:13 Now I just wanted to connect this to something we talked about before we said there’s static analysis and dynamic analysis. Is Pyrefly infer static or dynamic analysis?
Sam Goldman 00:36:23 Pyrefly Infer is totally static. There are other tools that you can use. I’m not as familiar. I believe one is called MonkeyType where you can run your program and it will do at runtime tracing of the values that come in through functions and you can then use that.
Gregory Kapfhammer 00:36:42 Okay, yeah, I remember Python’s Monkey typing tool and I’ve actually used it by running Mypy test suite and then running MonkeyType infer through a dynamic analysis what it thinks my Types are. But if I’m catching you correctly, Pyrefly infer is a completely static process.
Sam Goldman 00:36:59 Yeah, that’s right.
Gregory Kapfhammer 00:37:00 Okay. Now I wanted to quickly double click on issues that are related to performance because you’ve mentioned this idea of laziness and then also Danny you talked about how when the LSP is running it’s like running in the background and doing checks for me so that when I want to infer something down the road it can help me out. So, I know that your documentation says that it’s like a lightning-fast approach for auto complete or that it has instant feedback so that it can catch errors. So, what I’d like to unpack is the secret sauce associated with making it really fast besides the laziness that we’ve talked about, can you two help us out? What is it that makes Pyrefly so fast?
Sam Goldman 00:37:41 I think, one area where we spent a lot of time is parallelism. So Mypy is written in Python and because of Python’s global interpreter lock is single threaded and PyRIT written in TypeScript. So, running on a JavaScript engine also a single threaded kind of environment by default, Rust allows us to write very parallel analysis so we can use all of the CPU cores on your machine to do analysis, and this is how we achieve this. Staggering lines per second metric. We in the indexing phase that Danny mentioned are able to chunk up the work and do it in parallel across many cores.
Gregory Kapfhammer 00:38:28 Okay, that makes a lot of sense. So parallel processing helps you to be much faster. Do you have something in your own development workflow that helps you to catch performance regressions inside of Pyrefly and if so, how do you handle that process?
Danny Yang 00:38:43 We have some CI jobs that measure the performance along several different metrics. So, end to end like Type checking time on a project is one thing, but there’s also in the language server for example, when you first open a file, how long does it take to index? Also when you make an edit, how fast is the incremental edit time? So, if you make an edit in one file and you have another file that depends on it, how quickly do the errors in your second file update? So, how long does it take to propagate across the whole project and we measure the performance for various code bases in CI and that’s enough to stop I think really catastrophic progressions. But it does require, like right now it requires some vigilance and profiling and monitoring and running benchmarks before each release to make sure we didn’t break something horrendously.
Gregory Kapfhammer 00:39:32 Okay, I see what you’re getting at. So, we talked about laziness and I can see how laziness would help in terms of performance and then we’ve also now talked about parallelism. Is there anything else that either of you would like to say when it comes to what makes Pyrefly fast?
Sam Goldman 00:39:46 Danny touched on this and it’s a great way to round out the list incrementality. So, say that we’ve started an analysis and we’ve given you the first round of Type errors for your project and then you make a change. We don’t want to redo all of the work for everything every time you Type a single character in your IDE. So, the other I think major aspect of the design of Pyrefly is incrementally updating the analysis when the code changes.
Gregory Kapfhammer 00:40:17 Okay, so now that we know a little bit about incrementality, is the idea that it’s like progressively increasing the scope of the analysis that Pyrefly is going to study? Is that what incrementality does?
Sam Goldman 00:40:29 So what I mean by incrementality, the way that it works in practice is that as we do the analysis and we talked a little bit about chasing dependencies, right? So, I referenced the name that comes from an import that comes from another file as we resolve those dependencies, we record that in a dependency graph, and the dependency graph tracks the dependencies and then also the reverse dependencies. So, if I have a file, I know all the files that depend on me. So, when I change what Pyrefly does is, it looks at my reverse dependencies and says, okay, now you’re invalidated too and you also need to be rechecked.
Gregory Kapfhammer 00:41:10 Okay, I get it. Now I noticed that both of you are active in the repository for Pyrefly on GitHub and so I’d like to turn our conversation briefly to a discussion about the governance of Pyrefly and how you at Meta and others at Meta are helping to build it and release it as open source but then also apply it directly inside of Meta. So, I’m wondering, can you tell our listeners a little bit about how you go about managing Pyrefly on GitHub both internally and externally?
Danny Yang 00:41:41 Yeah, so this is one area where Pyrefly’s development has differed a lot from Pyre or Pyre was more like, it was built primarily to be a tool at Meta and our main users were people at Meta and the code was shared on GitHub but we weren’t necessarily taking a lot of pull requests or responding to issues like quickly or making public releases quickly. Pyrefly has a completely different model. So, we’re making weekly releases with detailed release notes for people outside the company to consume. We get dozens and dozens of pull requests every week and we try to review them in a timely manner, and we have very active activity on the issue tracker, and we try pretty hard to solve issues that were raised by early adopters and people outside the company as well. So, like no longer are people at Meta, the primary user base or the majority of users like Pyrefly probably have over a million, probably more active users in the IDE every day through various editors that bundle Pyrefly like Antigravity, Positron, things like that. But also, you can see PyPi downloads, a lot of people use Pyrefly in their CI as well. So, we’re well aware that Pyrefly is not mainly for developers at Meta, it’s designed to work well with the broader Python ecosystem outside the company.
Gregory Kapfhammer 00:43:02 Thanks, that was helpful. Now I know that the Python typing community has something that’s called the Conformance test suite. So, what I’m wondering is how do you decide what new feature to add to Pyrefly or what bug to fix and then how do you track how well Pyrefly does when it comes to this conformance test suite? Could you share a little bit more Sam about this topic?
Sam Goldman 00:43:24 Yeah, so first let me explain what the conformance test suite is. So, we talked about how Type annotations in Python are actually part of the Python language specification and this is a really important point and it’s what make one thing that makes Python Type checking really different from say TypeScript in JavaScript. TypeScript is an extension of JavaScript, the JavaScript spec, it does not include Type invitations at all, but in Python it’s a part of the language and there is a council, the Python Typing Council, which is part of the overall python language governance and their responsibility is to specify what these annotations mean. So, part of their mandate is to maintain this typing specification and the conformance test suite, which is an automated like a CI kind for do Type checkers implement the specification correctly. So, we have tried very hard and done a lot of work to pass the conformance test suite.
Sam Goldman 00:44:31 I believe we just recently passed a 90% of tests passing, which is a really a big accomplishment that we’re quite proud of. As it stands today, the conformance test suite covers really a small fraction of what Type checkers need to do to work in practice on real world code. So when we decide what we’re going to build next, the conformist test suite is of course a factor, but the much more important factor is hey let’s try this on that corpus of real world code and see what kind of errors we find or don’t find in how do we make Pyrefly work correctly.
Gregory Kapfhammer 00:45:12 Okay, I get it. So if I’m understanding this the right way, the higher score that you get on the conformance test suite, the better job that Pyrefly or other Type checkers are doing when it comes to fulfilling the PEP and the specification for typing in Python, is that the right way for our listeners to think about this?
Sam Goldman 00:45:32 Yes, although I mean like I said, the conformance test suite doesn’t cover a lot of important things, so it doesn’t cover anything about Type inference. So, if you write there’s a very simple program x = 1, what does that mean? The specification does not at this moment have anything to say about that.
Gregory Kapfhammer 00:45:52 Okay, I get it. Thanks for course-correcting there. So it’s good if you pass the conformance test suite or have a higher score for the conformance test suite, but that still may not really tell a developer how good of a job Pyrefly or TY or other tools are actually going to do on their own code base and so therefore they’re going to have to try it out and learn from their own experiences.
Sam Goldman 00:46:14 Yeah, I mean I think that really the test is to try it out. It’s not hard to try. So, definitely give it a shot but that’s the best way.
Gregory Kapfhammer 00:46:22 Now in a moment we’re going to take one big step back and to help us to do that, I wanted to take one moment very quickly to look at this from the big picture. So, some of our listeners are already aware of using a tool like PI test to run a test suite and maybe they’ve used other Types of tools like linting tools. So, if you take a big step back, what would you say Pyrefly fits into when it compares to linting and testing and how should our listeners think about using Type checkers and LSPs and test suites and linters in their overall big picture Python development process?
Danny Yang 00:46:59 So I think Pyrefly and Type checkers in general fit in together with both runtime tests and linters. I feel like there’s like a perception that like linters give like non-critical warnings that are like best practices and suggestions, whereas I think Type checkers mostly flag things that could lead to runtime errors. And of course, compared to runtime testing, I think it’s useful to have both Type checking and tests. The main benefit of Type checking in addition to tests is that you kind of, you almost get a 100% coverage for free because the Type checker reads all your code. You don’t have to write explicit test cases that cover every single branch and in addition to the command line Type checking, the way language servers fit into this is just if you want like a rich IDE experience. So it’s like to let you like understand the code better navigate your code faster, the language server helps and like the reason why Pyrefly does both is that the information needed to compute the all the Type errors for a project is kind of like a subset of what the language servers does, like the language server can also in the ID gives you all the errors for the project.
Danny Yang 00:48:09 So if you turn that make it a command line, then you have a command line Type checker. So, if you implement it as a language server first you get both and the language server can help both humans and AI now because you can have this MCP server, then your AI agent can know that oh Pyrefly provides these services. Like it can provide for example give me the Type at this position, the AI can query Pyrefly for that information and it’s more reliable than the AI having to do a bunch of repping and reading a bunch of files to try to piece together the context to get the Type of something.
Gregory Kapfhammer 00:48:45 Thank you Danny. That was actually where I was going to go for my final main question for the show. So, you mentioned the idea of an AI agent almost being like in the driver’s seat of Pyrefly and I wanted to dwell here kind of in a bigger picture, the future of Pyrefly perspective. What does it look like if Pyrefly is now a tool used by agents as much as it is by an IDE directly or by a human using the IDE? Do either of you have thoughts that you’d like to share on that topic as we draw our episode to a conclusion?
Sam Goldman 00:49:19 I think this is a really interesting question and it’s one that we are in the process of figuring out for ourselves. So, one thing that we’re looking at right now is trying to build an experimental framework to evaluate does Pyrefly help an agent succeed at a given task? So, this is an area of active research for us. My colleague Gia Chen has spearheaded a lot of this work on the team, but it’s super interesting and it’s not exactly clear, right? I mean there’s a big hypothesis that we need to prove because the agents, if you’ve used them, they’re pretty good at figuring out what the code is doing without much help. So maybe we can help the agent be more efficient, use fewer tokens, maybe there’s, not that much use for Type checking at all in an agent tick world. I think the future is not yet written.
Gregory Kapfhammer 00:50:15 Okay. So, I’m going to look forward to both of you helping to write that future. In our episode today. We’ve covered a lot about Type checking and Python programming and if listeners are interested in checking out some other software engineering radio episodes, we’ll link them to those in the show notes like Episode 589, which was on property based testing in Python and other episodes that we’ve done that are related to packaging management or FastAPI or other tooling in Rust like Episode 622 and 624. With that, I know we’ve covered a lot of ground, but Sam and Danny, is there anything that we’ve left out that you wanted to share with our listeners about Pyrefly?
Danny Yang 00:50:54 I think we covered quite a lot about Pyrefly’s capabilities. So, I guess my last thing would be like a call to action of sorts like please give Pyrefly a try. We are still in beta, but we’ll have our general release soon, so please give it a try in your projects and report any bugs that you find. We will get back to you as quickly as we can. If you have wanted to engage with Pyrefly maintainers directly, we have a Discord and we hold biweekly office hours where you can talk to us directly if you have questions.
Gregory Kapfhammer 00:51:25 Hey, that’s super cool and in a moment Sam, I’m going to turn to you, but since Danny you mentioned this call to action of trying it out, it also made me think about how Pyrefly has something that’s called the Pyrefly playground, which runs directly in our browser. So Sam, before I turn it to you, Danny, can you tell our listeners what’s this playground is about and how could that fit into the call to action that you shared?
Danny Yang 00:51:47 Pyrefly’s Playground is a, it’s a website on I think Pyrefly.org/playground or sandbox. I don’t remember the exact link, but it runs Pyrefly compiled to web assembly in your browser, and you can write small Python programs and you clarify will check them in your browser directly and give you feedback. You can try things like hovering over things like it’s hooked up to the language server just running in your browser and you can even run the code and using like a browser Python runtime, I think Pyodide. It gave you a little like mini browser environment that lets you test out Pyrefly without necessarily needing to download it. But downloading and running it is very quickly or very fast. So, it’s the sandbox is useful for playing around, but using it in a real project is, it’s not the same thing.
Gregory Kapfhammer 00:52:37 Okay, thanks for that clarification. And you’re right, it is Pyrefly.org/sandbox and if listeners want to install the tool, they can install it with PIP or UV or run it directly with UVX and then maybe quickly try it out inside of the sandbox. At this point, Sam, I wanted to turn it over to you. Are there other things that you wanted to share with our listeners?
Sam Goldman 00:52:57 Yeah, I think I’d like to mirror what Danny said that if you haven’t tried Pyrefly yet, give it a spin, find us on GitHub or on Discord. But I’ll also do a shout out specifically to Python Library maintainers. If you maintain a library written in Python that does not provide Types, I think you especially should consider it. The future of Python I hope will be Typed and users will expect Types from your library. So, if you haven’t made the switch yet, check it out and whichever Type checker you use.
Gregory Kapfhammer 00:53:35 Hey, those were great calls to action for both of you. I hope many of our listeners will follow up and learn more about Pyrefly by checking Pyrefly.org and its homepage, including lots of details about its performance and how to install it and how you architect it and designed it. Sam and Danny, it has been super fun for us and our listeners to learn all about Pyrefly, thank you for joining Software Engineering Radio. Thank
Sam Goldman 00:53:59 Thank you Gregory, it’s a blast.
Danny Yang 00:54:00 Thanks for having us.
Gregory Kapfhammer 00:54:02 Hey, thanks for being on the episode. This is Gregory Kapfhammer signing off for Software Engineering Radio.
[End of Audio]
