Demystify Python Types for PEP 729
This is a modal window.
The media could not be loaded, either because the server or network failed or because the format is not supported.
Formal Metadata
| Title |
| |
| Title of Series | ||
| Number of Parts | 131 | |
| Author | ||
| Contributors | ||
| License | CC Attribution - NonCommercial - ShareAlike 3.0 Unported: You are free to use, adapt and copy, distribute and transmit the work or content in adapted or unchanged form for any legal and non-commercial purpose as long as the work is attributed to the author in the manner specified by the author or licensor and the work or content is shared also in adapted form only under the conditions of this | |
| Identifiers | 10.5446/69423 (DOI) | |
| Publisher | ||
| Release Date | ||
| Language |
Content Metadata
| Subject Area | ||
| Genre | ||
| Abstract |
|
EuroPython 2024111 / 131
1
10
12
13
16
19
22
33
48
51
54
56
70
71
84
92
93
95
99
107
111
117
123
00:00
Pauli exclusion principleValue-added networkProcess (computing)Pauli exclusion principleProcess (computing)Right angleComputer animationLecture/Conference
00:38
Pauli exclusion principleSystem programmingMetreTrigonometric functionsSystem of linear equationsContent (media)Parameter (computer programming)Canonical ensembleStatement (computer science)WebsiteProcess (computing)Image resolutionTrailProcess (computing)Pauli exclusion principleLatent heatContent (media)CuboidPoint (geometry)Right angleVideo game consoleThread (computing)ImplementationMereologySoftware developerSoftware maintenanceP (complexity)Arithmetic mean2 (number)System programmingGraphics tabletComputer animation
03:51
Process (computing)ReliefTable (information)Content (media)TheoryType theoryFormal languageLetterpress printingBoolean algebraTable (information)1 (number)Computer programmingMultiplication signCodeVariable (mathematics)MereologyPauli exclusion principleContent (media)Latent heatOperator (mathematics)Programming languageBoolean algebraType theoryLevel (video gaming)BitCore dumpPattern languageTheoryProcess (computing)Arithmetic meanComputer animation
06:12
TheoryType theorySystem programmingPresentation of a groupLatent heatTheoryType theorySet theoryCategory of beingLatent heatContent (media)Presentation of a groupSystem programmingLogicProof theoryBridging (networking)Arithmetic meanStatisticsComputer animation
06:50
SineElement (mathematics)Regulärer Ausdruck <Textverarbeitung>WeightFitness functionEquivalence relationMathematicianType theoryGaussian eliminationElement (mathematics)MathematicianObject (grammar)ExpressionMathematicsCASE <Informatik>Proof theoryRule of inferenceCompilation albumWeightFitness functionEquivalence relationRight angleWater vaporArithmetic meanBackupCodeVariable (mathematics)Condition numberTheory of relativityEqualiser (mathematics)Latent heatFormal languageTheoryPropositional formulaComputer programmingCounterexample2 (number)Boolean algebraComputer scienceInsertion lossComputer animationLecture/Conference
12:43
Gaussian eliminationConditional probabilityRule of inferenceMathematicianTheoryClique-widthoutputCondition numberPositional notationFunctional (mathematics)Network topologyType theorySocial classBootingWordMathematicsMathematicianTheory of relativityObject (grammar)CASE <Informatik>Electronic mailing listCodeReal numberPauli exclusion principleRun time (program lifecycle phase)TheoryEqualiser (mathematics)Interpreter (computing)Rule of inferenceInstance (computer science)Operator (mathematics)Programming languageMereologyDivisorRectangleEmailGaussian eliminationAreaBinary multiplierBoolean algebraPointer (computer programming)Slide ruleQuicksortBackupIntegerBitMultiplication signString (computer science)Video gameInformationComputer animation
18:36
Clique-widthDemo (music)SineDesign of experimentsSystem programmingSystem programmingType theoryTheoryCodeMultiplication signFocus (optics)Pauli exclusion principleMultilaterationComputer animation
19:43
Ordinary differential equationElement (mathematics)ConsistencySet (mathematics)Function (mathematics)TypsystemoutputPauli exclusion principleCodeRun time (program lifecycle phase)Parameter (computer programming)TheorySystem programmingFluid staticsFunctional (mathematics)Rule of inferenceNumberElement (mathematics)Parameter (computer programming)outputConsistencyIntegerFunction (mathematics)Variable (mathematics)Computer programmingDefault (computer science)Error messageCASE <Informatik>Different (Kate Ryan album)TypprüfungMultiplication signElectronic mailing listMereologyString (computer science)Interpreter (computing)CodeRun time (program lifecycle phase)Real numberInferencePositional notationType theoryPauli exclusion principleRight angle2 (number)Heegaard splittingNumber theoryTheoryComputer animation
25:28
System programmingSingular value decompositionTheoryDesign of experimentsTheorySystem programmingType theoryPattern languageMultilaterationComputer animation
26:06
Pauli exclusion principleRoute of administrationSystem programmingMultitier architectureGoogolFluid staticsPairwise comparisonDrop (liquid)Single sign-onFormal languageCommunications protocolIntegrated development environmentDisintegrationCodeScale (map)Interpreter (computing)TypinferenzMeta elementExistenceoutputTypsystemFunction (mathematics)Pauli exclusion principleMereologySystem programmingScaling (geometry)CodeDifferent (Kate Ryan album)GoogolLine (geometry)Functional (mathematics)Meta elementSoftware developerIntegrated development environmentINTEGRALTypinferenzMathematical analysisPerformance appraisalCommunications protocolMultiplication signFormal languageCASE <Informatik>Hecke operatorPower (physics)Point (geometry)MathematicsComputer animation
29:40
Resolvent formalismType theorySystem programmingDifferent (Kate Ryan album)Field (computer science)Computer animation
30:15
System programmingCodeFunctional (mathematics)Variable (mathematics)Run time (program lifecycle phase)Electronic mailing listIntegerTraffic reportingString (computer science)Error messageResultantMathematicsSocial classTypinferenzDifferent (Kate Ryan album)Positional notationCASE <Informatik>InferenceMultilaterationSign (mathematics)PiComputer animation
32:31
System programmingHacker (term)State diagramType theoryOctahedronMathematical analysisRun time (program lifecycle phase)Communications protocolPauli exclusion principleVariable (mathematics)Parameter (computer programming)Function (mathematics)Shape (magazine)CircleScale (map)RadiusDifferent (Kate Ryan album)System programmingState of matterSoftware developerEquivalence relationElectronic mailing listPauli exclusion principleCodeRun time (program lifecycle phase)StatisticsLatent heatMultiplication signImplementationBoolean algebraInformationLine (geometry)Computer configurationPiNetwork topologySocial classWritingCASE <Informatik>Type theoryComputer animation
36:19
System programmingExact sequencePauli exclusion principleSoftware developerCore dumpRule of inferenceDesign of experimentsArc (geometry)RSA (algorithm)CodeWeb pageoutputTypsystemFunction (mathematics)Interior (topology)2 (number)SyntaxbaumParsingNetwork topologyMathematical analysisGeneric programmingMultiplication signDifferent (Kate Ryan album)Latent heatRight angleSoftware developerLevel (video gaming)Function (mathematics)outputInformation2 (number)ImplementationGeneric programmingCodeSystem programmingLibrary (computing)Lipschitz-StetigkeitMessage passingCompilerTypprüfungNetwork topologyTraverse (surveying)Arrow of timeParameter (computer programming)Digital photographySyntaxbaumSource codeComputer animationDiagram
38:55
Executive information systemPairwise comparisonCASE <Informatik>Lecture/Conference
39:37
TypsystemRevision controlRight angleScaling (geometry)System programmingLimit (category theory)Latent heatCodeComputer animationLecture/Conference
40:31
Point (geometry)InformationFunctional (mathematics)BitTypprüfungMultiplication signRun time (program lifecycle phase)Lecture/Conference
41:06
AdditionPoint (geometry)BitMultiplication signFunctional (mathematics)Interpreter (computing)Social classSystem callInstance (computer science)Lecture/Conference
41:51
Message passingPauli exclusion principleError messageStandard errorVideo game consoleMultiplication signProcess (computing)Software developerLecture/Conference
43:18
Multiplication signLecture/ConferenceComputer animation
Transcript: English(auto-generated)
00:04
All right, so hello, everyone. And my talk is Demystify Python Types for PEP 729. Before I start my talk, I want to just have a poll here. So how many of you have heard about PEP 729? Please raise your hand. All right, actually, not that many.
00:21
That's probably good, because that's the reason you sit here. PEP stands for Python Enhancement Proposals, and PEP 729 is about a typing governance process. So today, let's take a look at this PEP first, because we demystify Python types for it, right? PEP 729, if you check this thing,
00:44
originally there's a thread discussion, a very short one. People are basically there saying, thanks for consolidate all the things we already discussed somewhere offline. So this basically is the PEP. And this PEP, what it does is simply just a new way to govern Python type system,
01:01
as the name stands for. A part I would like you to take a look into is this PEP was endorsed. It claims it was endorsed by maintainers of all major type checkers. So that's an important thing, and let's look into it.
01:20
So initial member here, you may see some face you'll be familiar with. Of course, Grido here, and other type-related, or three Python developers here. So the motivation of this PEP, you can see four points mentioned in this PEP. First one is, like they say, PEPs
01:42
are the only sophistication. And I mean, what does that mean? It means that, for example, if you developed a PEP, usually you probably don't really think about how this PEP impacts three Python. But for Python type's case, it's also
02:02
involved the external tools. And here we mean type checkers, because there are many type checkers. So that's one motivation. They want a different way to govern type. And second thing is PEP is hard to evolve, which means certain specific implementation.
02:23
In fact, the third point is the PEPs try not to specify the detail for implementation. However, in this particular Python type's case, it could be something like, I will say, this should be specified.
02:41
And that could be the thing that these PEP can likely wonderful motivation for that. And finally, the fourth point is not something I mentioned. They say that steering console is not well placed to solve both problems. And that's basically what they say. And of course, I cannot on behalf of a steering console
03:01
or people talk about this point, but I will just say it may make sense, because of today's content, I will say, once you dive deep into it, you will see how deep the type is and may not be a good place for them to discuss that detail. And if you check some PEP, for example, PEP 695,
03:24
well, it's not important about these PEPs' content. This PEP just has a talk impact on yours this year. The thing is, once you check this PEP, you'll see there's a yellow box there. And that yellow box just tells you, OK, you should go to another type specification process instead
03:42
of here. And this is a kind of historical document. So that basically answers, OK, this is already something ongoing. All right. So we know this PEP 729 thing. And to me, it's just like, OK, I read the motivation. It looks just makes sense, but what does that mean?
04:04
And what type do they mean? And why do we need this new process? That's something I want to dive deep a bit into it. So that's my motivation of this talk. Let me just introduce myself again. I skip that in the beginning.
04:22
This is my first time in Europe, I think, in person. So I gave a talk during COVID remotely before. I am part of the PyCon Taiwan community. We have a conference this year in September 21st and 2nd. And it held not in the main city. Usually you hear about Taiwan is Taipei,
04:41
but it's in Kaohsiung Listan support city. So if you want to visit somewhere in Taiwan, now that the majority of people visit, then this will be a good chance for you to be there. And we also have a podcast called PyCast. It's basically target audience can speak Mandarin. So not sure how many of you here can speak that. But if you are, then this definitely
05:00
will be something I will recommend to check out. So table of contents today. I will talk about this counter-audiencing, but I will talk about the coursing first. So we talk about type theory, engraved typing theory, and type checkers, and list specifications. We go through all the things to demystify pattern types.
05:23
So why do we need to talk about type theory? That's because we want to answer what is type in Python, or maybe whatever programming language is. This code, I think whatever level, probably you learn Python, probably your day one, you already can know this code here.
05:42
You just assign some variable as a true value and a false value to another variable. And you can print that out, you can compare that, and you can do some operation on them. The thing is, we know A is a true variable,
06:00
and A is a Boolean type. This is probably something we may already know in day one's book. But what does a Boolean type actually mean for a programming language? That's something we should know today. So type theory is a presentation of a specific type system. So if you've ever studied other theories,
06:21
like set theory, categories theory, logic and proof theory, and so on, you'll know there's a thing called HOT, H-O-T-T. This theory bridges all those things together. So it doesn't mean a set theory is equivalent to categories theory. To be honest, I also don't really know about all those theories. But I'll just say, like today, the content will be,
06:42
although we talk about type theory, I'll use set a lot here, because that's probably easiest thing to understand type. OK, so look at this expression. X is an element of A. This is X expression. What does this mean?
07:02
In type theory, when you say X is an element of A, by promoting Love, one of the type theories, kind of original theories founder, I would say, there's four way to interpret it. He used four ways to interpret this.
07:20
I would say X is an element of A. And first one is definitely something you already know. X is an element of the set A. So programming language people, you write code. You would probably use this way to understand it. You say true is a Boolean. And so true is a Boolean type. True is an element of a Boolean type.
07:40
And there's other way to interpret this, including things like X is a proof object for proposition A. X is a program satisfying specification A. And X is a solution satisfying problem A. And to be honest, the first one is my favorite one. So later I will use the example for the fourth one to explain this.
08:01
So firstly, when we look at X is an element A, we need to define what is set A first. So the set A, basically, we have two conditions here. The first condition is what is in this set A. And we also need to define what condition makes elements
08:22
equal. So you have two elements in A, three elements in A, whatever. Are they equal or are they not equal? That's the thing to define a set A you need. And here, let's use an example here. For example, let's say we have a problem as loss weight.
08:41
We want to lose weight. And you can definitely find a lot of solution for these problems. For example, you can think about you can swim. You can jogging. You can eat healthier. I think three ways you can lose weight. But the thing is, the outcome of these three ways could be different. Let's say, for example, here, let's say swimming may lose you three kilogram.
09:02
And jogging may lose you five kilogram. And somehow, just to eat healthy also makes you lose five kilogram, let's say, in a certain duration. And so in this case, you may say, OK, so jogging is equivalent to eat healthier. But they are different from swimming. And that's the idea of first, you define this problem.
09:23
And you have some solutions in it. The second thing we need to answer is how to tell set A equal to set B. To answer this, it's pretty simple. Just you can find out an element in set A and also in set B.
09:44
And of course, you can find out the same equivalence relation with x-ply, another x-ply variable. That's also in set A and also in set B. And you can do so for y as well. You can find another element in B and also in A. And another y-ply equivalency relationship in B and A, too.
10:04
With this, you can say set A is equal to set B. This may be like, OK, let's use another example here. Let's say we have another problem in improved fitness. So we want to ask, is loss weight equivalent to improved fitness?
10:21
And that could be right. So if you can find two conditions, first is you can find two solutions to solve both problems. And you can also find the equivalent solution in both problems. Then you can say these two problems are equivalent. However, in this case, it's probably difficult to find out the equivalent problem,
10:41
but it's easy to find a counterexample here. So let's say we already know jogging is same. I mean, these three things we believe can improve fitness can also loss weight. But the thing is, the relationship between them will be different. So you cannot say these two problems are the same problem. That's basically the idea of how we define
11:02
x is an element of set A. Let me drink some water. OK, so further, let's look further into how mathematicians in here in Permanente-Löf,
11:22
how Permanente-Löf define a set. The answer is so-called general rules. So if you study computer science or mathematics in school, academic world, I think they will use this a lot to define all the types. For this particular case, the general rules,
11:41
there are basically four rules. First is formation rule. It's a way to define a problem. And in this case, we can say A is a set. That's formation rule. We define the set. And second introduction rule is we define the elements inside the set, so the solutions for the problem
12:00
we defined. And third one is the most tricky one, I'll say. It's like if you pick a solution, there is a premise you pick a solution, and this solution can solve the problem. And that's the idea of the invention rule. Equality rule is similar, but slightly different. It's like if you pick a specific solution, then that specific solution solves the problem.
12:22
Let's use Boolean as an example to see how a mathematician defines Boolean type. Here's the example here. Formation rule, of course, we can just say there's a Boolean type. We define it. And secondly is elements in Boolean. So Boolean is probably one of the simplest type here. We only have true and false. That's what we know.
12:42
In the mentioned rule, it's something pretty complicated. We have a premise. We have a Boolean type. And we have a condition set. So there's a selector to build a condition set. And then we can say, OK, we have a true condition set and false condition set. If we put true in this selector, we got a true condition set.
13:00
That true condition set is part of the Boolean set. And then equality rule is pretty much the same, but just like if you put true into the selector, this true is in true condition set. So it's in Boolean set. So that's the idea of this definition. And I'm not going to talk further like list and class and whatever complicated type you can find
13:22
in a program language. Basically, this is a simple idea here. Until here, you may just ask, wait, this is too far away from our life. That's true. Python is a wonderful word. But math is something we just don't want to know that far. And so the idea I want to give you here
13:41
is not really how mathematicians define all sorts of things. It's basically a semester's class about type theory. They will teach you all sorts of things, all sorts of types. Maybe in an examination, they will just check your understanding of each type. And you can define the preemies for the elimination rule and so on. But in here, I just want to let you know
14:01
is that all the types you use in a programming language are behind math theory. And some of you may just smartly just say, hey, everything is pi object pointer in Python, right? So which means we have string, we have true, we have whatever new type. They are all Python pi object pointer.
14:21
So everything is just a pi object. The answer is yes, it's true. So everything is pi object in Python with type information, in fact. So pi objects header defines a thing called OB underscore type. So for all the objects under when you run the interpreter,
14:41
they actually check objects OB underscore type to know what's that. And then the interpreter can understand that and determine the operation in runtime. And there are some functions you can use, like a type instance, X subclass, and so on. This tree function defines, I think,
15:02
just somewhere in type that's C or somewhere in the interpreter. And you can use them to check the thing we just talked about, such as we say everything is object. That's true. That's the first thing. You can put everything there, and it's instance object. It will be true. And you can also check the class relations.
15:22
It's pulling an object. That will also be true. And you can definitely just reverse it, say it's object and pulling. Definitely it's not the case. And that's the thing back to the theory we just mentioned. So you cannot just reverse talk in this way. And you can also check the true and the false
15:41
as pulling type. That will also be the case. So in fact, there's kind of a fun fact is there's definitely a PEP called PEP285. It's far away from today, more than 20 years ago, by Guido. So this PEP is definitely about just the booting. So at that time, Python doesn't have booting.
16:02
So Guido thinks like, hey, we need to have a booting. Otherwise, people just often use a defined true variable equals to one, false variable equals to zero, and so on. And in that code, they do so. So this PEP probably by far is the, I don't know if there's other types PEP, but this is one of the PEPs pretty interesting to know.
16:21
And in these PEP, it basically implement the booting type. And if you check the header files, you'll find out this is the definition of booting type. Simply speaking, there's on top of that, we define booting is a type. And later we have a lot of booting functions,
16:42
constructor, destructor, and some functions like you can run in C, that will be faster. So they do that in C instead of, you don't need to do that in Python. And the other important thing is there's a base type. So in booting's case, booting in Python, in fact, is integer. So that's maybe another factor you may not know before.
17:01
Just if you check a C instance booting for integer, that will be true, yeah. Okay, now we finish the, I will say basic type. We need to talk a bit further, because in the real world, Python world today,
17:23
when we talk about type, we actually talk about another thing called annotation. So annotation is based on a thing called gradual typing. Gradual typing here, simply just before gradual typing, Python code is just like the top side, it's un-typed.
17:44
And after gradual typing, you can partially type your code, you can fully type your code. Seeing as you got a notation here, that's exactly the idea of the type of Python here we mean. I don't think this talk is for people who want to know why we need gradual typing, why we want to write a notation for Python.
18:03
That's definitely not something I want to focus today. But still, I mean, I choose this one slide here to explain that. We need gradual typing, and that's because if you look at this code in the top side there's no notation, which means you can put anything there and some of the input you may get some surprise outcome
18:24
such as string, multiply integer, or at least multiply integer, you got some surprising outcome. That's definitely likely not something you expect to calculate to the area of the rectangle. All right, so gradual typing theory is another type theory,
18:41
and it's a pay-as-you-go type system. And probably the idea here is a type may be partially known and unknown at compile time. And the reference here, the first paper is by Jeremy Stig in 2006. This is a paper probably took the fundamental idea
19:01
of the gradual typing. And later, Jeremy Stig writes another book in Python. Actually, the example code is in Python, What is Gradual Typing? And in the same year, I mean, we have the PEP-4A-3. That is the theory of PEP-4A-4 you may heard of about type hints. And one thing I didn't focus on
19:23
when I introduced type theory is type system. So gradual type theory and type theory, they are both certain kind of type system. That's the thing. So we should introduce what is type system here now.
19:45
So type system, I mean, when we talk about system design, usually it's just like some input. We got into a system and then we generate some output. That's the idea. So type system is exactly like that, it's a system. It's a system to check the type consistency. So the input will be a lot of element in sets.
20:02
So that's the X element in A set, Y element in B set, and so on. And this type system there will basically just check, hey, is X element in A set? Is Y element in B set? If everything's yes, then we are good, right? So each element is in the right set. But if there's anything wrong, then this system will just report to you
20:21
that there's something wrong. This element is not in that set. And Python types consistency check before PEP4A3, that's exactly just like this. When you run the CPAS interpreter, it does do the kind of type consistency check that you may not know because usually when you run the interpreter,
20:41
you only care about outcome. Your program can run or cannot run. But in fact, it's under the hood. There is a check about, like, is this element in a certain set? And that's the idea. And after PEP4A3, we have the additional thing called type checker,
21:01
and the input can now be partially typed and fully typed now. And again, CPAS interpreter is still a type system. It can still check the types. And we have type checker additionally also can do the same thing, but it's in static time. So the difference is CPython execute your code, and type checker doesn't. Type checker just scan your code,
21:22
doesn't really run it. For example, if your program transfer your money from one bank to another bank, you probably don't want to run your code if you just want to check the type consistency. So type checker serves that purpose, and it only produce a type error or not for you. So, I mean, here, I just want to ask you,
21:42
okay, so do you think these two things are type consistent? If you think so, please raise your hand. All right, I see some hands here. The gradual type theory here, first, rule number one is,
22:01
all program parameters are default to any type. So this any type is consistent to all the types. And in this case, because before, we don't assign A to any, we don't annotate any types for A variable. It will be annotated as any type. And then, in this case,
22:24
we check any type and integer type is consistent or not. And yes, they are consistent because by the rule, any type is consistent, is type consistent to any other types. So in this case, we can say A and B is type consistent.
22:41
And second question again, do you think these two functions are type consistent? Raise your hand, please. Okay, again, rule number one here is, if you don't assign anything to the variable, in this case, the function,
23:02
the argument will be assigned to the any type and the return type will also be assigned to any type. And by the rule, when we compare two functions, they are type consistent or not, we basically check the arguments and return value type is consistent and any type is consistent to any type. So integer type is consistent and here we'll say these two functions are type consistent.
23:24
And third question, we have this A, we don't assign any notation equals to one and B we say is integer. And what will be the C type? Do you think the C type will be an integer? You can raise your hand here. This is actually a tricky one.
23:44
I don't see any hands here. That's actually pretty good, I would say. So in gradual typing theory, if you don't assign a type, A will be assigned to any type and then if you add any type to integer type, it will be any type.
24:01
But in fact, in the real world, Python's type checkers, it doesn't work in this way. You will find that A will be infer as a integer type and then C will also be integer type. So gradual type theory has another two rules. I'll just quickly go through that. First thing is pretty simple, just if you have a code like this,
24:21
it's not type annotated, so we consider, it's type annotated and you don't really assign the functions type, so it doesn't care because it's any type and so we consider it's okay. And the other one is if you try to assign some type and you put some inconsistent variable to it,
24:41
you got some argument type error. So basically the idea is this system should reject program has any inconsistency in the known part of types as static time. And at runtime, if there's any unknown types in runtime, your type system, your program can still catch that
25:02
in runtime, it's just that static time, you cannot catch that, but in runtime you can catch that. And here's one example that in my Python reference, this specific case, if you put a string into this function, the string is gossipy to list of string and the list of string plus the string will raise the type error in Python.
25:21
And some type checkers, particularly mypy detects no issue for this case. So we have a check away so far. I think, let me check how long we spent. We spent 25 minutes of our type theory so far. So we know that Python type system based on type theory, greater typing theory is something that not really,
25:42
it has a solid mathematic theory behind. Then we should talk about another thing is type checkers now. Here's a collab, you can also check this later. I mean, this collab is pretty simple just to try to let you be able to easily
26:03
to compare the type checkers. Remember in the PEP 729, the second part, we say these PEPs are endorsed by all major type checkers. So including pytype, pywrite, and mypy and pyre.
26:24
So they mentioned these four type checkers. Let's just check them then. So let's compare them quickly. Firstly, mypy is definitely something you may know. It's kind of OG. It's developed under Dropbox initially. I think Greedo was hired at that time. And then now it's under C-Python.
26:41
The time they started is developed in May 2012, December. That's actually earlier than the PEP 483's layer. And the advantage to use mypy would say, if you ask me why do you need to use mypy, I would say because it adopts the feature fast. I would say if you want to use some newest type features, then mypy should usually support that in a fast pace.
27:04
And there's pytype by Google from 2015 and pyre by meta 2017 and pywrite by Microsoft in 2019. That's four major type checkers they mentioned. And basically, when we saw other type checkers, we only care about why not use mypy. Just there's mypy, why do you develop
27:21
another type checker, what's the point? And for Google's case, mypy, they have a talk about this by the, I think I would say, original developer Rebecca Lehr. It highlights the capability of mypy to do the type inference.
27:40
So the coverage of the pytype will be higher than mypy because it can detect the, it can auto-annotate certain type by using type inference. And pyre, the reason why meta do it is because they consider this large scale called Instagram back end. And they want to adapt the greater typing at that time.
28:02
And they want a fast, fattest solution for that and mypy may not be a good solution for them. The other reason is also because they have some existing solution for hack, that's a PHP meta. So they just want to build up a new solution for it.
28:20
And Microsoft just want, I will say, the reason is probably some developer here, I believe, just IDE integration. So we know Microsoft is good at those IDE stuff. And they have a language protocol. So what it does is they need an efficient way to when you change one line of code and you don't need to rerun the entire static analysis
28:41
on your entire code. It can just change to detect what's wrong in the certain code line, lines change. And that's the reason that they call it a daily or just the intent type evaluator. And also what's to mention is that this, pyre is the probably only type checker not written in Python.
29:02
So we talk about many type checkers here. What do we want to know is like how do Python type system slow types? We have type checker S. We have many type checkers here. There is a function called reveal type, assert type in type system.
29:21
And it supports basically before Python 3.1.1, only the type checker supports it. So you need to write the code like this. But after that, you can write the code just directly. And this function does just check the types for different type systems.
29:41
And there's a paper, Python 3 types in the wild, published probably around 2020, yeah, and by RPI and IBM. This paper compares the mypy and the pytype. For me, today, it's not important to talk about the detail of this paper. Instead, there's an assignment mentioned in the paper
30:03
that's worth to look into. Because this field assignment in the type theory presents a different way, can represent how the type checker resolve type differently. So the example here, actually there's a GitHub issue I caught to just figure out this.
30:21
And it's kind of resolved by improving the document for the function, reveal type function. The variable assignment will be like this. We have a assigned to one, and later we assign the string to a. And the second case is the list of integer we assign to a, and then we append some string to a.
30:43
So that will change the type definition. And the other class variable is similar to variable assignment. It's just the variable under the class, they assign it. And let's see the type checker's results. I will find out here, if you use mypy,
31:00
sorry, let's look at C Python first. The C Python will interpret this clearly, as you expected, except you don't know the type under the list. That's the code that can intentionally erase the type to make the Python more efficient in runtime. In mypy case, you'll find out, like you cannot do so. Mypy reports all the errors here.
31:20
You cannot change the type in that time. That's because the first, when you assign integer to a variable, it's already inferred this error was an integer type. And then when you assign a string, it will just tell you that you cannot do so. And pytype, in this case, is relatively smart here. It just does the type inference for you,
31:42
and it does everything correctly. And then how about, let's just say, we do it with type of notation here. We tell those type checkers, we know the type is like this. And then now we know a could be integer or string, and it could be a list of integer or string.
32:00
And then you'll see the result will be like this. Again, the CPython just tells you everything is expected. And mypy's case, it does some type of inference. You'll find out in the beginning, it could be integer and string, and later it's inferred as a string. And in different cases, you'll find out, actually, even if we type or notate our code, the mypy and pytype, the behavior is still different.
32:23
In the third case, you got a different result here. So I'm not going to explain why you got different results. Instead, I just want to give you a takeaway here. In that paper, it mentions one thing. Arguably, have two fundamentally different type system violates the Zen of Python,
32:41
which famous states that there should be only one, and preferably only one obvious way to do a thing. And so definitely, can we rule a way to develop Python type checkers? So make all the type checker resolve the type equivalently. That's this takeaway here.
33:01
And move on, new specification in type systems, that's another thing I want to talk about. By the way, by saying new specification today, again, it's not about the first type theories, PEP285, that Boolean type we mentioned earlier. In stats is the specification about something, that is usually optional hints,
33:20
and basically not always checked at the runtime. And those are examples of PEP, and I will use the third one, the self-typed list one to go through it. Still, PEP 673 is self-typed. So again, not talking about detail here,
33:41
just the motivation of this PEP is before you have this PEP, when you try to have an inherent relationship of different classes, you'll find out there's a problem with our self-type. They need to use the type of R to define, to bound it, so to make it correctly. I would say to make it expectedly.
34:02
And with self-type, they expect you write code in this way, very clean, probably don't need to explain this further. That's the motivation for this PEP. And in fact, this implementation in C Python is super, super simple. You can see just one PR, and that PR is probably about 100 lines of code,
34:24
and most lines of code are just the comments. Firstly, you can, the first one is just that you can import this self-type in your code now. And as you can see, it's like you can return this self-type in your code as well. So the third thing is that there's a kind of place to describe how you should use this self.
34:43
But that's it, right? Because C Python does nothing on these optional hints. So you just need to support this thing. Okay, well you can now write a self. But a type checker is not a story. In my Python, let's take a look at my Python information. You'll find out it's almost eight times more effort
35:01
than C Python to support this. It needs to support the thing in their semantic analyzer to support self-type. It also needs to support it in their type checker. And further, because when we pass the code, we usually pass the code into a tree with many nodes. So you need to support the node as a self-type. And that's pretty much the PR.
35:21
You can look into this PR later if you are interested. And then how about another type checker? Let's just check one more type checker. In this case, let's check pytype. So pytype, I'm not going to talk about detail of how those PRs are doing. In fact, I also don't really check all the details there. You need to understand how to implement type checkers.
35:41
Otherwise, that could be too complicated about that. The thing what I want to say is the timeline to support a new sophistication you see here, you'll find out C Python takes from the PAP to implementation takes only three months. And my py takes 10 months to implement it.
36:01
And pytype takes 21 months to implement it. That's a really fun fact. OK, people are really happy. Finally, we'll have self-type in Python. Let's make our code really beautiful. But to find out the type checker actually takes way longer time than they thought to support that new annotation. That's exactly another type of way.
36:22
Can we shorten this noticeable time gap to support new specification to different type checkers? PAP 729 could be a solution. We don't know yet. It's an ongoing thing. But we'll say these two take away here, right? Can we rule the way to develop type checkers
36:41
and can we shorten this noticeable time gap to develop it? Let me see. OK, I still have time, so I'm going to just talk a bit further. In fact, when you see this photo, you see another onion on top. So that's your turn to do it. So a bonus here is like you can try
37:00
to implement your own mini type checker to understand type checker better, like me. Here is my implementation. It's not necessary you check my implementation, but just to let you know how to implement the type checker. Again, the information for this system is important because you plan to implement a system to check your type.
37:21
And so your input is supposed to be untyped code, partially typed code, and fully typed code. And your output just to be type error. And here will be some example you can try. Basically, they are all very basic. Argument type error, you can compare the OKs output and ng output. And assignment type error and the return value type error.
37:40
They are all very iconic one. Just you see like you intentionally just input something invalid, then your system should just report some issue. And then you got your mini type checker to do it for you. Mini type checker's implementation, I will say, if you don't know how to implement it, I recommend a library called libcst.
38:01
It's actually used by PyType Empire as well. And this libcst does the thing just to parse your code, helps to parse your code into a tree. And then you can use this tree as a thing to traverse it twice. Firstly, to semantic analysis it and then type check it. That's exactly what my Py supports self-typing.
38:21
You may notice that. And if you feel very boring, then further you can just try more inputs. Of course, you can come up with some currently supported specifications of Python types. Or I recommend you try generics, because generics is often tricky, like you need to parse the code twice.
38:42
First of all, you need to collect your type information. Second time, you need to use the information to check the type. And right, that's it. So thank you, and yeah. Thank you very much, Kia, for that informative talk.
39:02
We have five minutes for Q&A. We have two microphones. If somebody has a question, you can step up to the microphone and ask the question. Let's see if we have people who actually want one. And there we go. Please ask your question. So you look like a person who knows a lot about type checkers.
39:23
And what type checker do you use then? In my case, because I work for some famous big company, so I'm used to that comparison. I work for one of the company of them, so we use that. Your question probably is more about what type checker
39:43
I recommend you to use, maybe. Exactly. I will say, if you don't know what to use, then likely you just need to use mypy. And if you really want to seek for some specific purpose, such as you have large scale code, we may look into the pyer.
40:02
And if you use IDE, maybe Microsoft will just recommend you use their type checker. And if your system is not really type annotated, you can consider the pytype. They have a higher coverage. But pytype has a limitation. Their support is often slower than the Python version.
40:20
Right now, they support up to Python 3.11 only. So that's something you need to put into your consideration. Thank you. OK, thank you very much for the question. And it looks like our audience is getting hungry, so I don't see any other question. Are you going to ask a question? Yes, please come to the microphone.
40:41
Thanks a lot for the talk. I was wondering if you think that at some point in time, or if you have any information that is a bit hidden, that at runtime, if we pass the wrong type to a function that was annotated with a different type, we might get an early run type error instead of just
41:01
the function proceeding? Sorry, I don't really get what's your question. So if you think that maybe at some point in Python, they will have checks a bit earlier, for instance, at the time that we make the function call? You mean interpreter itself?
41:21
I think probably no, because when I proposed some kind of, I remember there is another issue I cut to the C Python, and they say usually they focus on the performance first, and that kind of additional check to have the efficiency cost. And that's not something they will try.
41:40
I think that one example I can share with you later is about some type thing in data class. OK, thank you very much for the question. We have a question at the other microphone, please. Yes, so two questions. So the first one, is there any effort to standardize the error messages between type checkers, so they're kind of like throw the same error message, rather than depending on how they're working,
42:02
they might throw different? And the second one, is there any thought put into how new type checkers can join the club proposed by PEP 729? These are very, those are very good question. I would say the answer is that's the reason we need the PEP 729,
42:20
because you have a certain console you can look into and you can consult with. And if you want to join the club, you are a new type checker developer, want to write such as a FET is the type check in Rust, maybe, then that could be the thing that people can join together to discuss about that. And about error message, I will say the same.
42:40
Just, I'm sure like this console was there after a lot of type checker was there, were there. So to, I will say to unify the error message, that could be the thing in the long run, in the future likely can happen. If again, the way type checkers resolve types are different.
43:01
So that's probably the biggest challenge they need to figure it out. And that's my take of that. But again, PEP 729 could be a solution, we don't know, but that's the reason why we formed this process. Yeah, I believe. Thank you very much for the questions and answers. This is, alas, all we have time for now.
43:21
So let's have another big applause for Kirschl. Thank you. Thank you very much.