Minimalism versus Types
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.
Muhammad, Hisham
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.
 All right, so let's get started. I am Hisham. I work at Kong and I'm also the maintainer of Lureox, 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 versus types and the long journey with the hard relationship between a minimalistic language like Lua and the desire for types. So minimalism, well, I love minimalism as all of us here in this room probably do and once someone asked me what do I like the most about programming with Lua and the answer that I gave right off the bat was that, well, Lua fits in my head. I feel like I know the entire language. The whole reference manual is like this one web page that you can read top to bottom and there's no corners of the language that I feel that I don't know. It's a very gratifying sensation being able to work in a language like that. As opposed to huge languages where there's always some kind of construct or part of the standard library that you have never touched. This is a classic example of huge language versus small language. The entire Lua reference manual is about the size of JavaScript, the good parts. The size of the languages and the size of their good and bad parts also kind of match. Hopefully, something like that. Well, it's actually older than JavaScript, but yeah, in many senses it's similar and some people who are thinking of the other side of JavaScript, they get surprised. No, they're nothing alike, but if you focus on the good parts of JavaScript, then they're surprisingly alike. So types, I also love types. And one thing that I like to say is that programming with types feels like pair programming with the computer. You program a little bit and then the compiler comes and say, well, you missed, like you made a typo here, something like that, or you cannot really pass this to that and all of that. So you get this nice feedback loop that's different than running the program and seeing if it crashes. Well, this is my interest in all types from a very practical perspective as a practitioner or as a programmer and not just a theoretical programming language, academic sort of interest. So before we dive into types, let's just get our terminology on the same page. When people often talk about typed languages and untyped languages, so the more accurate its terminology would be, like when you talk about untyped, you mean no types at all. So that would be like assembly. Everything's a byte. And those are not usually the types of languages, like the kinds of languages that we care. And for all the other ones, like there are types, like types exist. So string and number are different things. Automatic coercions can make this a bit confusing. So I said, oh, no, it's not typed because I can do string one plus two and I get a number. So no, it's actually like it's just doing an implicit conversion. They are actually different things. Like in Brad's presentation, he mentioned that all original A and 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 the theory field, they say like you shouldn't even talk about untyped. You should just talk about untyped because when you don't have typed, you really have one type, the type of everything. So the distinction that we usually care when we're talking about, ah, this language is typed or not, like when we informally say that, is that whether it's dynamically typed or statically typed. So dynamically typed in a nutshell means that values have types but variables don't. So you can move values that have types around and they fit any variable. So languages that fall into this category are like Lua, Scheme, Erlang, Python, Ruby and so on, all of those, like all of this typical, 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, C sharp, Rust, Haskell, like all of these other are statically typed. Checker and a step that you run before, like runtime, that tells you if your types are okay. So for the purpose of this distinction, we will totally avoid these terms like strongly typed or weakly typed because they're 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. So this is what we care about. But we also care about minimalism and apparently all of our favorite minimalistic languages all fall in the first group. Like there's Lua and Scheme and like all the other ones, TCL also there. So what gives? What happens when we put minimalism and types together? So let me go through a brief history of the efforts for typing Lua. So back in Lua Workshop 2013, Fabien Floteau presented Tidal Lock which was based on MetaLua, his Lua MetaProgramming library where he attempted to do like gradual typing of Lua programs. You could partially add type annotations, it would verify them and all of that. In his presentation, the main point of his presentation was that we all left scared of the prospects of how hard that problem was because he started showing like, oh, in the simple cases this isn't this work and then it starts getting messier and messier and messier because once you start to capture the way that Lua programmers deal with their data structures, he started to have to apply heuristics and things like that. So he start to scratch your head and say, well, wait, my type checker is going to be running heuristics on the code, right? Because when you think of a type checker, you kind of want some certainty and in the end it seems to be like a really tough problem. Nevertheless, tough problems is what research is made of. So around that time, André Midal was working with Lua and Types and two years after that he presented his PhD dissertation on that was called Typed Lua, an optional type system for Lua. So 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 and the thesis as he just, as he tried to make sense of the whole thing and he made an implementation that's on GitHub. And that implementation is a nice prototype of all those ideas, but really it's not ready for prime time in a sense that you can't really feed real world programs in it and try to use it as a day to day tool because the type checker is just too strict. It complains about lots of, lots of things that you as a Lua programmer said, no, this is right, but 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 in a completely unrelated subject but I got 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 started 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 would be slightly typed that would 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 say like, let's just do something else and really Titan tries to fit more as when you're programming like in that part C part Lua like embedded language type of thing, Titan would be more suitable for replacing the C parts rather than the Lua parts. So it's not really the same thing. And at the same time there's like super hard research questions on how to go about this and like some of us were approaching it from a very practical standpoint, some of us were approaching 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. 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 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? So I did some soul searching and thinking about the whole thing and I want to share like my thoughts about it. So our first stab at that question like when you think about it like and we are here talking about minimalistic languages and I start talking about types, types, types 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 and 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? 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? 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 right you are the type checker 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 would that type system look like for Lua code that we actually write nowadays with our tiny Lua language that fits in a you know in a 200k guitar ball you know so if you are the type checker what type system are you checking you know because this is the kind of work you do like you do like you have multiple returns in Lua you do oh 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 that line on the top is not going to work this is the kind of doing that you are doing in your head 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 type systems right because I was talking about dynamically typed languages I was talking about statically typed languages but within the realm of statically typed languages there are dependently typed languages dependently typed languages that is like new like 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 since well since types have values and values have 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 the third one is actually like a proof assistant like you know the cock from Nghia right so really but this is the kind of type system that you have in your head when you are 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 well A is an integer and B is well if A is less than 256 then B is a string otherwise B is an array of string you know when we have when we programming with dynamically typed languages we do that kind of stuff all the time without like even realizing that we are creating these complex types that have like 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 determine 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. But isn't this just a programming criteria because this is a very bad IPI so. 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 imposed 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 programming in your head every time because suppose you have those variable variables here red green and blue in there and there and you know they're all integers right you know that all 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 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 need to be strings and not to raise so that so there's probably an error here right but if the type checker had the information that read it's only ever between 0 to 255 you had specified that in the type right or then the type checker would have an easier job we would be actually able to do that right but it was 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 mathematics is mean like by the current Howard correspondent means like every types system corresponds to a kind of logic right so like first order logic second order logic you know and and and those things right so and by the way since the 50s we know that arithmetic is proven undecidable in logic so if you can have a type system type checker that knows all of arithmetic 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 okay and an error if not okay then well the type of error is like is dependent on the type of okay like if it's a string if okay is false right or if it's nil right and then when then what's the type of t 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 flow analysis could get really complicated and when you get to that like in the 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 can be an array it can be a dictionary it can be a struct can be an object it can be 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 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 when we 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 like touring completeness you know that's they are all the same blah blah blah but really it's like how can you express it right so and then in that sense dynamically type language is super expressive but it's super expressive in the same way that a blank sheet of paper is now the paper accepts everything you know the dynamically type language accepts everything and well it goes boom and you know if you do something wrong at runtime. On the other hand the type checker works both for good like oh thank you for catching my silly typo 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 fuel 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 name fields right and also servants in array like the 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 was still feel like Lua. Alright so okay so I'm just gonna jump ahead. So here for the final section like how 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 could still represent something like that like in Java right to just make an object that has like the name field and then a list you put one inside the other so it's like you have to think those thoughts like in a different way right. So 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 Lua then 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 and a table and say like oh in my typed version you have to do something like that you know items right or and maybe say Lua I cannot make something that's like sometimes a nil sometimes a string and I can instead of doing return x and 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 three available entry would have to be like the error message like those are simple those ones are fixable right but I'm just giving 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 program that the type checker accepts has correct types to something like oh if I complain then it's probably like wrong but if I don't you know if I don't complain I give you no guarantee and still that's hard because you made your the equivalent logic of your types of your type checker it's an unsound logic and when you add 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 deeper you are in research territory. Everyone has felt like whoever tried to deal with that ended up doing 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 closed by design by design by design it's not meant to detect that failure. So what about Lula? 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 in Lula but just like what's the minimum set of features so that it could type check itself. That would 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 fails 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 and the turtle. But yeah the idea is to do something a little like. It's here because even if then though it's not finished it wouldn't be false then if you know I talk about code then it's not a source. So in closing yeah the story will continue and thank you.
 All right, so let's get started.  I am Hisham.  I work at Kong and I'm also the maintainer of Lureox, 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 versus types and the long journey with the  hard relationship between a minimalistic language like Lua and the desire for types.  So minimalism, well, I love minimalism as all of us here in this room probably do and  once someone asked me what do I like the most about programming with Lua and the answer  that I gave right off the bat was that, well, Lua fits in my head.  I feel like I know the entire language.  The whole reference manual is like this one web page that you can read top to bottom and  there's no corners of the language that I feel that I don't know.  It's a very gratifying sensation being able to work in a language like that.  As opposed to huge languages where there's always some kind of construct or part of the  standard library that you have never touched.  This is a classic example of huge language versus small language.  The entire Lua reference manual is about the size of JavaScript, the good parts.  The size of the languages and the size of their good and bad parts also kind of match.  Hopefully, something like that.  Well, it's actually older than JavaScript, but yeah, in many senses it's similar and  some people who are thinking of the other side of JavaScript, they get surprised.  No, they're nothing alike, but if you focus on the good parts of JavaScript, then they're  surprisingly alike.  So types, I also love types.  And one thing that I like to say is that programming with types feels like pair programming with  the computer.  You program a little bit and then the compiler comes and say, well, you missed, like you  made a typo here, something like that, or you cannot really pass this to that and all  of that.  So you get this nice feedback loop that's different than running the program and seeing  if it crashes.  Well, this is my interest in all types from a very practical perspective as a practitioner  or as a programmer and not just a theoretical programming language, academic sort of interest.  So before we dive into types, let's just get our terminology on the same page.  When people often talk about typed languages and untyped languages, so the more accurate  its terminology would be, like when you talk about untyped, you mean no types at all.  So that would be like assembly.  Everything's a byte.  And those are not usually the types of languages, like the kinds of languages that we care.  And for all the other ones, like there are types, like types exist.  So string and number are different things.  Automatic coercions can make this a bit confusing.  So I said, oh, no, it's not typed because I can do string one plus two and I get a number.  So no, it's actually like it's just doing an implicit conversion.  They are actually different things.  Like in Brad's presentation, he mentioned that all original A and 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 the theory field, they say like you shouldn't even talk about untyped.  You should just talk about untyped because when you don't have typed, you really have  one type, the type of everything.  So the distinction that we usually care when we're talking about, ah, this language is  typed or not, like when we informally say that, is that whether it's dynamically typed  or statically typed.  So dynamically typed in a nutshell means that values have types but variables don't.  So you can move values that have types around and they fit any variable.  So languages that fall into this category are like Lua, Scheme, Erlang, Python, Ruby  and so on, all of those, like all of this typical, 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, C sharp, Rust, Haskell, like all of these other are statically typed.  Checker and a step that you run before, like runtime, that tells you if your types are  okay.  So for the purpose of this distinction, we will totally avoid these terms like strongly  typed or weakly typed because they're 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.  So this is what we care about.  But we also care about minimalism and apparently all of our favorite minimalistic languages  all fall in the first group.  Like there's Lua and Scheme and like all the other ones, TCL also there.  So what gives?  What happens when we put minimalism and types together?  So let me go through a brief history of the efforts for typing Lua.  So back in Lua Workshop 2013, Fabien Floteau presented Tidal Lock which was based on MetaLua,  his Lua MetaProgramming library where he attempted to do like gradual typing of Lua programs.  You could partially add type annotations, it would verify them and all of that.  In his presentation, the main point of his presentation was that we all left scared of  the prospects of how hard that problem was because he started showing like, oh, in the  simple cases this isn't this work and then it starts getting messier and messier and  messier because once you start to capture the way that Lua programmers deal with their  data structures, he started to have to apply heuristics and things like that.  So he start to scratch your head and say, well, wait, my type checker is going to be running  heuristics on the code, right?  Because when you think of a type checker, you kind of want some certainty and in the  end it seems to be like a really tough problem.  Nevertheless, tough problems is what research is made of.  So around that time, André Midal was working with Lua and Types and two years after that  he presented his PhD dissertation on that was called Typed Lua, an optional type system  for Lua.  So 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 and the thesis  as he just, as he tried to make sense of the whole thing and he made an implementation  that's on GitHub.  And that implementation is a nice prototype of all those ideas, but really it's not ready  for prime time in a sense that you can't really feed real world programs in it and  try to use it as a day to day tool because the type checker is just too strict.  It complains about lots of, lots of things that you as a Lua programmer said, no, this  is right, but 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 in a completely unrelated  subject but I got 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 started 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 would be slightly typed that would 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 say like, let's just do something  else and really Titan tries to fit more as when you're programming like in that part  C part Lua like embedded language type of thing, Titan would be more suitable for replacing  the C parts rather than the Lua parts.  So it's not really the same thing.  And at the same time there's like super hard research questions on how to go about this  and like some of us were approaching it from a very practical standpoint, some of us were  approaching 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.  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 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?  So I did some soul searching and thinking about the whole thing and I want to share like  my thoughts about it.  So our first stab at that question like when you think about it like and we are here talking  about minimalistic languages and I start talking about types, types, types 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 and 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?  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?  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 right you are the type checker 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 would that type system look like for Lua code that we actually write  nowadays with our tiny Lua language that fits in a you know in a 200k guitar ball you know  so if you are the type checker what type system are you checking you know because this is  the kind of work you do like you do like you have multiple returns in Lua you do oh 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 that line on the top is not going to work this is the kind of doing  that you are doing in your head 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 type systems right because I was talking about dynamically typed languages I was talking  about statically typed languages but within the realm of statically typed languages there  are dependently typed languages dependently typed languages that is like new like 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 since well since types have values and  values have 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 the third one is actually like a proof  assistant like you know the cock from Nghia right so really but this is the kind of type  system that you have in your head when you are 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 well  A is an integer and B is well if A is less than 256 then B is a string otherwise B is  an array of string you know when we have when we programming with dynamically typed languages  we do that kind of stuff all the time without like even realizing that we are creating these  complex types that have like 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 determine 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.  But isn't this just a programming criteria because this is a very bad IPI so.  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 imposed 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 programming in your head every  time because suppose you have those variable variables here red green and blue in there  and there and you know they're all integers right you know that all 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 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 need to be strings and not  to raise so that so there's probably an error here right but if the type checker had the  information that read it's only ever between 0 to 255 you had specified that in the type  right or then the type checker would have an easier job we would be actually able to  do that right but it was 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 mathematics  is mean like by the current Howard correspondent means like every types system corresponds  to a kind of logic right so like first order logic second order logic you know and and  and those things right so and by the way since the 50s we know that arithmetic is proven  undecidable in logic so if you can have a type system type checker that knows all of arithmetic  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 okay  and an error if not okay then well the type of error is like is dependent on the type  of okay like if it's a string if okay is false right or if it's nil right and then when then  what's the type of t 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 flow analysis could get really  complicated and when you get to that like in the 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  can be an array it can be a dictionary it can be a struct can be an object it can be  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 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 when we 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 like touring completeness you know that's they are all the same blah  blah blah but really it's like how can you express it right so and then in that sense  dynamically type language is super expressive but it's super expressive in the same way  that a blank sheet of paper is now the paper accepts everything you know the dynamically  type language accepts everything and well it goes boom and you know if you do something  wrong at runtime.  On the other hand the type checker works both for good like oh thank you for catching my  silly typo 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 fuel 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 name fields right and also servants in array like  the 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 was still feel  like Lua.  Alright so okay so I'm just gonna jump ahead.  So here for the final section like how 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 could still represent something like that like in Java right to just make  an object that has like the name field and then a list you put one inside the other so  it's like you have to think those thoughts like in a different way right.  So 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 Lua then 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 and a table and say like oh in my  typed version you have to do something like that you know items right or and maybe say  Lua I cannot make something that's like sometimes a nil sometimes a string and I can instead  of doing return x and 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 three  available entry would have to be like the error message like those are simple those  ones are fixable right but I'm just giving 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 program that the type checker accepts has  correct types to something like oh if I complain then it's probably like wrong but if I don't  you know if I don't complain I give you no guarantee and still that's hard because you  made your the equivalent logic of your types of your type checker it's an unsound logic  and when you add 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 deeper you are in research territory.  Everyone has felt like whoever tried to deal with that ended up doing 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 closed by design by  design by design it's not meant to detect that failure.  So what about Lula?  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 in Lula but just like what's the minimum set of features so that it could  type check itself.  That would 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 fails 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 and the turtle.  But yeah the idea is to do something a little like.  It's here because even if then though it's not finished it wouldn't be false then if  you know I talk about code then it's not a source.  So in closing yeah the story will continue and thank you.
