Article Publishing
~ sophisticated type system of the future
Continued discussion from this article: Type Systems of the Future Danger Zone

Today with our toy 1970's based languages like plain C and Pascal, how would you do something so basic and simple needed by every space ship or rocket: cm/mm/meter/feet/inch types. And I mean types, not some library hack that makes you sort of program the code in such a way that you use run time checks of your own using some math module or special module dedicate for helping with this situation. Helping won't cut it. I mean a proper native support for such issues. I mean an actual type system that really does deal with these measurements natively in the language.

More precisely, this article is addressing the fact that C and Pascal, and SQL have toy type systems. Maybe I mis-spoke when I started this article saying C and pascal are toy languages; what I really want to focus on is toy type systems. At the time, actually, when Pascal was invented in the 1970's it's type system was considered rich. But really?

So if we want to use "5cm" or "5ft" in our languages today, can we do it? Well in plain C and pascal or SQL, Nope. A strong "nope, you can't".

You could do the worst possible thing: just use strings! everything is a string. Pseudocode below...

var
  landingDistance: string;
begin
  landingDistance := "5ft";
  landingDistance := "You can fuck this string up.. now it's anything you want";
  landingDistance := "Strings are flexible, not precise landing tools for rockets";
  // ...
  // reinvent a type system at run time
  if checkDistanceStringIsCorrect(landingDistance) = false then
    print("your landing distance has an error);
  end;
end.

Obviously using a string is absurd since a string, for a precise numbered measurement, is not going to be type checked, unless you run functions/procedures on the string at run time, basically reinventing a type system of your own that should be in the compiler itself.

So then you could instead use a struct or record (again this is all pseudocode):

type
  TDistance = struct
    number: integer;
    measure: enum(ft, meter);
  end;

var
  landingDistance: TDistance;

begin
  // set the current measurement system to feet or meters
  landingDistance.measure := ft;
  landingDistance.number := 5;
  // so now it is 5 feet or 5ft. But this took two steps..
  // ...
  // and now below is where issues start to occur
  landingDistance := meter;
  print(landingDistance.number);
  // above prints 5.  But with a proper type system...
  // doing the above would actually print the correct converted distance in meters
  print("1.524");
  // but does it print 1.524, or does it print 1.524m, or 1.524meters
  // subtle differences... all scary to think about
end.

Maybe you aren't as scared as I am, but I see a madness starting here.


In the above example a struct (or record) contains a enumeration that can change from meters to feet for a measurement system.... But at what point do you start to have to expand the compiler itself to include this type system? if you don't expand the compiler you are stuck doing pathetic run time (read: erroneous) checks that reinvent a type system at run time instead of having at least a partial proof at compile time.

So you could add a "convert" method or procedure/function to the struct and just make sure the programmer calls the convert each time.

type
  TDistance = struct
    number: integer;
    measure: enum(ft, meter);
    proc convert();
  end;

// ...

implementation

import SaeMetricTools;

proc TDistance.convert();
begin
  // ..
  case self.measure of
    ft:
      self.number := SaeMetricTools.FeetToMeters(self.number);
    end;

    meter:
      self.number := SaeMetricTools.MetersToFeet(self.number);
    end;
  end;

end;

But we are just talking about meters and feet here. What about a million other potential types that could be implemented in a language or type system? So how do you stop the compiler from growing to a monstrous complexity? Put it in the libraries, some say. You take the run time route and modify your language at run time to support new types, or you just use libraries and don't modify the language; how do you stop it from growing into a Lisp or a Common Lisp, or a Constructive Type System that grows like Lisp but even more horrendous.... how do you stop Ada from becoming monster ada? Likewise for c++.

If you put it in the libraries you still can't so easily go:
  distance := 5ft;

Instead you do:

  distance.number := 5;
  distance.measure := ft;

This can get very verbose when doing lots of calculations...

The buzzword is "expressive power" (or lack of).

So then you could make a domain specific language inside your language (lisp much, folks? we know how that goes...). Domain specific langauges, or hacks, tend to be half assed broken versions of a language that are buggy, and half implemented, improperly.

The fact that cm/meter/feet/inch issues baffle us today is cause for serious concern. FFS (for fine sake), the cm/meter/feet/inch issue should have been solved in what, 1960 or something? I mean that seems like a trivial issue... now think of 5 million other types that could be of issue and of use for humans: decibels, RPM of an engine, Hours/minutes/seconds, light years, relativity, coordinates (you think records/structs solve these?), dates (month, year, calendars, etc), AM/PM vs 24 hour clocks (most people solve these issues at run time with functions that check or convert, but why can't a compiler ensure the safety of a program at design time?), mathematics units, science units, acres of land, hectares, knots as a speed, kilowatts, horsepower, torque, and FFS (fiftyzillion further systems).

See also:
- Predicate Type System Related
- And More

Note: This article is a work in progress. It is not finished yet.
Copyright © War Strategists, M.G. Consequences 2009-2017    Help! Edit Page