Now we've got Shagan, who's going to tell us about tie.
I think if people are in the Python community, you've probably heard of this really cool
typing here, type checker, yeah, but I'll let you explain it all, so take it away, so thank
you.
So, welcome, hello everyone, my name is Shagan, and I want to talk about tie tricking
Python in Rust.
This is about a project called TY, it is a tie tricker for Python from Astral, the
same people behind Roppen UV, both are very popular projects in Python ecosystem, it
is available as a CLI tool, it connects to your editor, we are language server protocols,
so you can use it in VS Code and VIM, and it's also available on Play.ty.dev, where you can
run it on the browser, it focuses on a speed, and reached out to no sticks, as you can see
there, it's pretty fast, that's for running TY on the CLI for touching your whole project,
but TY is also pretty fast when you run it on the editor, because when you run it on the
editor, it actually needs to constantly type trick what you are typing, and what
the project has to give you accurate autocompletion and diagnostics, and for that one,
TY made a couple of decisions that really helped to achieve that speed, which I'm going to
be talking about in the next slide, so this is going to be more technical talk, and yeah,
I'm a contributor to TY, and I'm going to be talking about some of the interesting aspects
of the internals, so before looking into it, I'm just going to give you a very small example
of what a type tricker does for you, so this is a Python piece of code that I have,
I have a function, it should be taking integers and input, and then I'm calling it with a string,
obviously if you run this, you would get an error in run time with a type tricker, it would
tell you that hey, you're passing a string that's all here instead of an integer, so it's
going to obviously error on the run time, but it's also inspired by the rust compiler, which
you might be familiar with, that it gives you more information about what other things can
be helpful to fix this type or for you, so here, for example, we do show the function signature
and the parameter that is declared, so you can get some help from the type tricker here
to fix the problem, now let's look into how a talk tricker would work in a very simple way,
just an overview, you might have a talk tricker that has more components than this, but
this is the standard things that you would have in a type tricker, so the type tricker consists
of a couple of passes that run over the source code and each one produce some data structures
that the next pass can use to do more stuff on the source code, and then finally, we have
a lot of information and then we can do the type inference, because we know about all the
variables, all the functions and everything, and we can do the type tricker, so what
does the parser does? Well, it takes your source code as ticks, and it will transform
it into a set of strokes that we have, so it's a big statement, you know, and with a lot
of a strokes in it, and because every Python program is just a set of statements, you
can convert any line of code that you have into a statement, or a couple of lines
going to one statement, and then in the later parts of the program, you can work with
those statements since that, so we can do matches on them, and cover all the cases, and
you can see here, I have a, I'm defining X, with annotation int, and assigning one to it,
and I capture all that information into this stroke, and here the value is an expression,
annotation is an expression, the target is just a name here, then we have the semantic
analyzer, which goes over the ASD that parser produce for us, goes over all of the
structures, and then we would try to drive more information from that, things like what are
the definitions in my program, functions, classes, scopes, all these things, what are the
variables defined, so I have all of this information, and then later in the type inference,
when you're assigning another variable to another variable, then the target tricker can
ask the semantic index, where is this variable defined, and I have all these definitions
index and the semantic index, so I can look it up and do the inference, then finally we
have the type inference, and it just goes over all the statements and expressions I have
in the program, and infer a type for them, so here I had int, it was an annotation, it's
an expression, so we infer the type of it as class literal int is referring to the int
inside Python, then I have one and the same type because one was assigned to x, now let's
look at the semantic index more close, with some examples of stuff that it records for
us, here I have a class, and it function inside of it, so a method, and then these two
create two scopes, I have classes scope, and then I have the function scope, we need to record
these scopes so later, for example, looking up variables in the method food, then you can
know what are the pants scopes, so you can walk up the scopes and see what are all the variables
that are visible to us there, and we do this by recording every scope into a vector, we just
put scopes in the vector, every scopes gets an ID, so scopes can refer to each other by
an ID, that's where the file scope ID comes in, and scopes inside themselves have their parent
attribute, where it just points to another scope with that ID, this is a pattern that you
would see in TY a lot with having IDs that refer to stop, so you can have the IDs inside
different structs to point to each other, and then you would look up the vector with that
ID to get the actual information, and our example of stuff we record are definitions, so here
I have a function is defined, a parameter is defined for a function, and all of these are
recorded in the hash map with the node key, with all the definitions, I think I have multiple
definitions in Python, you can just overwrite the stuff, so you need to have all the definitions
for that, and we also record the constraints, so constraints are two kinds, you have a narrowing
constraint, like the if statement I have over there, and saying X is either type of integer
or non, and then I'm checking if X is not non, so then this would narrow the type of X in
that if branch for me, and it does that by recording all the constraints within the scopes,
so I can know what is the type of X inside that if statement, and then it would be integer,
then I have reachability constraints, and these would be things like you have, and if statement
that would say if Python version is bigger than this tree point 11, for example, they find
this variable, and then the type to record that reachability constraints, and then if you type
a project with a smaller Python version, then it would note that that part of code is not
reachable, and the variable should not be defined, and you get an error if you use it, then let's
look at the type inference with more examples, so here I have a, again, a small piece of code,
and the type inference is set of calls that recursively call each other until all the expressions
are inferred, so in this example if you focus on the second result, a plus 3, we would call
infer expression, that is just a big if statement, and then it would call the appropriate function
that should be inferred binary expression here, because that's a binary expression, and then that
again needs to call infer expressions, so it recursively calling itself with a and 3 to get the
type for those things, and then finally based on the type of those things, it knows that what happens
when you add those things up, and gives us the final type, and this is the big if statement
I talked about, so it's a match statement on the expression enum, and then we have cases for
all the different expressions that you can have for a in the Python program, here just one is a
numberally troll, so it matches the case, and we infer the type for it, for the result a plus 3,
it's a bit more complicated, I need to call infer expression again on a and then on 3, and then it
would resolve or a was defined in the previous line, and it was assigned one, so the type of it would
be integral 1, and then finally with the two things I have, again I have another big match case where
has the all the result for what happens when you apply add on two integerly trolls, and it has
different cases for all the other types that you would have, so this was about the usual
type checking stuff, one of the things that he why does that makes it fast in the editors is
incremental type checking, this is about only type checking what you need, and when you need it,
so imagine this program I have a main dot pie and a lip dot pie, and main dot pie is only
importing a part of lip dot pie, and it's not depending on all of it, so when I type check
main dot pie my editor, but I'm open main dot pie my editor, TY only infers the type of lip
dot pie that I actually need, and in this case it would be a square function, and it would just
a skip over the square with function, and also when you like as you work with more files and more
files it will type check those, and it also catches this stuff for all of you, so if I don't change
the lip dot pie at all, because it's a library, and I just focus on main, it will reuse the
cash from the type inference, so you never need to do the compute again and again, and the way
does that is really a library called salsa, it is, if you're familiar with rostanalyzer, it's also
uses this, and salsa provides us a couple of components that we can build our compilers, type
triggers in this way, with the incremental compute model, and here's an example of one of the things
that salsa provides, so this is what we call a salsa query, because of that macro at the beginning,
and this macro is telling salsa to track dysfunction, and let's see what it does it track, so
I passed the function a database, the database is used to track things like what dysfunction does,
and the memoization of the function, it is a central database that salsa just stores everything
inside of it, so every query gets that database argument, and then I'm passing also a definition
to it, so I want to infer the top square definition, and inside of the function, I am calling
two other queries, again parse module and semantic index, and salsa records that this query depends
on these two other queries, so if the results of this other queries change, it means that this query
is also invalidated, so I need to recompute this, otherwise if the input is the same, this query
is the same, I can reuse the compute, so it would have a graph that looks like this kind of,
so input and what it calls, and then as long as those things are staying the same,
then I don't need to recompute the value and I can just use the cache.
This is the database that you saw in the previous file, it's just a salsa DV macro,
and salsa does all the stuff for us. salsa also provides a couple of other macros for our
structs, so we have the salsa input macro, this one tells salsa that this is an input to our
program, and you can think of, for example, the source code as an input to our program,
and we can mutate the input because that's what the user changes. The other things that we have
are intermediate values that we are computing, we are query functions, and the input is the thing
that users mutate, and we have the intern structs, interning is a technique to, if you have
something repeatedly happening in your program, you can just store one of that ones, that thing
once, and then refer to that thing. For example, if you have a function name, and then if you
encounter that function name over and over again, once it's defined, once it's called, and so on,
you can store it once, and then get back an ID from salsa, and we did ID, you can refer to it.
So you just allocate the memory once to the Cisco once, and then just have the ID, and then if you
intern something over and over again, salsa just gives you back the same ID. Also here, if you
intern a function type, if you have a lot of functions with the same type, it's just going to be
one object in our database, and the risks are going to be using that, and then we have the queries
that we just looked at, so it takes a database, something that implements the database create
with the DB lifetime. So as a result of this, all of our structs would be copy, we can pass
a stuff around, you don't have the problems that people usually face in draft projects,
you can move stuff around, you don't need to clone, you don't worry about it, it's just an ID.
Everything, all the field values, all the stuff are stored in the salsa database, you need to
look them up in the database when you actually use them, but if you just want to pass in stuff,
it's an ID, and most of our structs will get the DB lifetime. This will help us to, for
example, if you want to pass references around or return references, everything has this
DB lifetime, so you also don't need to really worry about what should be the lifetime,
because it's all DB lifetime, and then it also prevents some things like, for example,
mutating something in the middle of when you are using a cash value and stops you from mutating
the input, for example, at that point. In order to take advantage of these functionalities that
also provide, we need to think about the problem a bit differently, so if I just infer all the
Python program all at once or all at once, if something in the file changes, then I need to
redo that again, so the cashing is not as good as it can be. One technique here that PY does is
you split the inference into multiple regions, so to scopes and definitions, and then
if the file changes, some of that inference region can survive, because if you touch something that
is not affecting other scopes, then other scopes can still be in the cash and can reuse the cash in.
So, same with the inference, also we have like a smaller query, so for example, here we can
depend on the place table, instead of depending on the whole semantic index, if something is only
using that, or we only infer the definition types instead of inferring the whole program
or all at once with one giant query. Well, it's also does a lot of nice things, but it's not
done yet, here's an other big problem that you would face in type taking, and that is cycles.
Cycles happen usually when you have a thing that refers to itself, and although it might seem,
I don't know, confusing, but this can actually run as a Python program, because someone can
make an object of D, and then assign x to it outside of this class, and then create another object,
and just call D copy with the order of object that they assign the x to. And this can work,
but from the perspective of a type tricker, if we could, or something to the shoe, it would be
exactly like, I'm trying to find out what is the type of self.x. To do that, I need to know
what is the type of order of the x. The type of order is D, so I need to go to the class D,
and find the attribute x, so I know what is the type of self.x, and that was exactly what I was
doing, and those infer expression calls keep calling each other repeatedly until you crash,
and you never actually quit, so this kind of loop happens, and solso has a solution for this,
it is called fixed point iterations. With fixed point iterations, you would have, so let's think
about a problem again, we have one function calling another function, and then finally calling itself
again. If we have some kind of if statement at a function, so it knows when it calls itself again,
then it can stop that infinite loop from happening, but when we need to know what should we
return at that point, we are calling it or so again, and you can't set the cycle, if in,
and cycle initial attributes in the tract, solso tract macro, and it would exactly do those things
for you. So, cycle initial would tell solso what type should I use when I'm calling myself again,
and I have no way out, and it would return that type, so you can have all the functions that
recursively call each other, do their compute, and then finally resolve, and then you get back to the
first function that called itself, and then you would have two things, I assume the value, and I also
computed a value, or these two things are same, if they are the same, I assume something and I ended up
with the same thing, so if I do that again, it will also be the same, but sometimes you might
assume type never, which is the bottom type in Python, it is representing as distinct never happens,
and if I assume something like type never, and then I do my real computation, and then I end up with type
unknown, well, this is not valid, so I can do this cycle again, I would iterate again, I now have
type unknown, and I can say, okay, imagine that assume that I have type unknown, and do the compute
all over again, and if I end it up with the unknown type again, it means that if I just do that
over and over, it's just going to be the same result, so it's at least a stable, it converged
the cycle, otherwise if it never converges, you might have something that just toggles
between two values or things like that, then the cycle has two ways, you can either iterate until
sometime that you would panic, or you can also fall back into an unknown value, and just say,
I couldn't solve the value for this, and yeah, this is really helpful, because with all the
recursive calls that you have, manually instrumenting your code with the big hassle, but it's also
it does this for you, with this solution. Then we have the testing framework in TY, it is built
in house, it is a very nice thing, so all the tests only a huge chunk of the test suit is written
in markdown, and we have big markdown files, we Python code is typically outside of them, and then
we explain, for example, this test case is testing this behavior, and then inside the Python code,
there is a magic function like that reveal type, and you would write your own Python program,
and you can use the reveal type to assert that the type of that thing is what you want, so in the
comment, so it's a valid Python program, and it's also a test case, and here I have, for example,
revealed int, it is not an int, it is literal one, TY tries to be very specific with the types,
and when it knows about it, so it knows that you assign one, it is definitely this for one,
and when you run core but test, you would get a pointer to that annotations MD file, so that's
your test case, and then the exact line that the problem happened, and then it would say,
it reveals literal one, not integer, and whenever you submit PRCTY, there is a huge test suit
that runs, you have this MD test, the same markdown test, I just showed you running,
then there is a conformant test in Python, that's the thing that Python type in
console works on, and they have sets of rules of what type figure should show for different
annotations, and it also runs on a lot of open source projects to know, what is the impact of your
change on these projects, how many more diagnostics are you showing, what are your memory and timing
metrics changing, and this is an example of one of those reports that you have, and then you can
go to the projects to see, for example, what were the new diagnostics that you added, and she's
very helpful for her, if you don't really know what's the bright answer for some decision,
you can just try it out and see what happens on the open source projects, because people
write Python in a lovely different ways, that's it, here's my blog, there's more Tribal Posts