We're sorry but this page doesn't work properly without JavaScript enabled. Please enable it to continue.
Feedback

Types and Ruby Programming Language

00:00

Formale Metadaten

Titel
Types and Ruby Programming Language
Serientitel
Anzahl der Teile
69
Autor
Lizenz
CC-Namensnennung - Weitergabe unter gleichen Bedingungen 3.0 Unported:
Sie dürfen das Werk bzw. den Inhalt zu jedem legalen und nicht-kommerziellen Zweck nutzen, verändern und in unveränderter oder veränderter Form vervielfältigen, verbreiten und öffentlich zugänglich machen, sofern Sie den Namen des Autors/Rechteinhabers in der von ihm festgelegten Weise nennen und das Werk bzw. diesen Inhalt auch in veränderter Form nur unter den Bedingungen dieser Lizenz weitergeben.
Identifikatoren
Herausgeber
Erscheinungsjahr
Sprache

Inhaltliche Metadaten

Fachgebiet
Genre
Abstract
Types have been a big interest for Rubyists for more than ten years. Even before Ruby3, some researchers have tried to type check Ruby programs. All of them had failed. No one in the world has successfully implemented practical type checker for Ruby programs yet. Why is it difficult? How have we tried? What do we want exactly? Can we find any solution?
43
Vorschaubild
29:29
44
Formale SpracheSoftwareentwicklungAnalysisStatistische HypotheseProdukt <Mathematik>TypprüfungProgrammDatensatzModifikation <Mathematik>TypinferenzHydrostatikGasströmungObjektorientierte ProgrammierungMeta-TagDynamisches SystemCoxeter-GruppeMultiplikationsoperatorObjektorientierte ProgrammierungSoftwareentwicklungGruppenoperationFormale SemantikProzess <Informatik>KonditionszahlProgrammbibliothekParametersystemKartesische KoordinatenArithmetischer AusdruckProgrammierungProgrammiergerätSoftwaretestUnabhängige MengeProgrammanalyseProdukt <Mathematik>Freier LadungsträgerGlobale OptimierungRechter WinkelNichtlinearer OperatorMultigrapht-TestZellularer AutomatWiderspruchsfreiheitKategorie <Mathematik>Generator <Informatik>VerkehrsinformationEin-AusgabeMailing-ListeStreaming <Kommunikationstechnik>Physikalische TheorieNeuroinformatikSichtenkonzeptNotepad-ComputerPunktTLSTwitter <Softwareplattform>Wort <Informatik>Endliche ModelltheorieURLAnalysisTypinferenzKlasse <Mathematik>GraphStichprobenumfangZahlenbereichCodeMetaprogrammierungDatenflussProgrammfehlerZeichenketteAppletVerschiebungsoperatorElektronische UnterschriftNatürliche SpracheJSONXMLUMLComputeranimation
TypinferenzHydrostatikModifikation <Mathematik>Relation <Informatik>SystemidentifikationOrdnungsbegriffZeichenketteKlasse <Mathematik>Ganze ZahlObjektorientierte ProgrammierungSchreiben <Datenverarbeitung>GleitkommarechnungLogischer SchlussAnalysisParametersystemInstantiierungStrukturierte ProgrammierungHydrostatikLogischer SchlussParametersystemObjektorientierte ProgrammierungZeichenketteModifikation <Mathematik>t-TestRechter WinkelVerschiebungsoperatorInverser LimesGeradeProgrammierungKlasse <Mathematik>SystemidentifikationZahlenbereichTypprüfungRelativitätstheorieGanze ZahlSystemaufrufTypinferenzCodeImplementierungMessage-PassingMaßerweiterungSoftwareentwicklungStreaming <Kommunikationstechnik>Mailing-ListePerfekte GruppeKonditionszahlSpeicherabzugFormale SemantikNichtlinearer OperatorGraphFehlermeldungMereologieIdeal <Mathematik>Computeranimation
TypinferenzProgrammDatensatzModifikation <Mathematik>Logischer SchlussObjektorientierte ProgrammierungDynamisches SystemApproximationStellenringInformationSystemaufrufSinusfunktionHill-DifferentialgleichungFormale SemantikMeta-TagSoftwareentwicklungStrukturierte ProgrammierungProgrammiergerätElement <Gruppentheorie>StellenringSoftwareentwicklungLogischer SchlussVollständigkeitAlgorithmusFreewareSpannweite <Stochastik>Klasse <Mathematik>Schreiben <Datenverarbeitung>Virtuelle MaschineEinsCodierung <Programmierung>p-BlockParametersystemTypinferenzMAPFormale SemantikRelativitätstheorieProgrammierungProgrammierspracheInverser LimesVariableGebäude <Mathematik>Mapping <Computergraphik>ZahlenbereichModifikation <Mathematik>SystemprogrammierungMeta-TagMatchingApproximationObjektorientierte ProgrammierungDatensatzSchlüsselverwaltungCodeFitnessfunktionVersionsverwaltungPhysikalischer EffektLogarithmusBildschirmmaskeSoftwareschwachstelleOrdinalzahlWeb SiteTabelleAggregatzustandWort <Informatik>ZeitrichtungRechter WinkelDiagrammFunktion <Mathematik>MinimumDigitale VideotechnikComputeranimation
TypprüfungLogischer SchlussKlasse <Mathematik>SoftwareentwicklungMeta-TagObjektorientierte ProgrammierungOffene MengeDatenstrukturLaufzeitfehlerAbfrageGasströmungHydrostatikImplementierungPrimitive <Informatik>MetaprogrammierungSoftwareentwicklungUnabhängige MengeOffene MengeTechnische OptikAttributierte GrammatikCASE <Informatik>ResultanteSingularität <Mathematik>Lineare OptimierungZufallsgeneratorGraphSchreiben <Datenverarbeitung>KonditionszahlFormale SemantikMultiplikationsoperatorObjektorientierte ProgrammierungMailing-ListeIndexberechnungHydrostatikDatenbankImplementierungKartesische KoordinatenMereologieSpeicherabzugMultigraphRechter WinkelTypprüfungGRASS <Programm>Automatische IndexierungStrukturierte ProgrammierungKlasse <Mathematik>Dynamisches SystemVariableSystemaufrufCodeFunktion <Mathematik>BitProgrammbibliothekInstantiierungComputeranimation
HydrostatikImplementierungTypprüfungGasströmungFehlermeldungZeichenketteJust-in-Time-CompilerRechenwerkLaufzeitfehlerDatenstrukturFormale SpracheSoftwareentwicklungKonditionszahlSchreiben <Datenverarbeitung>ProgrammbibliothekSpeicherabzugSystem FCASE <Informatik>ProgrammierungStatistikTypprüfungMultiplikationsoperatorWald <Graphentheorie>Mailing-ListeSystemprogrammierungÜberlagerung <Mathematik>Strukturierte ProgrammierungPunktWeb SiteGesetz <Mathematik>BitFehlermeldungKonfiguration <Informatik>Rechter WinkelEinfacher RingCoxeter-GruppeMereologieImplementierungUnabhängige MengeSoftwaretestLogischer SchlussLaufzeitfehlerKlasse <Mathematik>RechenwerkProgrammiergerätSystemaufrufIntegralZeichenketteCodeSchlüsselverwaltungKomponententestProdukt <Mathematik>Computeranimation
Formale SpracheSoftwareentwicklungZeichenketteProgrammierungElektronische PublikationKlasse <Mathematik>Elektronische UnterschriftParametersystemFunktionale ProgrammierungArithmetischer AusdruckFormale SpracheKategorie <Mathematik>Gesetz <Mathematik>Einfacher RingOffene MengeSoftwareentwicklungWärmeleitfähigkeitKonditionszahlPunktResultanteComputeranimation
ZeichenketteKlasse <Mathematik>VererbungshierarchieProgrammDynamisches SystemSoftwareentwicklungSchreiben <Datenverarbeitung>Klasse <Mathematik>ZeichenketteExogene VariableCodeObjektorientierte ProgrammierungMultiplikationsoperatorParametersystemProgrammiergerätZahlenbereichTeilmengeProgrammierungSpieltheorieKonditionszahlPunktWärmeleitfähigkeitMechanismus-Design-TheorieAdditionKonvexe MengeCASE <Informatik>MetaprogrammierungSchnelltasteRechter WinkelZusammenhängender GraphResultanteFaktor <Algebra>Güte der AnpassungStichprobenumfangElektronische UnterschriftComputeranimation
TypprüfungObjektorientierte ProgrammierungLogischer SchlussFokalpunktMeta-TagSoftwareentwicklungModifikation <Mathematik>ProgrammDatensatzTypinferenzHydrostatikGasströmungDynamisches SystemMAPProgrammierungSoftwareentwicklungCoxeter-GruppeFormale SpracheElektronischer ProgrammführerTypinferenzStellenringMultiplikationsoperatorHydrostatikObjektorientierte ProgrammierungDefaultProgrammiergerätKontrollstrukturMereologieComputeranimation
Offene MengeMetropolitan area networkKontextbezogenes SystemAggregatzustandComputeranimation
COMXML
Transkript: Englisch(automatisch erzeugt)
It's time to start my presentation. So, my presentation is about the type checking
for Ruby programmers. So, okay, so let me introduce myself. I'm Sotaro Matsumoto. So, my account is that one, and you can find me on Twitter or GitHub.
So, I'm working as a CTO at a startup company called Saishii. It is located in Tokyo, and our product is a code review assistant. It analyzes your pre-requests automatically and gives you some reviewing suggestions automatically.
So, technically, this is a program analysis. So, I have been working for program analysis. It is to reason some properties of your programs
without executing it. So, it includes some flow analysis or some of the type checking. So, it was in 2005, I was a graduate student, so I started studying about the program analysis, and then I published some papers
about the type checking of Ruby programs. So, I have, in fact, about 10 years of career for this program. So, yeah. So, let's start about what is the type checking benefits?
So, as you know, it helps you to find more bugs without running your tests, without writing your tests. So, if your program contains some invalid method calls,
that type checking will tell you. So, if you pass an invalid argument to some method calls, type checking will tell you. So, it helps you to find more bugs in your program. So, another aspect is, it is a verifiable documentation.
So, when you are writing your libraries or you are writing your application code, you see a lot of libraries, I'm sorry, you see a lot of documentations. So, the class documentations and method documentation, so you find which methods are available in that class
or how to pass the arguments to that method. So, they are usually written in English or Japanese, so natural language. So, you can read and understand what the methods are, but the computer doesn't. So, with types as a verifiable documentation,
that type checking tool can verify instead of you. It also helps some refactoring. So, when you are working on some legacy code, so you try to refactor some of that code.
Maybe you change the method signatures or method names. So, after changing your definition of that method, you have to update all of the calling locations on your programs. So, you have to find out every method calls in your code. So, instead of using some graph or running tests,
the type checking tool will help you where you have to fix. Another big benefit of type checking is the optimization, but today it is out of scope of my talk, so.
So, this is a really short sample of the type checking for Ruby. So, the humans have tried to type check Ruby programs for about 10 years. So, I list here four type checking tools.
So, it is developed by some researchers, some students, including me. So, it starts with 27 or 29. I call it, it is the first generation of the type checking tool for Ruby.
So, it was focusing to type the objects in Ruby. So, I mean the duck typing. So, the second generation is number three and four listed here, and it is for support meta-programming.
So, the difficulties for type checking Ruby program is at least three difficulties. The first one is type inference. As you know, Ruby is dynamically typed language, so there is no type annotations included in your Ruby code.
So, to check the consistency of the types in your Ruby code, it first to infer the types, how that code, the expressions, the nodes only in your program should be typed. So, the type inference is the first difficulty. The second one is that the semantics
of Ruby's object typing. So, I call here the dynamically typed objects, or you know that it is duck typing. So, what is the duck typing is?
So, it means that the class of the receiver does not matter when you call some methods. So, this is different from other popular, some of the popular statically typed languages, like Java or C Chef, so you are a lobbyist,
so you love the feature. So, let me explain using the example. So, the right code is to define the right method. So, it receives one argument called IO, and using the left shift operator,
then bring some string. So, from the point of view of the types, we can use any object if it supports the left shift operator. So, we can use the right method for IO files,
or you can try the string IO objects. You can try the string, and in fact, we can try with the array. So, they all have the left shift operator, and we can use for that.
So, to support that duck typing semantics. So, I'd like to introduce a paper. It is static type inference for Ruby. It's published in 2009 by Professor Foster
and maybe his students. So, it is based on the structure of subtyping, and it needs some annotations for polymorphic method. So, I found one week ago that the implementation is still available on GitHub,
so we can try to build that tool, called the Diamond Back Ruby. So, what is structure subtyping? It is subtyping with the structure relation identification.
So, yeah, let's see the example. So, this is the right method has the type it is shown in the left. So, it takes one argument of an object. It should have a left shift operator,
and it should take the string argument. The return type of the left shift operator is not used at all in the method, so it is written using the variable a. So, let's see how we can type check that method calls.
Like this. So, this is the first example. It pass a string. So, it checks the type of the string, that definition of the string class object. So, it finds there is a left shift operator in that definition.
So, the typing is okay. How about string IO? So, it also have the left shift operator is okay too. It returns the string IO, but the return type of the left shift operator
is not used at all in the right method, so it doesn't matter. But, how about we pass a true? It is a true class, so we cannot find any left shift operator in the definition of the true class. So, this is a type error.
How about integer? It has a left shift operator, but the argument is integer. So, we cannot use that integer to pass, we cannot pass the integer object to the right method. So, this is a very easy explanation
of how structural subtyping is. So, the diabond-back Ruby is based on the structural subtyping, and it can infer some types of some of your Ruby programs but there is a big limitation
that it cannot infer the polymorphic method. So, this is an example of the polymorphic Ruby programs, right, that ID method takes one argument and returns that argument immediately. So, the first line is ID new of ID three will be number three
so we can calculate three plus three will be six. And the next one is we pass a string, so the type of the ID of who is a string, so string concatenation also works.
So, there is no type error in this program. But because the diabond Ruby cannot infer the polymorphic method, so it saves some type errors. So, if we want to infer, if we want to define polymorphic type methods,
we have to write some annotations in our Ruby code. So, this is my paper in fact. So, it's type inference for Ruby programs based on polymorphic record types.
It was published in 2007. And my paper is to infer the polymorphic method types for Ruby programs. So, it is based on ML type inference. ML is not machine learning, it is meta language, programming language.
So, we used an encoding of polymorphic record types to represent the type of Ruby object. So, I believe it works, but there is also a big limitation that it cannot type some Ruby buildings.
So, some Ruby buildings includes array hashmap. So, our type system cannot give a type to array match. Then we have a conclusion like this. So, we can give types to Ruby's object
using structural subtyping or maybe polymorphic record types. So, it is a good approximation of the semantics of Ruby's type. So, that subtyping relation is defined by
if that type has a method or not. So, it is really good fit for the Ruby semantics. But the problem is that type inference does not work well. So, if we choose a structural subtyping,
we cannot infer the polymorphic types. If we choose a ML based type inference, we can infer the polymorphism, but we cannot type some of the Ruby buildings. So, the next question is that do we really need type inference for Ruby or not?
So, we can see that next idea of local type inference. So, it is the weaker version of the type inference. So, instead of inferring everything in the program, it only infers the local elements.
Like the local variable types and if we use a polymorphic method, it infers the types. So, with local type inference, the programmers should write method types or class types.
So, we need some annotations in the Ruby programs, but we don't have to write everything. So, a good thing is it is easily integrated with existing languages, like maybe C++. It's recently introduced a local type inference and we can think about the Scala or Swift.
They also have the local type inference. So, this is an example that, this is a Ruby program with no type annotations. So, to type check this Ruby program,
we need a complete type inference algorithm. So, there's no type annotations. It is untyped or we need a complete inference. So, this is the opposite. It is the free type annotated. So, we have to, I'm sorry,
the range ones are the type annotations. So, we have to annotate the method arguments, method return type, and we have to annotate for the local variable types.
The size local variable is integer here, what type, I think like that. We also have to annotate the types of the block parameters and the block return values. And in fact, the map is a polymorphic method, so we have to explicitly give the type applications,
so it is a string. So, the middle is the local type inference. So, we need to give the type annotations for the method parameters and the method return types, but in this example, we don't have to declare any type annotations
in the local variables or to using the blocks or maps. So, the type of local variable size is inferred from its right-hand side. So, array.size is integer. So, the type of size is integer.
So, something like that. So, we have something like, some answer like this. So, we should try that structure subtyping and local type inference. So, we know that structure subtyping is enough to support the little semantics
called stack typing, or we can use the local type inference to minimize the number of keys you have to hit. So, this design is similar to typescript.
It has structure subtyping and it also infer the types locally. So, the type checking difficulties now like this. So, instead of having complete type inference, we can use the local type inference.
We annotate some Ruby code using the type annotations. So, but we don't have to write every types in your method definition. So, we have the difficulties on dynamically typed object,
but we now, we can support that stack typing semantics using the structure subtyping. So, the difficulties it is left to open is meta-programming.
So, what is meta-programming? You know that it is a program that modifies a class or method definitions during its executions. So, the popular meta-programming primitives in Ruby includes defining method for class.new.
So, if we write without meta-programming, we can write the left hand side. So, it's defining a person class and defining a method called name. It returns instance variables.
So, using the meta-programming primitives, we can write on the left. So, we use the class.new method. We use the class.new method instead of the class syntax. We use the define method method to define the method instead of the def syntax. And we can also use the instance variable get method
instead of writing the name of variables. So, the meta-programming is so popular, so abused in your Ruby code. So, it's not a special one.
So, you write attribute reader or attribute accessor, it's a meta-programming. It's a method to define the accessor methods. So, it's meta-programming. How about give record? So, it connect to your database and finds the current definitions
and finally it defines some attributes by itself. So, it's meta-programming. How many or belongs to also define the methods by itself. How about require? Require, I think that everyone have used require.
So, we can do something like this. If some condition holds require, so it says that the random number, probably about 30% of the execution defines PP method,
but the rest is without the require. So, this is same to the open classness, something like this. So, we can have a condition surrounding the class definition
so it's not clear that the class is defined or not. So, this is the difficulty of meta-programming. So, it's done by some method calls. So, it's really difficult to identify the structure of actual type structures, the structure of the types
without executing that. So, we have to infer the cases that if there is the code snippet using the meta-programming, it's called before this case was sold. So, one idea is to support,
to give a special support for attribute leader. So, if we find attribute leader in the class definition, we see that it is to defining the methods using, we translate the ADDR leader method code
to the depth syntax. Maybe we can do that, but what if that method is over-laden? So, yes, so in that definition of person class, it looks like that it is to define the leader attribute,
but in fact, there is override in the object class. So, it is ADDR access, so everything will go broken. So, this is the meta-programming difficulties and I think there is two solutions for this.
So, the first one is we stop type checking in static array. So, we can type check that during the execution instead of the check everything in before execution.
So, this is a really cool paper. It is published last year, just in time static type checking for dynamic language. It is by Professor Foster and I don't know who is that.
Professor Foster is the team, he develops that Diamondback lobby, so his team continues almost 10 years for the lobby's type checking, so it's awesome thing. So, in this paper, the interesting thing is, it runs the static type checking during execution.
Static type checking during execution, so it's a bit difficult to understand to me. So, the implementation is called Hummingbird and it's built on top of RDL, so you may know that it is a dynamic type checking.
Dynamic type annotating of library for Ruby. So, this is how the Hummingbird implementation type checks. So, this is an example that it define F method.
So, if we execute that program in Ruby, it is no error will be detected, no error will happen. So, we pass the F method, empty string and false.
So, it goes to the if condition is the false and then x.foo will not be called. So, then no type error will happen. But, with just in time type checking is called Hummingbird,
so type error is detected. So, it doesn't type check statically, but during the execution of the program, when the execution reaches on the beginning of the method F, it type checks its body.
So, then the x.foo if y is checked. So, usually the static type checking ignores the branching conditions. So, it goes when the if condition holds or not. So, it checks up both case. So, it tries to type check the else case
and it type checks the x.foo's method call and it knows the string doesn't have a foo method, then it is a type error. The interesting thing is that the type checking
is done during the execution. So, if we have a method definition in the string class like this, so if there is a call snippet to define the foo method of the string, so it will pass the type check by Hummingbird.
So, yes, so it has a good point that it detect more errors in unit test. So, it's expected to be used to run the unit testing or integration testing, anything you write
the automated testing. So, in the automated testing, your program calls the most of the methods you are defining. So, then it type checks most of the cases of your programs. So, this is much better than writing the unit test
for every branching coverage. So, even if we have a low branching coverage, it finds more errors. However, in my opinion, I don't like this approach so because that type checking
is depending on the runtime behavior. So, if your program requires some library, it is not called in the production. So, that library, I'm sorry, you have some classes in your program may have another method.
It is not available in production or such things. So, I want to go to the next one. So, to support metaprogramming, we want to ask programmers to give the type structures.
So, instead of the type checking tool to infer the structure of types, the programmer gives how the type is. So, this is, in fact, my type checker called Steve. I had a presentation last week, I guess, September.
So, it is a gradual typing for Ruby. So, it's available in GitHub or you can try using gem. So, I'm sorry, it is really experimental still and it's not released yet. So, you have to give the pre-option to install that.
So, key idea of the type checking tool is the type definition is written by another limited language. So, it is not extracted from the Ruby code. So, this is an example.
It defines a contact class. So, it has an initialized method. It has a name keyword arguments and the type of the name is string. It also has a name properties.
It returns the ring. So, we write something like this. We specify the signature of classes you are defining in your Ruby programs. Every classes you define in your program, you have to write the signatures. So, this is written in .rbi file in Steve
and the type definition language is really limited functionality. It's really limited expressiveness. So, it is to give the precise type definition statically without execution. So, there is no open class, no conditionals,
no require, no meta-programming. So, we can read the type definition file and understand how that type is defined precisely. So, let me explain how the type checking will be.
So, we have the contact class type definition here and we have some Ruby code to define the contact class. So, we give type annotation like this at implements contact. It tells that the class is conforming to the class definition of contact.
So, if we find the implements annotation, it checks that it define if the class defines all methods defined in the signatures. So, it first checks the initialize method is defined or not and it checks that name parameter
have, name parameter is defined in the initialize method or not. And finally, it also checks the name method is defined or not or if the type of the name method is correctly defined or not. So, this is about the meta-programming.
So, we can try to define the contact class using some meta-programming called ADDR reader. So, in this case, the name method is not defined no def syntax for the name method. So, the Steve cannot understand
if the name is defined or not. So, it is the programmer's responsibility to tell that we, I define the name method using without the def syntax. So, this is at mark dynamic syntax. So, if you know objective C programming language,
so it also has at mark dynamic annotation. So, because the Steve doesn't know how the name method is defined, so you can use another meta-programming technique like the method missing.
So, instead of ADDR reader, you can define any way you want. So, the difficulty is some Ruby programmers cannot be typed statically using Steve. So, this is a very simple example.
It defines foo method in class A. So, in the definition of the foo method, it defines foo method again. So, if you call the foo method first, it returns number three, but it also defines new foo method.
So, the next time you call the foo, it returns a string instead of the integer. So, unfortunately, Steve cannot give a good type for this kind of program, but in my opinion, foo cares.
So, probably, maybe you don't write a Ruby program like this, or maybe you don't want your teammates to write program something like this. So, it's not a problem. So, I'm sorry.
So, I introduced the four type checkers it has developed for this 10 years. So, the first two type checkers are focusing on typing the dynamic array type objects, and it tries to infer the types,
but after some years of some efforts, we found that we cannot infer the types to Ruby programs. So, we have to write some annotations in Ruby programs, or we can use the technique called local type inference to give that,
to tell how the Ruby program is typed. And it moves to the next stage that we focus on how metaprogramming can be supported. So, just in time, static type checking for dynamic language is a really awesome paper.
It's very interesting. But I don't like that, because it requires program execution. So, I tried to develop my own, another type checker for Ruby. So, it is steep, so I had a presentation in Ruby guide.
So, I introduced the four type checkers, two historical type checkers about 10 years ago, and two relatively new type checkers. So, and there is no conclusion in this talk, so,
the type checking for Ruby is still an open problem, so anyone on the Earth doesn't have good answer to, we can do that one, not how we can do that one. It's impossible, so there is no answer yet, so. I'll stay, so, yeah.
We are working for this, so, yes, thank you.