Types and Ruby Programming Language

Video in TIB AV-Portal: Types and Ruby Programming Language

1 views

Formal Metadata

Title
Types and Ruby Programming Language
Title of Series
Number of Parts
69
Author
Matsumoto, Soutaro
License
CC Attribution - 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 license.
Identifiers
Publisher
Confreaks, LLC
Release Date
2017
Language
English

Content Metadata

Subject Area
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?
Loading...
Meta element View (database) Scientific modelling Multiplication sign Parameter (computer programming) Semantics (computer science) Programmanalyse Programmer (hardware) Type theory Object (grammar) Row (database) Aerodynamics Polymorphism (materials science) Product (category theory) Process (computing) Electric generator Electronic mailing list Formal language Hypothesis Independent set (graph theory) Category of being Type theory Fluid statics Typprüfung output Right angle Mathematical optimization Point (geometry) Computer programming Product (category theory) Presentation of a group Transport Layer Security Mathematical analysis Student's t-test Streaming media XML Graph (mathematics) Computer Theory Twitter Operator (mathematics) Typinferenz Software testing Traffic reporting Condition number Consistency Cellular automaton Expression Computer program Cartesian coordinate system Computer programming Local Group Dynamical system Uniform resource locator Word Personal digital assistant Charge carrier Object (grammar) Library (computing)
Meta element Greatest element System call State of matter Range (statistics) Finitary relation 1 (number) Instance (computer science) Parameter (computer programming) Function (mathematics) Mereology Semantics (computer science) Inference Fluid statics Programmer (hardware) Type theory Atomic number Object (grammar) Core dump Row (database) Diagram Arrow of time Information System identification Extension (kinesiology) Local ring Error message Vulnerability (computing) Physical system Social class Logarithm Polymorphism (materials science) Theory of relativity Block (periodic table) Electronic mailing list Parameter (computer programming) Inference Type theory Message passing Fluid statics System identification Website Hill differential equation Right angle Clef Computer programming Implementation Perfect group Typinferenz Floating point Mathematical analysis Student's t-test Streaming media Approximation Number Writing Social class Causality Operator (mathematics) String (computer science) Ideal (ethics) Typinferenz Integer Data structure Condition number Form (programming) Shift operator Graph (mathematics) Key (cryptography) Sine Computer program Set (mathematics) Semantics (computer science) Limit (category theory) Computer programming Approximation Table (information) Dynamical system Word Digitale Videotechnik String (computer science) Object (grammar) Integer Local ring
Meta element Computer programming Query language Implementation Random number generation Run time (program lifecycle phase) Multiplication sign Primitive (album) Graph (mathematics) Mereology Semantics (computer science) Open set Attribute grammar Fluid statics Social class Object (grammar) Database Core dump Linear programming Aerodynamics Data structure Implementation Typprüfung Condition number Graph (mathematics) Metaprogrammierung Electronic mailing list Set (mathematics) Price index Cartesian coordinate system Grass (card game) Computer programming Open set Inference Independent set (graph theory) Type theory Subject indexing Fluid statics Personal digital assistant Optics Mathematical singularity Typprüfung Right angle Object (grammar) Data structure Writing Resultant
Ferry Corsten Multiplication sign Parameter (computer programming) Mereology Inference Type theory Computer configuration Forest Core dump Aerodynamics Error message Typprüfung Physical system Covering space Electronic mailing list Bit Functional (mathematics) Formal language Electronic signature Type theory Independent set (graph theory) Category of being Fluid statics Typprüfung Website Right angle Thermal conductivity Data structure Writing Resultant Point (geometry) Computer programming Implementation Presentation of a group Run time (program lifecycle phase) Open set Software testing Data structure Condition number Just-in-Time-Compiler Expression Ring (mathematics) Statute Computer programming Error message Personal digital assistant String (computer science) Statistics Units of measurement Library (computing)
Point (geometry) Meta element Computer programming Inheritance (object-oriented programming) Presentation of a group Connectivity (graph theory) Multiplication sign Auto mechanic Dynamical system Control flow Parameter (computer programming) Mereology Focus (optics) Subset Number Fluid statics Programmer (hardware) Social class Goodness of fit Type theory Object (grammar) Row (database) Typinferenz Aerodynamics Condition number Addition Default (computer science) Polymorphism (materials science) Metaprogrammierung Keyboard shortcut Computer program Sampling (statistics) Computer programming Inference Electronic signature Type theory Fluid statics Convex set Personal digital assistant String (computer science) Factory (trading post) Typprüfung Dependent and independent variables Right angle Game theory Object (grammar) Thermal conductivity Resultant
Context awareness State of matter Coma Berenices Metropolitan area network
a was a a a
a the the the the the the and it looks so it's
time to start my presentation so my presentation is about tight checking cold the program so the so they can introduce myself and so the what's model I accommodates that and you can find me on Twitter so I was deemed as a city or at a company that a company called Cyber Shiite it is repeated in Tokyo and product is about called view assistant it and the right is we operate with salt much theory and gives you some reviewing this suggestions automatically and to compare this is a program and then it's it's so and have been working for program analysis it is to read and some properties of you have programs resolved executing 8 so it can grow some from 1 and is what are some of the text checking and it was in 2 cells and I I was a graduate student so I studied studying about what's the program analysis and then I published some papers about that of taking over the program so I have to import their about 10 years of a carrier pull this the problem the fed up with that then a boat that whether it's that chicken benefits so as you know it terrorist it it helps you to find more what bias without running at test result right your so if you your program contains sound in bright of called that type checking with the you so if he was you past and braid argument to some MIS of course that you can really do you so it helps you to find more about it in your program so that's another aspect is that it is up but if I ever wrote documentation so when you are writing your Ribery's white writing your application could you see a lot of libraries and so if you see a lot of the conditions so that crossed the conditions is of the conditions so you find pitch methods of a a in that process for how can you they hope to pass the arguments to the method so they are usually written in English or Japanese so much a wrong answer so you can read and understand what the missiles at but computer doesn't so with tight as a preferred documentation that type checking to can be fired instead of you what it's also have some new proctoring so when you are working on some because cold so you try to to us and some of them called maybe you change that snitches 1 is of the names so after changing here the condition of that mess that you have to update or or point locations on your program so you have to find out every MIS of course in your court so you instead of using some graphs while running the tests that that chicken curious hope you where you have 2 weeks and as the benefits of such a thing it's optimization but today it is out of the scope of my book so so and this is very short in summary of the top 2 teams for the so and the humans have tried to take the chick to be programs for about 10 years so and list here for and this she had out for tech taking to so that is the report by some some some such students including me so it's that it's that really 7 what in the 19 accords it it is so fast generation of said that objecting to a full of the so it was focusing and tight to objects into these so I mean that that that so that's 2nd generation is that of must be an aphoristic yeah and it is full support so programming so said that the characters for OPEC taking newbie programmers and this test be difficulties the first one is that in France as you know the the is that they carried type to run it so it stays in or politicians in group into logical so 2 chicks set consistency also types in your to be called bit fast to invite the tides how we set called the expressions that no was on in your program should be tagged so that they in friends itself hostage currently to take on 1 needs that there the semantics of the who be objects that so I called she had that they immigrated objects or what you just you know that it is bad that that being so what is that that words of that thing is so it means that that crossed over the embassy but doesn't might out when you call some missiles so this is different from what other people beer some of the popular that the agreed to run its right to about what she ships you who are the beast so you lots that future the average explained using the example so that the right qualities due to find the right missile so it receives a 1 argument caller ID and using left deceived operator and bring some doing so the from the point of view with that time so that we can use any object if it supports their look to see if the operator so we can use right missile fall hordes find what you can't write that you objects can't write are streams and their input we can't write these so they the all have lifters Rabin abbreviated and then we can use so had to support
that that that they've been semantics so on I'd like to introduce up OK that it is a static type inference for b it's published in 2009 by the promise of course there maybe his students it is based on the structural subtyping and thought it needs done conditions for perfect missile so so following 1 week ago that the implementation is there a way over on the top so we can try to be used in that set of called that they want but the so but there's structure of subtyping it is there subtyping with that structure relation identification so so list ever sees that example so this is that the right method constant tying it is shown indirect so it states 1 and and book of eject it has it should have a lived to shift operator and it should take some strange I mean that began tie that lived shift operator is not used at all in our message so it is and and using some idea of a so this see how we can accept this of callers like this so this is the last example it past extreme so it's chicks that type of the stream that an definition of a stream graph objects so it days I received operator in that said 2 conditions so that I think it's OK publish string ideal it was so hot star if the shift operator so K 2 it returns I you but said the turntable that if the shift operator is not used at all in the right message so it doesn't matter but how well it and we passed them to do it is to regress so we cannot find any you have to sift operator in the technique and that to aggressive so disease like error how about indigenous it has a lift school operate but the argument is an integer so we cannot use India to pass and we cannot integer objects to the right so would disease that many easy of how structural subtyping so so they want but really is based on the structures of dating and it can mean some types of that some of the of the programs but states out the limitation that it cannot moving so this is an example of that part it to be programs right IT Mr. takes 1 argument and we dance at Edmund immediately so that that that that the 1st thing is I need new for IT to be will be number so we again great great to be pressed the ruby aspects and the next 1 is and we passed a stream so that they will that IT old crew is pestering so string concatenation or select so days note that are in this program but any ghosts they on the B cannot impose upper so it stays on the paper so if we want to infer once if we want to define our promote extent message we have to lights emendations in a lot of the core this
is my day what's so it's that in France for ordinary programs based on bring because it's it about published in 2 thousand and 7 and of my paper is to be inferred supplement weakness of types for of the program so it is based on it's in France I it's not passing running it is made up of and in our program granules we used out of I thought we used including all form of a critical of text to reproduce and that type of the object so ADV it works but there is also a big limitation that it cannot types some Luby nutrients so somebody butenes includes at at a so so work type system cannot give tied to much then we have KONGRA-GEL made it so we can give it up types to the B is object using structures updating while me for market because types so it is about good approximation of the semantics of Libby's types so I said that that and but it sets of taking mediation is dif defined by if that take has admitted what not so it is very good there could be forced out of its semantics so that the program is that type inference doesn't work with so if we choose and structures of data being we cannot in France the bottom of expects if we choose that based type in France began to we can infer the output of all this but we can note types some also the beach between so the next question is that ad do we really need a typed in France for review so we have the next idea of local taking finds so it is that we can burgeoning of that i've been friends so instead of in inferring everything the entire program only in fast at low and look at look look at women's rights and over what irritates and so if we use that from weakness of course in it in class types so who is lower than in France so programmers programmers should rights to of states so across types so we need some annotations into the programs but we don't have to write everything so a good thing as it is is a really integrated with existing wrong it's it's right maybe she prof prof recent reintroduce arrow partake in France and then we can think about stuff gonna last week they also have to look at inference so and this is an example of that this is our Luby program was no have annotations so 2 types check that this will be program that we need a complete that in France the words so no their type annotations idiots untyped what we need are competing in France so this is the opposite it is that free diagram of the so we have to half it's a range range ones and that I've annotations so so that we have to other states that Ms. Oates arguments Miss to the downside and we have to annotate pose a low-carbon ever types that sizable could whatever it's been teaching shit here what they integrate that and we also have to open the dates that that's also broke parameters and broke the Dember news and an important mark each up thickness of so we have to explicitly give that type publications so it is soaring so the major ways that protect inference so we need to give that have annotations for them is of from a dozen miss of the dentate spot in this example we don't have to be created in need of annotations in the locker by rose work at to using that blocks what so that table Roca whatever size is invited from its right-hand side so unable to size is addition so that a site atoms reads a title size is in so something like that so and we have something right and and erectus so we should try that structural subtyping and local in France so we know that the structure of fighting is it's enough to support so that is underscore duct-taping or we can use logarithmic inference to minimize the number of keys you have to show so there this this is a new similar to TypeScript because of structure subtitling on it also in France and that takes a look at the that type-checking difficulties now make this so instead of having ComBridge typing prior so we can use the logarithm inference we annotate some Luby cause using that the type annotations FIL but we don't
have to write any every types in your MIS of the pension so we have that it currently is bound then a creative object but we now began supports that taping semantics using structural subtyping so rest of that the difficulties it is referred to open it programming so what is the programming you know air it it is a program that modified said cross squatness of definitions during its institutions so that yeah metaprogramming primitives intervene grows defining mistletoe cross of 2 new so if we write if we liked result metaprogramming we can write set right return side so it's defined not passing graphs and defining an MIS of court name street and set science by you bros so using a programming primitives we can write on the left so we use that cast button using that method that we use that craft of the new method instead of the craft and that we use that defined method methods to defines that is that instead of this text and we can also use their instance about get to miss instead of that making that name opening of roads so so the programming is so popular so of used in Europe core so it's not special 1 so you write attribute we don't want to be that's that is a a program it's missiles to defined axis of missiles so it's in a program how about to record so it connected to the database and finds that Condit conditions and finally it defines a review it's by itself so it's metaprogramming having what belongs to also defined set of methods by itself how about me quite here I think that everyone I have used it for years so we can do something this if in some condition holds the quite yet so it stays it that the random number probably about ascetic path in the old days indication defines the deepness of but so a list if without timely play yeah this and explain it so this is thing do their open crassness something right the so we can have a condition surroundings across the commission so it's not that graph is defined when so and this is that discovered government a programming so there is that by its some of course so it's very difficult to identify their structure after tight structures the structure was a types without indicating the It's about in front of the cases that it's a is the singing but using servant programming needs and called because in this case was so so and 1 idea is to support just to give us the show support for to read it so if we find a attribute to be there in that crossed the Commission we see that it is hard to defining that using the we prostrate said it yeah the of court to his optics index maybe we can do that but why the sentence of is always of and so yes so intact detention passing grasp at bricks writes that it is defines a reader tribute but in part 2 days override in the object grass so it is it it yeah accessible distinguishable broken so and this is that linear programming difficulties and an hour I same days to solutions for these so the FastFind needs we stopped by objecting in steps carry so we can't take checked that during the execution instead of every singing in the choir execution so this is the Leary Corps paper it is published last year just in time instead expect checking for dinner crime it is by the promise of foster ardent and if I don't know which that lend and the promise of 4 so it's that changed heat you broke set their mind about will so his team continues almost 10 years forward that Libby's budgeting so it's or something work in this vein that it's it adds the interesting thing is it runs up static type checking during execution static type-checking during execution so it's a BIG dish cults that doesn't mean OK and the implementation is cauda something about and that is built on top of our ideas so you may know that it is that dynamic tight checking that type of up library for
so the and this is how does something about implementation tactics so and this is an example of that it's defined our in Minnesota so if we execute step programming will be it is no all I will be detected no every topic so we passed so if method and histamine and our forests so it goes to lose the if condition needs the forest and then exit food we would not be called so 10 no 1 type and I would happen but we just said just in time type-checking score common but so have a right is detected so it doesn't take chicks statutory but there during the the Qiutian of the program when it's a it's a Qiutian beaches on the beginning over the missile if it's type text it's called the so things that except food beef why here it is checked so it's they're usually just that ecstatic in in the nonstop fronting conscience so it goes down when setting on hole so I'm not so it's checks of both cases so it's tries to take the air type checks up so that in most cases and its tactics that exit who is most of the core and Bucchino was thus tuning doesn't have a full list of its then it is at a greater the interesting thing is that that type checking is dominant during xi execution so if we harbor of MIS of divination in just ring cross like this so if there is a Gaussian bits to define the fullness of obsess rain so it will be passed that I've checked by hopping about so yes so it it it has good points that it did take more a us in you need to this so it's expected to use to be used to run said you need to testing while and rich and this and that and sing you the rights that would make its distinct in that would make its testing you you you have a program called stat most of that missiles you're defining so 10 it chicks most the cases called your programs so this is much greater than writing is a Unisys for every branching of rights so even if we have out low branching cover it it find more errors the and for that it's and an e-mail opinion I don't like this approach so because that that that taking is depending on sat around and behavior so if you add your program legal ideas some library it is not a poet InterPro election so library at so it's that the have and you have some some is in your program makeup Naziruddin that's it is not available in predicting us systems so I want to go it's an excellent so to suppose that made of program and we want to ask program asked to give acetic structures so instead of that that checking the due to the inference that structural types the program out how at that it's so this is in part my Paktika courts steep I had our presentation in the last 2 to be guided September so it it's at gradual taking so is available in did have you can't write using its so sorry it is Leary experience payment the austere and it's not in the at so it have to give up pretty option to install so that's the idea of all the type checking who is that that definition fees bitten by another limited to run its so it is not extracted from site to be called so what
the this is an example of it's 2 points about conduct crust so it is that it has an initial rise nestled it has a name and keyword arguments and that they put all that name is storing it also has the main properties we dance ring so we write something like this we specify and so that the signature crosses you're defining your the programs every crosses you define your program you half to write that signature so this is began in that of the fire in steep and stuff tactical shown relying it is leery limited function the it's really limited expressiveness so it is to give that precise that keeping mission statutory result execution so no open Krosno condition hours Nordic y you know with the program so we can leads that the definition of 5 and understand followed that types defined press speed so with me
explaining how was that 2 can will be so we have that conduct cross type definition here and there we have some movie called to defines a convex so we did our type addition mechanism at but implements conduct it there's that the cross is the component do that the condition of a contact so if we find that implements annotation it takes it's defined it said crust defines all muscles defined in the signatures so it fast sticks their insurance missile these defined went out and it takes that name from a date hot air name barometer is defined in the insurance mess with 1 and finally it also to accept name method is defined 1 of all of its that type of that name missile this corrected the square for quick quick to be defined by no so this is a programming so we don't try to to bind to contact things some metaprogramming called it idiotic the dead so in this case the name is is not defined known for syntax falls and a method so that it cannot understand if that name is defined when up so do it is that program was responsibility that to those at an we I defined that name using results subjects and X so this is my dynamics and that's so if you know there will be this the QC program along it so it's also have their at with dynamic annotations because tested governed and that doesn't know holes and name method is defined so you can use another metaprogramming tectonic plates a missile of missing so instead of a guarantee that you can define anyway you want so and so the county is somebody programs cannot be typed static ORAU thinks the so this is an based in Briggs sample It's good points food nestled in 8 so in that the condition of the full method it defines who mess of a game so if you recall that fullness of fast it recounts numbers to be but it also devise new food medicine so the next time you flu it began at 3 instead of that condition so of course factory just did cannot gives their tied give and it's type for this kind of program but madam in my opinion for so probably maybe you don't write and the the program parameters what maybe you don't want your teammates do right program sensing this is the program those
in the 2 so and introduce that tactic as it is developed for this 10 years so the fast do is the parts to attempt to guess at focusing on that things that they rate objects and it tries to types but as of today some years it was a some defaults and we found that with 10 invited types to programs so we have to write some annotations for in the programs or what we can use that technique goalwards that look at that in France to to to to give that to tote how's that the program stacked and when it moves to the next stage that we focus on how metaprogramming can be supported so just in time static type checking for dynamic run it is Leary some paper but it's very interesting but I don't know it and breaks at the costly to acquire yes their programmers situation so I tried to develop my own and as a tactic careful of so it it's steeper height and it though I had a presentation inca because the so I introduced that
for their tickets through history context occurs over 10 years ago and to reactivity new tactic so and there's no grant region in this talk so death that hectic and voted is still an open problem so any man on Diaz doesn't have that as do we can do that 1 and how we can do that 1 it's impossible so there's no answer yet so in the if have state so you and we out what for this so thank you the we really
Loading...
Feedback

Timings

  684 ms - page object

Version

AV-Portal 3.13.0 (5c8e2efe74178fb46921415ac72371299d2e6b01)
hidden