Things to say about typescript

There are type annotation proponents who think everything should be type annotated. I figure they think that "large scale" software doesn't stay organized otherwise. I guess I have to agree these guys are correct, but they could as well be wrong because they keep getting the details wrinkled.

For an example lets look at Typescript. Last time I watched at typescript code, I just rewrote it again in coffeescript because that was faster and less inconveniencing than understanding how to use the code.

On top of that it was some sort of boilerplate -thing that I didn't need to even implement in that Javascript code. Typed languages could be made with capabilities to build up boilerplate from type information. Typescript doesn't seem to be one of those languages that does it that way.

I also don't like that it's an OOP-style language. OOP-programs do not compose in a very useful manner because OOP-compositions hide race conditions. This is something people figured out a good while ago. Typescript seem to be that language that still does it.

I hate the autocompletion features VSCode/Visual Studio has to offer for Typescript because they pop and distract and correct my code such that it goes wrong and then nags about it. You probably start to see a trend here.

I haven't used refactoring tools in either Typescript or C# because aside renaming things the program doesn't remain correct anyway.

Typescript has been built such that it leaks the implementation details of Javascript. The strings, integers, etc. It exposes are those from Javascript. There's even "null" and "undefined" exposed. You shouldn't need "basic types" in typed languages. How about I'd actually want to not ditch all the code I wrote when I change a language?

'any' -type... You'd think that if you wanted to make a bridge into an implementation language, you'd make it in a way that it requires you to parse the structures so you wouldn't get surprise-runtime errors.

Typescript:

let notSure: any = null;
notSure.SOILING_MY_PANTS();
    // it is okay, a function like this might exist there!

Elm got this right with its json-API, Idris got it right... There they actually require you to validate your 'any' such that it becomes x → y before you call it. Sure there are languages where it's like this other way around but why Typescript is such a language that got this wrong?

Then we got "never", and there would seem to be the ∀a. never → a -axiom for it in the subtyping rule. This is potentially an useful type but why it's quirky? while (true) {} is a valid way to produce "never", but then there are return error("") and throw new Error(...) as well. "never" clearly tries to be the empty type but it doesn't distinguish between programs that won't run, and programs that crash.

In a formally verified language "crash" command cannot be given without providing a reason why the program cannot continue. This may come from a contradiction or from a precondition. Eg. You'd be able to state that "it was promised this value is filled in, but it's not present". Crashes coming from contradictions mean that a data corruption occured while precondition-related crashes mean that the program was used incorrectly. Difference between these two form of failures is quite significant because corruptions may lead to halting while incorrect use generally must not. Typescript doesn't recognize this idea, it just loaned errors&crashes from Javascript and treated types as a fancy form of syntax rather than something that has semantics.

There would be more to write about "never" type and its quirkiness, but it'd require digging open the structure of Typescript that it loaned from Javascript. If something crashes it's a literal crash with no internal way to recover. The operating system or other supervising layer should step in. "Callee" isn't a proper supervisor because it's part of the same space where the crash occured.

Also, let me tell you subtyping and type inference is doable, but I doubt they've perfected it with Typescript. Even if that's a bit of a red herring, the type inference.

I could keep going on but to cover the whole thing I'd have to go through the whole user manual of Typescript and I'm trying to make a filler post here.

You could try to argue that Typescript isn't supposed to do this. It's just a layer of types over Javascript. Eg. If we modeled Typescript's objects in Idris, they'd be those of Javascript:

data Js : Type where
    JsArray  : List Js -> Js
    JsObject : Map String Js -> Js
    JsString : String -> Js
    JsNumber : Number -> Js
    JsNull : Js
    JsUndefined : Js

And typescript types would be restrictions over the Js type, then we'd have notion of what is a valid Js type that "inhabits" the Ts type:

data Valid : Ts -> Js -> Type where
    ValidString : (s:String) -> Valid (TsString) (JsString s)
    ValidArray : (a:Ts) -> (xs:List Js)
      -> ForEvery (Valid a) xs
      -> Valid (TsArray a) (JsArray xs)
    etc...

I don't mean to show that Idris would enclose Typescript somehow. The point is that Typescript's type system isn't very useful because it focuses on irrelevant things.

The useful thing about types is that...

  1. It provides some indirection between how the program is interpreted and what is meant with the structures being used.
  2. It allows to write programs that are correct up to a spec that is expressive enough to weed out program states that we don't want. For example. "You have numbers 'x', 'y', 'z', 'x' number is between 1 and 4 and 'y' is divisible with 'x' and 'z'."
  3. It can be used to check that specs are consistent in relation to expectations that we can encode in the type system. Eg. We can check that some interface satisfies some behavior we care about.
  4. It allows automatic construction of trivial "glue" programs. Eg. Case splitting in Idris or FFI-interface buildup from declarations.
  5. It also gives a way to compose programs together while abstracting over implementation details, allowing multiple ways to implement things.

I hardly see anything of that happening in Typescript.

Similar posts