|
Article Publishing
|
~ type systems of the future danger zone |
Our toy languages of today and their trivial toy type systems from the 1960's and 1970's are actually a good thing, because they are just toys. When you have a very limited type system, it is easier to prove programs correct or reason about them, to some sense.
Imagine a type system so powerful and profound that it could model almost anything in our universe. A type system that had no problem dealing with foot/cm/inch/mm/meter/cm measurements right inside the language itself (somehow), a type system that could model decibels (dB), a type system that could deal with time (hours, minutes, seconds) without runtime conversions (most checks done at compile time)... a type system that could model anything imaginable. Something like Unicode where pretty much anyone's imagination can cough up a language and barf it into a computer; but instead of languages used by different races, I'm talking about types which model things.
..for more discussion on theoretical and practical implementation of such a system see the page:
Sophisticated Type System of The Future
The issue we know with unicode is that it is very hard to prove a program does something correct when you've got a million symbols. It's much easier to reason about a program that only deals with 255 or 26 symbols or characters, or 26+10 digits. a..z 0..9 and nothing more.
The issue with type systems that are powerful is that we will end up with super creative people going on, and on, and on, with brand new type models or types. Sort of like the string theorist who kept discovering a new dimension or new addition to string theory, or sort of like the excited unicode happy person who just added yet another symbol to unicode, that, unfortunately, will just make programs much harder to reason about.
On the other hand the positive side: with a powerful type system that can precisely model something, you save lives. 10 people could die because some person does run time hacks/checks to try to make a program correct, when a space rocket is flying to Mars or whatever planet. It can cost human lives, but also millions of dollars. With a type system where any type can be created using constraints/restrictions/predicates, you could theoretically save Nasa or Elon Musk, or whoever, 10-1000 human lives (or if talking nuclear warfare, possibly a million lives or more), and also millions if not billions of dollars.
If a compiler was able to check a meter/foot conversion and catch the error at compile time or at least give a strong warning then a space ship could be prevented from crashing.
You might think what is the big deal? we can already model cm/mm/meter/foot/inch and other measurements by simply creating a struct/record that models it. But what you end up doing is manually creating and rolling your own type system at run time that could have been implemented more at compile time. Now there is indeed no perfect compile time only system (if that were the case, our compilers would prove our program correct 100 percent and there would be no "unit testing" or real world testing needed), but there certainly is need for improvement of our toy type systems we have.
But as I warned in the start of this article this of course is a double edged sword. With a powerful type system where you can model anything you want in the universe, you can end up with something along the lines of a Lisp like effect. Creative people will get a hold of this type system and create millions or thousands, or even hundreds of types and type models and type variations. Like going to a restaurant and seeing 5,608,398 different meal systems to choose from (not just meals but meal systems) and wondering: "why can't we just go back to plain C or standard pascal where I could actually understand what was on the menu?"... i.e. trivial toy type systems where you could almost write the types down on a napkin or your hand. A limited set.
With an unlimited set this is indeed a danger zone... infinite complexity, infinite possibility.. Kind of like unlimited unicode symbols but no one knows if a program is correct or will have an error because there are so many symbols to choose from.
Another issue that scares me is the problem of compatibility. If Haskell or Ada or C++ a language with a sophisticated type system tries to link to another language (whether through a DSO or DLL, or some other means, even IPC).. you may have issues with type system compatibility. In fact you will, not may. So then to communicate with other languages it will be the lowest common denominator, i.e. going back to plain C types or standard pascal style types; Which kind of defeats the purpose of the type system if you have to go back to a lowest common denominator to do real work or integration with other tools. Still that may be a solution to the problem: work with a sophisticated type system where you need to, but then if you really need to integrate some other tool then use an escape route, a disciplined lowest common denominator set of types, like simple arrays, records, structs, tuples, integers, booleans.
How does one stop neo type systems of the future from becoming a nightmare of complexity, like a box of unicode symbols in a cardboard box that falls out of a truck and scatters it all over the highway. Some nasty people are going to get a hold of type systems and complicate the hell out of them, or expand them to beyond humanly understandable....
I both fear and love the idea of a sophisticated type system that is not a toy and trivial. Indeed the type systems of the 1970's (or maybe 1960's) are a limited important set to work with that have given us some wonders. Are they enough? Do they cost us human lives and millions of dollars in rocket ship, and war damage...
Even a router that crashes that you have to reset, or a voip router that needs to be unplugged every month... could be because a type system was not used that suited its model. It would be easy to just blame all problems on poor type systems and that's not likely all there is to it, but indeed it could be that we have been sadists working with these toy type systems we have in place. I suppose object orientation tried to expand on type systems by adding inheritance but really is inheritance going to save you a life when a spaceship is on its path to a new planet... I somehow doubt that inheritance or other object oriented features will improve the safety of a ship in travel.
One question is, what the hell have Ada designers been doing for the last, few decades? Should they have not been working on all these problems discussed in this article above> Have they only added half-arsed solutions and not actually addressed the problem fundamentally? I do not know enough about Ada (or Haskell) but C++ programmers (the founder of) is talking about it (especially cm/mm/foot/inch/km/mile issues).
The only reason I do not modify a C compiler or Oberon or Ada or Haskell compiler to implement a sophisticated type system is that I see no ponzi scheme attached to it (way to make a living off it). It's an interest I have, but, looking at type system related books such as Tutorial Dee / The Third Manifesto, they aren't very popular sales in the free market, as people tend to not generally give a flying fudge fuck about academic topics like such.
Then you have the question of, SQL's toy type system. A joke it is. On the other hand working with a toy limited type system can be good because you can understand it in almost one sitting or one evening. A really sophisticated powerful type system might take years for someone to understand. How are these paradoxes and issues resolved? I don't know: I'm not getting paid to study this, so I really don't care. I do care, but, when there is no money involved, it goes on the back burner, and I really don't care. The only free market solution is to become an academic nut working at some university that is interested in such, or maybe, being hired by Nasa or Elon Musk who cares about deaths on a ship and human lives lost. But could someone study (and implement) type systems for 10 years or would it quickly become tedious and you'd only want to have it as 10 percent of what you do in the day, or the month.
What was really funny was to see all the object oriented dynamic language people ignore the idea that types exist and pretend that somehow these objects or classes they were using were not just type systems in disguise.... I'm thinking something along the lines of SQLite which apparently is typeless, and then, you end up reinventing your own type checks at run time using code, to defend your database from containing errors. I am also thinking about languages like PHP/ruby where you do not declare your types or even know much about types, until you, well, go something like somevar.to_s. As soon as you admit you are making something "to a string" or "to an integer" you just admitted your language does have types even though you denied it had types or denied that types were really of any use to anyone.
The danger is always the double edged sword. I can see type systems of the future being much more sophisticated than the 1970's toys we use today. Array, integer, boolean, and string? are you kidding me? I'm afraid type systems can be a bit more sophisticated than that. But I love a trivial toy as it's much easier to reason about than a monster mammoth sophistication.
This space ship is in the danger zone: it's landing.
|
|