Minimalism_versus_Types_An_experience_report_on_the_development_of_Titan__a_statically-typed_Lua-li__0_323.png Minimalism_versus_Types_An_experience_report_on_the_development_of_Titan__a_statically-typed_Lua-li__324_1079.png Minimalism_versus_Types_An_experience_report_on_the_development_of_Titan__a_statically-typed_Lua-li__1080_1151.png Minimalism_versus_Types_An_experience_report_on_the_development_of_Titan__a_statically-typed_Lua-li__1152_1295.png Minimalism_versus_Types_An_experience_report_on_the_development_of_Titan__a_statically-typed_Lua-li__1296_1535.png Minimalism_versus_Types_An_experience_report_on_the_development_of_Titan__a_statically-typed_Lua-li__1536_1739.png Minimalism_versus_Types_An_experience_report_on_the_development_of_Titan__a_statically-typed_Lua-li__1740_1847.png Minimalism_versus_Types_An_experience_report_on_the_development_of_Titan__a_statically-typed_Lua-li__1848_1895.png Minimalism_versus_Types_An_experience_report_on_the_development_of_Titan__a_statically-typed_Lua-li__1896_2027.png Minimalism_versus_Types_An_experience_report_on_the_development_of_Titan__a_statically-typed_Lua-li__2028_2111.png Minimalism_versus_Types_An_experience_report_on_the_development_of_Titan__a_statically-typed_Lua-li__2112_4511.png Minimalism_versus_Types_An_experience_report_on_the_development_of_Titan__a_statically-typed_Lua-li__4512_8099.png Minimalism_versus_Types_An_experience_report_on_the_development_of_Titan__a_statically-typed_Lua-li__8100_14951.png Minimalism_versus_Types_An_experience_report_on_the_development_of_Titan__a_statically-typed_Lua-li__14952_16019.png Minimalism_versus_Types_An_experience_report_on_the_development_of_Titan__a_statically-typed_Lua-li__16020_16859.png Minimalism_versus_Types_An_experience_report_on_the_development_of_Titan__a_statically-typed_Lua-li__16860_18059.png Minimalism_versus_Types_An_experience_report_on_the_development_of_Titan__a_statically-typed_Lua-li__18060_18803.png Minimalism_versus_Types_An_experience_report_on_the_development_of_Titan__a_statically-typed_Lua-li__18804_19571.png Minimalism_versus_Types_An_experience_report_on_the_development_of_Titan__a_statically-typed_Lua-li__19572_20819.png Minimalism_versus_Types_An_experience_report_on_the_development_of_Titan__a_statically-typed_Lua-li__20820_21359.png Minimalism_versus_Types_An_experience_report_on_the_development_of_Titan__a_statically-typed_Lua-li__21360_21431.png Minimalism_versus_Types_An_experience_report_on_the_development_of_Titan__a_statically-typed_Lua-li__21432_21587.png Minimalism_versus_Types_An_experience_report_on_the_development_of_Titan__a_statically-typed_Lua-li__21588_21659.png Minimalism_versus_Types_An_experience_report_on_the_development_of_Titan__a_statically-typed_Lua-li__21660_21779.png Minimalism_versus_Types_An_experience_report_on_the_development_of_Titan__a_statically-typed_Lua-li__21780_24215.png Minimalism_versus_Types_An_experience_report_on_the_development_of_Titan__a_statically-typed_Lua-li__24216_24647.png Minimalism_versus_Types_An_experience_report_on_the_development_of_Titan__a_statically-typed_Lua-li__24648_24911.png Minimalism_versus_Types_An_experience_report_on_the_development_of_Titan__a_statically-typed_Lua-li__24912_26879.png Minimalism_versus_Types_An_experience_report_on_the_development_of_Titan__a_statically-typed_Lua-li__26880_27575.png Minimalism_versus_Types_An_experience_report_on_the_development_of_Titan__a_statically-typed_Lua-li__27576_28907.png Minimalism_versus_Types_An_experience_report_on_the_development_of_Titan__a_statically-typed_Lua-li__28908_32003.png Minimalism_versus_Types_An_experience_report_on_the_development_of_Titan__a_statically-typed_Lua-li__32004_33299.png Minimalism_versus_Types_An_experience_report_on_the_development_of_Titan__a_statically-typed_Lua-li__33300_33467.png Minimalism_versus_Types_An_experience_report_on_the_development_of_Titan__a_statically-typed_Lua-li__33468_33633.png