Minimalistic typed Lua is here
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 | 490 | |
| Author | ||
| License | CC Attribution 2.0 Belgium: You are free to use, adapt and copy, distribute and transmit the work or content in adapted or unchanged form for any legal purpose as long as the work is attributed to the author in the manner specified by the author or licensor. | |
| Identifiers | 10.5446/46951 (DOI) | |
| Publisher | ||
| Release Date | ||
| Language |
Content Metadata
| Subject Area | ||
| Genre | ||
| Abstract |
|
FOSDEM 2020105 / 490
4
7
9
10
14
15
16
25
26
29
31
33
34
35
37
40
41
42
43
45
46
47
50
51
52
53
54
58
60
64
65
66
67
70
71
72
74
75
76
77
78
82
83
84
86
89
90
93
94
95
96
98
100
101
105
106
109
110
116
118
123
124
130
135
137
141
142
144
146
151
154
157
159
164
166
167
169
172
174
178
182
184
185
186
187
189
190
191
192
193
194
195
200
202
203
204
205
206
207
208
211
212
214
218
222
225
228
230
232
233
235
236
240
242
244
249
250
251
253
254
258
261
262
266
267
268
271
273
274
275
278
280
281
282
283
284
285
286
288
289
290
291
293
295
296
297
298
301
302
303
305
306
307
310
311
315
317
318
319
328
333
350
353
354
356
359
360
361
370
372
373
374
375
379
380
381
383
385
386
387
388
391
393
394
395
397
398
399
401
409
410
411
414
420
421
422
423
424
425
427
429
430
434
438
439
444
449
450
454
457
458
459
460
461
464
465
466
468
469
470
471
472
480
484
486
487
489
490
00:00
Multiplication signSoftware developerOpen sourceFreewareProjective planeSlide ruleType theorySoftwareDevice driverFormal languageData managementSoftware maintenanceSequelComputer animationLecture/Conference
01:09
String (computer science)CalculusType theoryVariable (mathematics)Numbering schemeScripting languageJava appletFormal languageImplementationFunction (mathematics)Formal languageCuboidRight angleProjective planeComplex (psychology)Formal grammarComputer programmingData structureProgramming languageDynamical systemType theoryInheritance (object-oriented programming)Disk read-and-write headWeb pageVariable (mathematics)Order (biology)DialectImplementationNumberCASE <Informatik>String (computer science)Fluid staticsForm (programming)Moment (mathematics)Scripting languageMultiplication signCompilerFunctional (mathematics)Process (computing)Lecture/ConferenceComputer animation
05:29
ImplementationLine (geometry)MereologyElectronic mailing listoutputComputer fileImplementationLibrary (computing)Physical lawSocket-SchnittstelleRoundness (object)Direction (geometry)Reverse engineeringSource codeLine (geometry)Single-precision floating-point formatCompilerWebsiteRight angleFunction (mathematics)Type theoryDirectory serviceStandard deviationFile systemComputer animation
06:41
ParsingBootingAbstract syntax treeStandard deviationLibrary (computing)Type theoryInsertion lossLibrary (computing)Computer fileSource codeMereologyPattern languageQuicksortParsingMultiplication signCodeRight angleRecursive descent parserType theoryStructural loadFunction (mathematics)Traverse (surveying)BootingParsingComputer animation
07:22
Asynchronous Transfer ModeFunction (mathematics)Local ringError messageString (computer science)Table (information)Type theoryBoolean algebraPoint (geometry)Inheritance (object-oriented programming)Interface (computing)CodeChecklistPrice indexVariable (mathematics)Computer configurationType theoryDynamical systemAsynchronous Transfer ModeComputer fileComputer programmingFunctional (mathematics)Formal languageDot productCodeSemiconductor memoryExtension (kinesiology)Different (Kate Ryan album)DataflowNumberError messageInheritance (object-oriented programming)Table (information)Physical systemEqualiser (mathematics)Turing testRight angleCompilerInterface (computing)Pointer (computer programming)Projective planeResultantPoint (geometry)Single-precision floating-point formatRow (database)InferencePattern languageVariable (mathematics)Programmer (hardware)Multiplication signData storage deviceKey (cryptography)Axiom of choiceMappingString (computer science)Declarative programmingException handlingOrder (biology)TypprüfungGeneric programmingTraffic reportingArray data structureHash functionData dictionaryComputer configurationElectronic mailing list10 (number)Data conversionPhysical lawObservational studyData structureMereologyCartesian coordinate system1 (number)Arithmetic meanChecklistObject (grammar)Value-added networkWebsiteAlpha (investment)TowerDivision (mathematics)Goodness of fitVideo gameMaxima and minimaCore dumpPay televisionSystem callComputer animation
17:04
Mathematical analysisDataflowComputer configurationType theoryTable (information)Projective planeMereologyPoint (geometry)Right angleComputer animation
17:35
ParsingMathematical analysisBootingAbstract syntax treeStandard deviationLibrary (computing)Type theoryFeedbackModul <Datentyp>InformationAsynchronous Transfer ModeVariable (mathematics)Point (geometry)DataflowMathematical analysisProjective planeLibrary (computing)Declarative programmingType theoryRight angleCompilerComputer programmingGraph coloringDisk read-and-write headLine (geometry)Forcing (mathematics)WordNeuroinformatikFeedbackFormal languageComputer animation
19:04
Network socketComputer fileFunction (mathematics)Operator overloadingComputer virusNumberLengthNumberException handlingValidity (statistics)Programmer (hardware)Disk read-and-write headType theoryLibrary (computing)Computer programmingFormal languageProgramming languageFunctional (mathematics)Right angleDressing (medical)Point (geometry)Table (information)Parameter (computer programming)Proof theoryMultiplication signComputer fileForm (programming)Graph coloringRow (database)2 (number)Position operatorOrder (biology)Different (Kate Ryan album)String (computer science)1 (number)Physical lawGame theoryExpressionStandard deviationCodeBookmark (World Wide Web)Green's functionAlpha (investment)Dot productLine (geometry)Array data structureTypprüfungCompilerInheritance (object-oriented programming)Polymorphism (materials science)MultiplicationPointer (computer programming)Computer animation
23:55
Function (mathematics)String (computer science)NumberType theoryAutonomous System (Internet)Type theoryComputer programmingFeedbackClosed setCartesian coordinate systemComputer animation
24:49
Row (database)Lecture/Conference
25:14
System programmingCASE <Informatik>Revision controlCompact spaceInformationPhysical lawRight angleVariable (mathematics)Single-precision floating-point formatInsertion lossSpeech synthesisMessage passingCodeType theoryMultiplication signGoodness of fitLibrary (computing)Lecture/Conference
27:06
Open sourcePoint cloudFacebook
Transcript: English(auto-generated)
00:06
Well, I think we're past time so let's get started. Hi everyone, I'm Hisham and I've been involved with Lua for a long time and I'm the maintainer of Lua Rocks, the Lua package manager, and also I'm involved with other free software projects
00:25
Like mainly Htop. I work at Kong where we develop also an open source project, Kong We're hiring by the way, are we? Yes, we are So Yeah, so we are here to talk about Lua and types and minimalism
00:41
So this talk is actually a sequel Because last year I was here at what was then called the minimalistic languages developer room to talk about minimalism versus types so it was about like the journey of you know the difficulties between Lua and the idea of types and I hinted in the end about some further development. So my last slide was actually like to be continued so
01:07
here I am and It's very fortunate that the the scope of the dev room was expanded this year And it's now called minimalistic experimental and emerging languages because what I'm going to be talking about today Hopefully ticks all boxes
01:23
Alright, so let's get started I'm gonna start with a quick recap of what I talked about last year in case you weren't here. So We're gonna be talking about adding types to languages essentially every Like modern practical programming languages has types even though we called some of them like typed and not typed untyped
01:43
like they do have types because Like strings and numbers there are different things even if you don't have to like Name your variables because essentially what we're talking about is having dynamically typed languages where values have types but variables don't so any variable can accept any value and Here are a bunch of examples and the statically typed languages where values have types
02:04
But and variables also have types, right? So only things that match can be assigned to each other right and in recent years has have been a lot of grammar to avoid mistakes So there has been a bunch of projects related to that like Python has mypy and recently pytype, Ruby has Sorbet
02:27
Typescript has become super popular for for JavaScript and and so on But what about Lua? So Last year I talked about the challenges involved in bringing types to Lua, which is such a minimalistic tiny language
02:44
Right there have been projects such as title lock and Typed Lua, which was an academic project, right, but We never really got there So what's the what's the main challenge especially in a minimalistic language?
03:01
Well adding types or really adding anything to a language makes it larger, right? So it makes it larger both conceptually and also in implementation Last year I kind of argued that Conceptually the complexity when you're writing your programs, well not in the language itself But in your programs, the complexity of types are already there, right? If you you're maybe using a dynamically typed language
03:26
But you're constructing complex data structures And well you have to put the right kinds of data in the right places or else your program is not correct So the idea of all of the types, they are already there. Your program is as complex as you know
03:44
Its purpose, though The implementation one is kind of hard to counter argue It's really a thing if you're gonna be adding more stuff, more features, your implementation is gonna get more complex So here's the conundrum like if the language grows too much it doesn't feel like Lua anymore
04:04
You know if there's a tons of concepts, you know, and it starts turning in slowly turning into C++, right? But if we keep the implementation and everything super minimalistic and simplistic Then it will stop you from doing all of the powerful things that you can do with Lua because it's like super dynamic and
04:25
And very like freeform, you know as dynamic languages are So if it's too simple, then it's too restrictive and it doesn't feel like Lua anymore either right So But we want both. We want a small language that fits in your head And it's like how I like to describe Lua and why I like it
04:43
Like the full reference manual is this like small single page that you can kind of read in one go and Understand everything there is to understand about the language But also I want a type checker that at least like catches when you make a silly typo or something like that, right? I want the practical benefits of You know doing like pair programming with the compiler, you know in order to catch my mistakes
05:06
So the challenge really is to find the sweet spot between minimalism and functionality, you know, this is this is What this is about? So I'm gonna be talking about TL. I'm I'm in search of a better name still, right?
05:20
So this is like the temporary name that I still had last year I'm still haven't found a better name yet, which is a typed dialect of of Lua So it's let's talk about the minimalism part so the implementation tries to be very minimal in the Lua spirit Lua itself if you download from the Lua.org website you get like a
05:41
300k tarball which is For which you can build a full VM right and it's written in pure standard C with no dependencies That means only standard C libraries that means no sockets, you know, it doesn't come with batteries included That even means no directory traversal, right? If you want to do file system manipulation have to get an extra library
06:01
So TL is in that same vein. So it's a single file. It's currently as like less than 5,000 lines With blank lines and comments and everything, right? So it's one pure Lua file with also with no dependencies, right? Actually, it's a pure TL file, which is
06:22
Transpiled compiled is the source-to-source compiled into into Lua, right? It is a it is a source-to-source Compiler or as people nowadays call it transpiler. So it's essentially the output. It's essentially your input without the types, right?
06:42
So this is the breakdown of the source code on to which like every every part is You know, so we have a lexer We have a little pretty printer that I used to debug the lexer a parser written by hand like recursive descent parser Probably could be smaller if I had like used an external dependency to use a parser generator But I wanted to keep everything self-contained
07:02
Right, so there's like a small AST traversal that implements a visitor pattern which I use for the pretty printer that dumps the output file Then the type checker, which is the bulk of the thing Definition of types for just Lua's tender library, which is still incomplete, you know And a small loader that allows you to load TL files with require from Lua code
07:23
So the idea of no dependency is that you can take the generated TL that Lua drop it in your Lua project and off you go like you can require You can require TL files and mix them with your with your Lua files Of course this has pros and cons as I said, but
07:42
For now, this is this is what I'm going with So there's also a TL It's not like one single file because the bulk of it for running it in your project is one single file But there's also like a little command line TL file, which you can use to check a TL file so it's gonna look at your TL file, see if the types match and if your program is gonna go to the
08:03
good place or the bad place and Then there's a gen file which strips the types generates a Lua file, but does not type check it so even if your type program has type errors, you can still convert that to Lua and run it and TL run which does all things like it checks the file and if it passes it
08:24
generates the Lua file in memory and just runs it straight with your Lua VM so So that the experience becomes self-contained It has two modes of execution Which is depending on that like the extension of your file So dot TL would make it like strict mode and dot Lua would be more of a lax code
08:43
Lax mode essentially for interacting for having like Lua programs that interact with TL files So the difference would be something like this if you write a Lua If you write code like this in Lua, which is this is this is fine, but if you are in strict mode then
09:00
That means like you haven't annotated any return types, right? So that function is annotated so that it doesn't return anything and we don't do advanced like in the minimal spirit We don't do advanced Flow inference, right? So in strict mode this would be an error because it says like F of X does not return anything and
09:21
You're trying to get its return value here when you're when you're calling it, right? But that would be accepted in the Lua mode because in the Lua mode the return type of that function is Unknown which is the type of everything that it's not annotated So if you do that then strict mode is happy and it knows oh you're gonna return a number and everything's fine
09:42
in a TL file So TL reports errors and unknowns separately so when you start to convert your Lua file into a TL file It's not that you're gonna get like, you know, hundreds or thousands of errors You're gonna get hundreds or thousands of unknowns, right? It says it will look at it and it will decide that okay I don't know anything about like there's no type annotations anywhere. I don't know basically anything about this file
10:04
so as you start to Annotate the types then the values of the type start to propagate things start to be left become less unknown Right and eventually it might spot errors and then this is how you you gradually convert your your program
10:20
So the type checker really as we have seen it is it is the bulk of the compiler right and It does It does very minimal It does just like local inference if you initialize a variable like local local x equals 0 then it knows it is a number you don't have to type in like the types every time
10:44
Depending like it can take like the return For example in in that example, it knows that f of x returns a number. So here's D is a number as well and And it also does some very very naive Flow inferencing like for things like empty tables like that. So that KS you seem like it wasn't
11:06
it it wasn't inferred to become the string the first time it the first time it was used and In table in table in search so in the end that that works and it knows it to returns an array of string And and if there is an error in that and you use it in consistently it will report an error and it will say
11:24
Well, I was expecting an array string because I inferred it like at that spot, right? It records for anything that's inferred that records the provenance and where it was inferred so that you can see Okay, that's why you guessed it wrong, right? So the main thing about the type checker and the bulk of its work is determining the types of tables
11:43
That's usually the most complicated thing about type checking in Lua because a table is such a general type That's the main thing about Lua. There's no separate Like arrays and dictionaries and or like lists and hashes. Everything is a table and a table can do everything, right? So what is a Lua table in practice when we are
12:01
Typing it we have to determine that and so essentially tables in TL can be either Maps, they are declared like this, you know, so like keys are strings and values are boolean Arrays declared like this. They're essentially the same as maps with number keys But like for better error reporting and like registering programmer intent, I kept it as a separate type
12:26
Then records, which is specified by name. So a record is a table that has you know keys with names An array record which is like a record in an array all in one Which is a very common Lua pattern in which people like store things and name keys
12:43
But also when the number keys start an array with that You know kind of like C programmers do when they do a struct and then they put an array in the end so it's a very common Lua pattern and I had kind of had to support it from day one and Sometimes people do array maps as well, but I have not implemented that yet I'm sure people will ask about it like very soon as they as more people start using it
13:04
But I just didn't have the need so I was going with like the very minimum that I needed because my very first Project which I talked about last year was trying to bootstrap it Like now we've got to the point where it did like by the time I ended my talk I remember I had like 300 or something type errors and but now the thing actually type checked itself
13:23
So I mentioned that that records are declared by name So that was a big design choice to keep things minimalistic to keep things small, right? There was a choice of making like type systems can be able to can be either like nominal or structural and I chose with nominal because
13:41
Just makes everything simpler essentially like to compare if things match you just check the names if you know If the names are the same then it's fine, right? So so you can declare You can declare record types like this and then you use them by name So for now, there is no inheritance or any kind of like interfaces or traits and things like that
14:05
So this is this is one limitation and but I think eventually some of something of that kind will have to be added But Then as I was as I was writing and typing the as I was typing the compiler itself the code of the compiler itself
14:21
I started writing it in Lua because TL did not exist, right? So I wrote it to the point that it could start Checking itself and then I started annotating the types, right? And then I realized that well with when a programming dynamic language with dynamic types It's trivial to generate very generic code, right?
14:42
So I Realized that I actually needed Generics in order to write the code like the in order to translate the code that I had already written in Lua Right, so I added that with with the like a backtick there and as a slight nod to OCaml the quality types, so
15:01
So this is the same code as that one, right? But instead of like Of any kind because I either had two choices when I got to the point that I was was translating it was typing that code like either I would have to add inheritance to the language and Then readjust all my Lua code to make it more object-oriented or I could keep it the way I originally programmed in Lua
15:25
But then I had to have generic types. So so I added type variables like that. They only check for equality They're not very smart, you know, they're that's it's a very minimal support That's mostly useful for things like this which are general containers of things But it works quite well
15:41
So I was able to use like the divisitor for different things like preprinting and and type checking and all of that Right. So this was a important example of prioritizing the practical needs over going through a feature checklist, right? Okay, I have records. I need inheritance or I need traits or I need this or I need that, right? It was going through what I needed
16:00
So yeah types, now what? Then I realized that once I had the types and I kept working on it Like I didn't like all of those silly typo errors were gone because they were immediately caught by the compiler And then all I had left were tons of tons of like it seemed that every error that I got was related to nil Like what Turing Award winner Tony Hoare called his billion-dollar mistake, right? Adding nil references
16:26
so yeah, so we still have nils and as in Lua any variable of any type may be a nil and How do you solve that? Well, in many statically typed languages you have option types, right? Maybe result in Rust
16:43
But for Lua that would be very tricky because essentially like every table access can return a nil So that means that every table access returns an option type and you have to like Destructure that and check and like that that really wouldn't make sense Right, it would take But what if we can have the compiler detect it, you know, that would be smart and that would be fun to do
17:04
So Yeah So I started so this is the experimental part that I started going down this rabbit hole and doing something that I promised myself that I would not do which would be to start doing researchy type things in the project, right? So I started writing some flow analysis to see if I could detect like the need for optional type detection
17:23
Or if you can derive that that table access is never nil and all of that, right? So I started writing writing writing and get myself totally sidetracked into that fun Project of dealing with nils, right? So to the point that I started to add the flow analysis and it started growing growing growing right and
17:44
But essentially I was dug out by off the rabbit hole right and and by the FOSM deadline because I wanted to have something to show here and Most importantly by user feedback, right? And I want to shout out to Patrick who's
18:02
Been active in the github project over there posting issues and just just merged his first a PR into the project So someone else was actually trying to use it and they were hitting like the things that were Actually missing when you want to get really work done
18:20
Right that I didn't hit when I was writing the compiler because that was just one program Right. So it's interesting to take a look and what were those issues and how you know How that goes So the the first of them five minutes, all right, we are in the tail end so The first one was that was that okay. I must I want to use a I want to write a TL program
18:44
Of course, I'm gonna have to use little libraries because you know, there are no TL libraries So, how do I add the types to existing Lua? Libraries so I can so I can use them Right. So will it support something equivalent to typescript declaration files? So that obviously that that was like sorely needed if you wanted to do get anything done with the language, right?
19:05
So, yeah, so I got ahead and did it like it was a very quick like ten line thing to just add that and Have it. Okay. So when we're type checking I just blatantly copied the the typescripts Standard for that which is dot D dot TS
19:20
So essentially when type checking before trying to require like the TL file or a Lua file Just try to when type checking try to use the Definition file instead to read the types from with even though there the functions are not there But when running then you actually use the real code The the next thing he asked for so he does okay
19:42
I have a definition file so I can start writing a definition file He started writing a definition file for the love 2d library for writing Lua games, right? So he got to a point there said Some functions in love have multiple overloads such as this one but now it seems that you know TL kind of ignores the previous ones and just keeps the last and
20:01
That's what really what the compiler was doing, but he needed both both definitions So Turns out that Lua does not have function overloading like that But it's super common to fake it like love actually has one definition of that function, but the types are dynamic So it just does some if type of the first argument equals this and that you know
20:21
Do this otherwise do that and it feels like the user has two different functions with the same name, right? The funny thing was that I had cheated myself and for the definition of the standard library I had added Polymorphic functions like that, but I did not expose the type for
20:41
In the language because TypeScript does something complicated as intersection types for that But then I decided to just expose that with the exact syntax That he guessed said okay, if you have multiple entries of function types in a record, you know They are just mushed together as a as a ad hoc polymorphic function
21:02
But then there was like the last one which is a fun one It's the last thing we're going to talk about here this challenge. How do you type that table over there? Which is an array of things. Well the the love Documentation says that it's okay It's a table containing colors of the strings and that for color one string one color two string two and each color is in the
21:22
form red green blue and alpha Right. What's the type of this, right? So what's the type of color text like that depends on how precise you want to be about it, right? The first type could be any which is a type that TL has that says like I don't know anything about this The or you could say well, actually it's a table which is more precise
21:43
You can pass it. You cannot pass it a number, but don't know anything about a table We could say something that it's an array of something Right because what the user asked you why he asked for union types, right? What he wanted to write was this. I want an array of strings or arrays of numbers, right, but
22:02
TL does not support that so the best that TL can do at this point is number three But this if you can think about it like this accepts a lot of invalid tables as well, right? You can put the colors and the names in the wrong order and this would still accept it It would not be a type error. So essentially what you would want would be something like this, right? So in the in the odd ones you would have numbers and in the even ones you have strings like, you know
22:24
Does your favorite programming language like can your favorite programming language express this one, right? But this still accepts invalid tables, right? Because actually what you want is in the odd ones. You want a raise of numbers of length four
22:41
Right, but this still accepts invalid tables right because Well, the the length of the full array has to be even because you have to have pairs of colors and right but this still accepts invalid things because the numbers in there have to be between 0 and 1
23:03
right and Looks like this is now the actual real type that lives in the programmer head when like the dynamic programmer when they wrote about it when they designed the function This is the type that really had in their heads if they even if you don't realize it, right? But this still accepts invalid tables because this is not accounting for nil
23:24
right, so Yeah, so as you can see here like each each each type here Expands on it saying like something more precise about the idea of the definition, right? You would have you would need to have like something like Idris dependently typed languages where essentially you have to
23:40
Define like a proof of you know, and you could have like number eight, right? There are languages that can do that right, but they're like mostly research languages now TL could do number three, but if you have like the statically typed mindset you would probably write like this instead the definition of your function, right and
24:00
Then this works today in TL and would give you the same guarantee as number seven right, so Well, so the conclusion is like typed in Lua did they deliver? Is it actually easier to maintain application working in TL? And my answer is yes because I never felt this fast programming Lua like
24:22
Responding to the user's feedback and like refactoring things and adding features and all of that, right? So So in closing Well, TL is here I just tagged the very first 0.1.0 like, you know, super early early release Can run it lorox install TL. I'm still looking for a better name. Suggestions are more than welcome
24:45
And well, Lua and types, so join us. Thank you
25:00
All right, okay question here Generic records. Yes, it does Have them I'm 95% sure
25:21
But yeah, yes, yes, yes it does Yes, it does and it's it's it's very naive and how it matches the variables It just like it goes very top to bottom It does a single pass and everything has to be like the first the first time the variable is used That's the type it gets and it works well for simple cases
25:40
Any other question while next one sets up here Yeah, good question in which for which version of Lua does this work right now the code is Right now the code it generates it's it's it's
26:01
Right now the code that it generates it supports like 5.1 and up And it can use Compat 5.3 library in the in the back to to give better compatibility This is kind of still an open question, but I probably want to support the latest Lua and the latest JIT, right? So now a question are there plans to take advantage of type annotation to generate better codes?
26:52
There you go You know, we're gonna switch speakers and yeah, well happy happy to talk about this offline. Thanks again