Minimalism versus Types

Video in TIB AV-Portal: Minimalism versus Types

Formal Metadata

Title
Minimalism versus Types
Subtitle
An experience report on the development of Titan, a statically-typed Lua-like language
Title of Series
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
Publisher
Release Date
2019
Language
English

Content Metadata

Subject Area
Abstract
We love minimalistic languages because they let us do so much with so little. But when we start doing a lot with them, often we start yearning for types to help us make sense of it all. Adding types to a minimalistic language (well, adding anything!) makes it larger. Is this worth the price? Is a rich type system antithetical to minimalism? Let's find out! This talk is based on the experiences in the development process of Titan, a statically-typed Lua-like language.
Loading...
Programming language Multiplication sign Maxima and minima Software maintenance Data type Formal language Identity management Data type
Web page Programming language Constructor (object-oriented programming) Right angle Maxima and minima Mereology Disk read-and-write head Data type Formal language Library (computing)
Programming language Execution unit Matching (graph theory) Feedback Similarity (geometry) Bit Mereology Perspective (visual) Entire function Computer programming Formal language Compiler Goodness of fit Quicksort Data type
NP-hard Presentation of a group Group action Run time (program lifecycle phase) Java applet Code Multiplication sign Execution unit 1 (number) Numbering scheme Calculus Mereology Computer programming Variable (mathematics) Formal language Programmer (hardware) Different (Kate Ryan album) Computer configuration Data conversion Physical system Programming language Meta element Metaprogrammierung Bit Maxima and minima Numbering scheme Variable (mathematics) Category of being Right angle Heuristic Data type Erlang distribution Web page Point (geometry) Implementation Assembly language Maxima and minima Branch (computer science) Modeling language Theory Field (computer science) Number Hypothesis Prototype Term (mathematics) String (computer science) Integer Data structure Data type Assembly language Inheritance (object-oriented programming) Physical law Projective plane Java applet Personal digital assistant String (computer science) Library (computing)
Programming language Numbering scheme Set (mathematics) Maxima and minima Data type Rule of inference Formal language Formal language Physical system Data type
Rule of inference Programming language Source code Computer program Interactive television Disk read-and-write head Rule of inference Code Computer programming Formal language Hypothesis Data type Physical system Physical system
Programming language Complex (psychology) Multiplication Functional (mathematics) State of matter Java applet Infinity Line (geometry) Numbering scheme Variable (mathematics) Rule of inference Variable (mathematics) Category of being Tower Table (information) Data type Error message Erlang distribution Typprüfung Physical system Data type
Programming language Dataflow Functional (mathematics) Multiplication sign Java applet Parameter (computer programming) Numbering scheme Disk read-and-write head Variable (mathematics) Formal language Proof theory Personal digital assistant String (computer science) Function (mathematics) String (computer science) Right angle Integer Table (information) Integer Data type Erlang distribution Reading (process) Physical system Data type
Dataflow Correspondence (mathematics) Multiplication sign Disk read-and-write head Computer programming Formal language Number Component-based software engineering String (computer science) Integer Differential equation Local ring Error message Physical system Data type Information Correspondence (mathematics) Structural load Mathematical analysis Variable (mathematics) Process (computing) Rekursiv aufzählbare Menge Logic String (computer science) Function (mathematics) Right angle Table (information) Integer Data type
Personal digital assistant String (computer science) Mathematical analysis Right angle Primitive (album) Integer Object (grammar) Data structure Table (information) Local ring Data type Error message
Programming language Data dictionary Mapping Texture mapping Multiplication sign Expression Boom (sailing) Data dictionary Complete metric space Field (computer science) Formal language Array data structure Array data structure Object (grammar) String (computer science) String (computer science) Right angle Object (grammar) Drum memory Data type
Point (geometry) Complex (psychology) Mapping Java applet Data storage device Electronic mailing list Sheaf (mathematics) Field (computer science) Formal language Word Film editing Different (Kate Ryan album) Right angle Object (grammar) Table (information) Data type
Axiom of choice Functional (mathematics) Expression 1 (number) Computer programming Software bug Usability 2 (number) Revision control Pointer (computer programming) Film editing Programmer (hardware) Computer configuration Logic String (computer science) Integer Right angle Game theory Data type Error message Physical system Data type
Open source Code Maxima and minima Set (mathematics) Maxima and minima Turtle graphics Computer programming Error message Function (mathematics) Spacetime Arithmetic progression Data type Typprüfung Spacetime
all right so let's get started I am
I'm his Chum I work at Kong and I'm also
a maintainer of Lorex the package manager for the Lua programming language I've been involved with Lua since 2005 or so so it's been working with Lua for a long time and I'm here to talk about minimalism vs types and the long journey
with the about the hard relationship between like a minimalistic language like Lua and a desire for types so minimalism well I love minimalism as all of us here in this room probably do and once someone asked me like what do I like the most about programming when Lua and the answer that I gave like right off the bat was that well Lua fits in my head like I know I feel like I know the entire language right it's it's like the whole reference manual is like this one web page that you can read top to bottom and like there's no like corners of the language that I feel that I don't know it's just like in this it's a very gratifying since the sensation like being able to work in a language like that like as opposed to two huge languages where there's always like some kind of constructs or part of the
standard library that you have never touched so so like this is a classic
example of like a huge language versus like small language and like for a reference like the entire Lua reference manual is about the size of JavaScript
the good parts so it's and the language is the size of the languages and the size of their good and bad parts also kind of match hopefully like that well it's actually older than JavaScript but but but yeah like it's it's in many senses are simple it's similar and some people who are thinking of the other side of JavaScript they get surprised that no there are nothing alike but if you if you focus on the good parts of JavaScript then there rising Alya like so types I also love types and one thing that I'd like to say is that programming with types feels like pair programming with the computer like like you you program a little bit and then the compiler comes and say well well you you missed like you made a type over here something in something like that or all you cannot really pass this to that and all of that so so you get that you get this nice feedback loop that's different than running the program and seeing if it is seen if it crashes right and so this is like this is my interesting of types form they're very practical perspective as a practitioner as a programmer like and not just a theoretical like as a like programming language academic sort of interest so before we dive into types
just to let's just get our terminology on the same page like when we when people often talk talk about type languages and untyped languages and so the more accurate terminology would be like when you talk about untyped you mean know types at all so that would be like assembly everything is a byte right and those are not usually like the types of languages that like the kinds of languages that we care and for all the other ones like there are types like types exists so string a number of different things automatic questions can make this a bit confusing so said oh no it's not typed because I can do like string one plus two and I get a number so now it's actually like it's just doing an implicit converse conversion they are actually different things like brass presentation he mentioned that all originally in TCL everything was really a string and then now everything is representable string even though there really are different things so like modern TCL has types like all of the other model languages do so people in in the few in in the theory field they say like you shouldn't you shouldn't even talk about untyped if you just talk about unit types it because when you don't have time to really have one type like the type of everything so the distinction that we usually care when we're talking about this language is typed or not like when we formally say that is that whether it's dynamically typed or stacked statically typed so dynamically typed in a nutshell means that values have types but variables don't so you can move values that have it's around and like and they fit any variable so languages that fall into this category are like low esteem airline Python Ruby and so and so on all of those like all of this typically the ones that we call scripting languages and some that we don't but that's it and statically typed means that values have types and variables also have types so if you have an integer and you want to put in this variable this variable better be of the integer type because otherwise it will not accept it so like C Java go see sharp rust haskell like all of these other are step checker instead to run before like run time that tells you if your types are okay so for the purpose of this presentation we will totally avoid these terms like strongly
typed or weakly typed because they are very confusing and like everyone seems to have like a different definition of what those mean and the better distinction is really dynamic or static right so so this is what we care about but we also care about minimalism and apparently our all of our favorite minimalistic languages all fall you know in the first group like there's Luwin scheme and like all the only wants to see also there right so what gives like what we happens when we put minimalism and types together right so let me go through a brief history of the efforts for typing Lua so back in law workshop 2013 Fabian flirter presented tidal walk which was based on meta Lua his Lua meta programming library where he attempted to do like gradual typing of Lua programs you could you could partially add type annotations that would verify them and all of that in his presentation like the like the main point of his presentation was that we all left like scared off the prospects of how hard that problem was because he started like showing like how in the simple cases this and this work doesn't and then it starts getting Messier and Messier and Messier because once you start to capture the way that that blue programmers deal with their data structures right he started to have to apply heuristics and things like that so is that scratcher had to say well wait my type checker is gonna be running heuristics on the code right so because when you think of a type checker you kind of want some certainty and and in the end like it seems to be like a a real a really tough problem in other laughs tough problems is what research is made of so around that time under damn Idol was was working with Lua and types and two years after that he presented his PhD dissertation on that was called typed Lua and an optional type system for for Lua he worked hard on many of those complicated problems and he came up with a super complicated type system that had like many many pages full of little Greek letters in the thesis as he just as he tried to make sense of the whole thing and he made an implementation that sound github and that implementation is a nice prototype of all those ideas but really it's not ready for primetime in a sense that you can't really feed real-world programs in it and like try to use it as a day-to-day tool because like the type checker is just too strict it complains about like lots of lots of things that you as a little programmer said now this is right you know but the the type checker just doesn't understand and it is a super complicated one so I got involved back then I was doing my own PhD at the lab like it's completely unrelated subject but i guarante along with the people there and so we decided to start kind of a side project on that and two years later around 2017 we start a project called titan' that would be a statically typed language that would be like Lua like but not try to type Lua but create a new language that will be selling the type that will be somewhat like Lua and designed to interact with Lua and this is still an ongoing project and it kind of shows that we clearly like at that point we kind of gave up on trying to type Lua and I said like just let's just do something else and and really Titan tries to fit more as when you're programming like in that part see part Lua like embedded language type of thing Titan would be more suitable for replacing the C parts rather than the Lua part so it's not really the same thing and at the same time there's like super hard research questions and on how to go about this and like some of us were approaching it from a very practical standpoint some of us were pushing from a theoretical standpoint so at one point the project split off and like the research branch of it is the Pauline project in which they're really going like data structure by data structure from first principles and doing the research on that right so so yet here we are 2019 and we still don't have a type checker for Lua we don't have a way of like after that many years and and so many people like putting efforts on all that we don't have a way to use Lua and types together so what gives why is it so hard alright so I did some soul searching and thinking about the whole thing and want
to share like my my thoughts about it so our first first stab of that at that question like when you think about it like and we are here talking about minimalistic languages and it starts talking about types types types in it and how everything is complicated and from your own history experience dealing with typed languages and you think about like I don't know Haskell or rust or C++ you know like languages that has huge complicated type systems you start thinking oh they ended up being complicated languages because the types mess up everything like with the minimalism you know they like once you add like the types in the whole enchilada with it you know the language is no longer minimalistic so maybe like so types make our tiny languages complicated like is that the problem all right
my conclusion is that the problem is kind of the opposite and this can be a little surprising but when we think about like our little dynamically typed languages like Lua and scheme and like your favorite one you might realize after you look at it for a while that they actually have huge type systems and very complicated type systems and you go like what yeah yes so if you think about the type system as being well the set of rules that describe what are the valid
interaction of values in correct programs which are the things that a type checker checks right so essentially the type checker for those languages it's in your head like you are the type checker but but if you take like the C language and it has a type checker implemented inside GCC you can look at the source code and you can see this is a type checker and this is what it does those are the rules right so let's open our heads and look at the type checkers
that we have inside our heads for Lua what are the rules in there you know like how complicated like if you were to write it in Greek letters in a PhD thesis what Wow what would that type system look like for Lua codes that we actually write nowadays with our tiny Lu a language that fits in a you know and a 200k Qatar Bowl no so if you are the type checker
what type system error checking no cuz this is the kind of work you do like you do like we have multiple returns and Luo you do I'll get coordinates for those two values and you realize like you give a type error to yourself and say oh I can do that because yesterday I changed that function from returning two things to returning a table so so that line on the top is not gonna work this is the kind of doing that you're doing you know ahead that's why I mean by you are the type checker right so what are you checking what are those rules well now we have to go to the state of the art of sight systems right because I was
talking about dynamically typed languages so sorry mo statically typed language but within the realm of statically typed typed languages there are dependently type languages dependently type languages in like-new like in in the practical sense category of languages in which values have types variables have types but types have values and types have types right and and since well since types of values and values of types right you get into an endless infinite tower of complexity there and now and there's a few examples
of languages out there like Idris Agda there are not that many yet like people always say like the same three and then the third one is is actually like a proof assistant like you know the the from India right so really but this is the kind of type system that you have in your head when you're working with a dynamically typed language right you have like a nice function f a and B what are the types of a and B you know a is an integer and B is well if a is less than 200 say 256 then B is a string otherwise B is an array of strings you know when we have when we programming with dynamically typed languages we do that kind of stuff all the time without like read even realizing that we are creating these complex types that have like depend that the definition of the type has a dependency that's why it's called dependent types right on another value right so just pause for a second
and imagine like how hard would be for you to write a type checker that would be able to check that you know like you would have to go through the flow of every like possible path that leads to the first argument and determined that the integer that was evaluated could possibly ever be like less or more than 256 and then if you got a table you have
to you know prove that you know yes but if but once we have a dynamic language you do come up with those things because essentially the dynamically typed language since it imposes no restrictions it lets you think those thoughts right so but when you're doing
the work in your head like it's kind of like it's not that hard you don't actually do like the flow analysis of the entire program in your head every time because suppose you have those variable variables here red green and blue in there and there and you know there are all integers right you know that oh those if you see something like this and you know like okay so these are RGB components they go from 0 to 255 and then I'm I'm passing an RGB component there with an array and that's not going to work because I expect like those numbers to be within the range and so I named B strings and not a race so that so there's probably an error here right but if the type checker had the information that red it's only ever between 0 to 255 you had to specify that in the type right or then the type checker would have an easier job would be actually able to do that right but it won't once you have the idea of a type system that has like all of arithmetic in it right and by I mean like a type system that encompasses our Atlantic's it mean like by the curry howard corresponds it means like every type system corresponds to a kind of logic right so I first ordered a large X second order logic you know and and and those things right so and by the way since the 50s we know that arithmetic says proven undecidable in logic so if you can have a type system at a checker that knows all of our if metics so yeah so we kind of do those things all the time when we're programming here like for example you do something like this like load values into a table you give them ok and an error if not okay then well the type of
error is like it's dependent on the type of okay like if it's a string if ok is false right or if it's nil right and then what's the type of tea you know when you get there T of one right well it might have failed in between you know and all
those kinds of things like the floor analysis get can't could get really complicated and when you get to that like in a case like Lua where the table is the only structure type so when we say like everything's a table like apart from the primitives you know strings and integers and all that it means that a table is anything so a table it can't be an array it can be in dictionary and be a struct can be an object you give me a
dictionary mapping objects to strings or arrays depending on whether the field of the key object is true or false you know and without realizing you start creating the super complex types you know you can
you start creating those super complex structures that if you were to type them those would be the types that they would have to have so it comes to a matter of expressiveness right and what I mean like expressiveness in a programming language like how expressible it is I don't I don't mean like really what language can express because you know kind of but turing completeness you know that's oh they're all the same blah blah blah but really it's like how can you express it right so in that time in that sense the dynamically typed language is super expressive but it's super expressed in the same way that a blank sheet of paper is now the paper accepts everything you know the dynamically typed language accepts everything and well it goes boom and you know if you do something wrong that Bron time all the other hand the type checker works both for good like oh thank you for catching my silly typos and for bad like and you know like I know that this use of the variable is safe here why are you complaining about this right so essentially the expressiveness is like
the feel of a language like regardless of the look right so and in Lua you can have something like this like a table that stores like named fields like and also serve as an array like two like both of them right if I take like if I do like a small transpiler that's like took all of the keywords from Java and turn them into Lua like it was it will still feel like blue all right
so okay so I'm just going to jump ahead just going so here for the final section like hope so in the end like how much of the language do you change like do you make this illegal because like it's either a map or an array right because you could you can still represent something like that like in Java right you just make an object that has like the name field and then a list you know put one inside the other so it's like you have to think those thoughts like in a different way right so so the the final point is if you want to make it feel like lua then the type checker is super complex you want it feel like 100% like lower than the type checker is impossible right because you end up with undecidable things and if you want to actually finish writing your type checker you have to make cuts somewhere but not in the word somewhere so two
options on where to make your cuts well first you can cut on program expressiveness as I said like you don't allow them to mix an array in the table and say like Oh in my typed version you have to do something like that you know items right or and maybe say oh I cannot make something that's like sometimes a nil sometimes a string and a key instead of doing return X on Y and return nil and error in the same function if I want to use those two things in the same function then we have to do return x and y which is always like an integer or an optional integer and the third one would be like the next free available entry would have to be like the error message like those those are simple those ones are fixable right but I'm just gaming them as simple examples you know otherwise you can cut on the correctness of the type checker so you go from like the promise that every problem that the type checker accepts has correct types - something like oh if I complain then it's probably like wrong but if I don't
you know if I if I don't complain I'll give you no guarantee and still it's hard because you made your the equivalent logic of your types of your type checker it's an unsound logic and when you at once you add unsound logic you can start like proving absurd things and when you go back to the type checker it means that it will behave in very weird ways if you're not careful and probably even if you are so the more sophisticated type system the deep you are in research territory everyone has felt like who's ever tired try to deal with that ended up dealing with this so is that all lost like in the final minutes here well typescript has proven to be like a successful like attempt in the industry I'm doing that and essentially their choice was to go for usability above all else it means that the type system is intentionally unsound and this is not just a technical thing if you go there to their bug tracker there's lots of bugs that are close it by design by design by design it's not meant to detect that failure right so what about Lua I probably have like 30 seconds and just to give a glimpse of hope well I've
been working on exploring this design space and playing with it so I decided to try to write a minimalistic type checker love Lua in Lua but just like what's the minimum set of features so that it could type check itself that will be like enough to be like a real program and not there yet well when I try to run it like on itself it currently feels with 384 type errors a week ago it was a lot more so that's progress the thing is that once you start fixing it like you fix one thing that fixes 100 errors and but now it's like you know it's like Achilles in the turtle but yeah the idea is to do something Lua like it's here because even if then though it's not finished it wouldn't be fossum if you know I'll talk about code and it's not open source
so in closing yeah the story will continue and thank you [Applause]
Loading...
Feedback

Timings

  329 ms - page object

Version

AV-Portal 3.20.2 (36f6df173ce4850b467c9cb7af359cf1cdaed247)
hidden