Types do not need to have a one-to-one correspondence with runtime data structures and indeed in many type systems often do not. In the limit, a type does not need to have any runtime representation at all (this is more than just generic erasure or phantom type parameters, you can have an entire type signature that has absolutely no runtime representation of any of its parts).

There is not really a fundamental difference between types and static analysis.

A predicate is a computer program that accepts an input and returns "yes/no." A type system could be an arbitrary predicate which returns "well typed/not well typed" when given a term. But obviously there must be some difference between types and predicates, such as extensionality -- the type of an expression can be decided by examining the code alone.

Are you responding to my assertion that there's no fundamental difference between type systems and static analysis? If so, if we just change "well typed/not well typed" to "acceptable/not acceptable" I think you've pretty much just described static analysis.

> You can specify basically any type you what... stuff like “The Number 4 Or A Function That Returns The Number 4 Or An Object With Any Attribute Which Is Equal To 4” and TS will just work with that.

Hi, an amateur here. When I started to learn JS and later TS I always disliked this expressiveness. Like when the first parameter you pass to JQuery can be anything in the world: a DOM element, or collection of elements, or an object, or a function - and only then you declare what you want to do with it. Yes, the syntax is short. And you pay for it with a lousy code readability and steep learning curve.

My question is, is there a name for this "expressiveness"? Is there a name for the opposite? I am looking at the definition of AssemblyScript: "...compiles a strict variant of TypeScript (basically JavaScript with types)". But the word "type" is again used recursively here. Is there a name for this "strict type"?

> Like when the first parameter you pass to JQuery can be anything in the world: a DOM element, or collection of elements, or an object, or a function

That specific part is called overloading in OOP (java). Don't know about the rest.

> I would love if a compiler expert could chime in here, but my understanding is you could never write a Typescript compiler that was “strongly” typed because there is no data structure that can efficiently represent arbitrary types like “4 Or An Object With An Attribute Set To 4” in any meaningful way.

(I don't consider myself a compiler expert by any means, but I've been doing it for nearly 20 years, so I feel relatively safe weighing in here.)

In short, if you were compiling a function like that for bare metal (or anything relatively like it), there would be no one function that takes in all of those types and acts on them. Instead, you would compile that function once for each combination of incoming types. The version that only takes the number 4 would not have any inputs at all and may end up entirely constant (depending on what it does, of course). It's then up to the caller to make sure the right variant is called. If you have strong types up the chain, this is easy and completely overhead-free -- they'll be compiled in their different versions, too. If you have a weaker type constraint (e.g. just any Number, rather than THE Number 4), then you'd do conditional dispatching at the call site.

For what it's worth, this is essentially how templates work in C++. It's also why compilation can take so damn long and can produce gigantic binaries, because when you have a function with 2 inputs of 4 different potential types each, you're up to 16 variants. Change that to 5 inputs of 4 different types and you're at 625 variants.

All that said, static compilation of TypeScript in its current form would be very difficult to make efficient, simply because JavaScript types in the abstract don't map nicely to hardware; Arrays can be extremely simple and linear or ungodly complex with holes and property overrides, and the 'right' thing to do with a Number is often different from the fast thing to do. That's why JITs are so valuable; they allow you to get around the ambiguity.

Edit to add: I should mention, it's possible you won't actually generate all combinations. You might know that certain combinations are impossible to hit due to other type constraints, or you might just know that they're unused (which leads to problems when you don't have the original function definitions to turn to; that's why C++ templates have to be in headers (I think that's true, at least? I might be wrong on that; I just use the magic, I don't understand it)).

I don't really know anything, but isn't this how Haskell and Elm work? With similarly expressive type systems?

There's a general mismatch between popular conceptions of type system expressiveness and actual type system capabilities. Elm has a very simple type system. In fact it is very close to having among the simplest type systems in any statically typed programming language (the only things that really set it apart are tagged union types and record types). For example Java has a much more expressive type system than Elm in many ways. What perhaps makes Elm's type system seem advanced is that the runtime essentially never violates the guarantees of its type system, unlike Java (depending on your opinion of unchecked exceptions).

Haskell has a much more expressive type system than Elm, but still lags behind Typescript unless you turn on a truly gargantuan number of extensions.

It's also a bit weird to compare the languages because Typescript has a very different typing regimen than Haskell or Elm. Typescript is entirely structural while Haskell is almost entirely nominal and Elm is mostly nominal (with the exception of records).

Typescript has an extremely expressive type system. It is in fact so expressive I'm amazed that it's gotten so much adoption when languages like Haskell are still considered "advanced." I suspect it has to do with the semantics of the languages rather than the type systems.

> Haskell has a much more expressive type system than Elm, but still lags behind Typescript unless you turn on a truly gargantuan number of extensions.

IIUC: it's not a total order, Haskell (even '98) has things TypeScript doesn't[0], and TypeScript has things that Haskell (even with extensions) doesn't[1].

[0]: eg. higher-kinded types [1]: eg. (convenient) row polymorphism

Yeah you're right it's not a total order. I was being fast and loose and conveying a subjective feeling.

RE row polymorphism, Typescript doesn't quite have what users of ML-like languages are asking for when they want row polymorphism (which is usually parametric polymorphism rather than subtyping). But it's close.

As for convenient... well I'd argue by the time you've got the whole cornucopia of GHC extensions at the top of your file nothing is quite convenient at that point.

> RE row polymorphism, Typescript doesn't quite have what users of ML-like languages are asking for when they want row polymorphism (which is usually parametric polymorphism rather than subtyping). But it's close.

How would you distinguish this from the following?

    function foo<T>(x: T & {field: number}): T {
        ...
    }

> As for convenient... well I'd argue by the time you've got the whole cornucopia of GHC extensions at the top of your file nothing is quite convenient at that point.

That was one part of my point. That said, I think the problems implied by language extensions are often exaggerated (probably not deliberately so, most of the time).

The other part of my point was that even with all the extensions you need, I've not found good row types in Haskell, although the particular failings vary by approach. Which isn't to say I can't get something that works well enough for my particular situation most of the time.

    function foo<T>(x: T & {field: number}): T {
        return x;
    }
    
    function bar<T>(x: T & {field: number}): T {
        const x0 = foo(x);
        // type error because x0 doesn't have field
        // would compile fine with row types
        const x1 = foo(x0);
        return x1;
    }

Yes it's true. I also sorely miss the lack of row types in Haskell (I miss them even in something like Idris where you can create them more easily, but it's still not great compared to first-class support).

EDIT: I may be being dumb. You could probably fix this by adding an intersection type again on the right-hand side. I think there was something else I was missing from TS, but I'll have to noodle on it a bit more.

Not dumb, you answered the question I asked :D

But yeah, I agree that duplicating the intersection produces another interesting question.

In any case, "convenient approximation of row types" probably still applies to TS more than Haskell. And possibly also "more convenient row types", but that remains TBD.

Most typed languages work like this way. For example, Java compiles down to the bytecode. The JVM bytecode doesn't have preserve generics information. But Java code has generics so when it compiles down to the bytecode, it removes that information. This is almost true for all high level languages. Kotline's type system is very different than Java but it also compile down to the bytecode so Java and Kotline shares their libraries without sharing the type system. Type Script is no different. Only problem here is that Type Script doesn't bring its own "runtime" or libraries.

> These kinds of “wacky types” are things you can statically analyze but not really “compile” per se. That’s why it’s a good fit for being transpiled down to a language with no types at all.

> TL;DR, TypeScript is not really a “typed programming language”, it’s a static analysis tool. It’s not really designed to “run”.

I think you have an interesting point but you've come to the wrong conclusion. Assembly language doesn't really have any notion of types (there is some notion of sizes as some instructions operate on, for example, single words and some instructions like SIMD ones operate on multiple words at a time) yet we still consider C, C++, Rust, Pascal, etc to be "typed programming languages". It's really only languages that compile to some kind of VM which have a notion of types at the runtime level and even then, many VMs erase some of those details like the JVM and generics.

This isn't strictly true, and @erikpukinskis has a point. Typed languages often do have type info that can make it to runtime. `typeof` -- virtually the only tool JS has for type reflection -- doesn't even compare to the richness of TypeScript. All of that richness is indeed lost in transpilation.

In C++, for example, we have `decltype`, `typeid`, type traits, RTTI, and so on -- all of which are available at runtime. Not to mention that in certain special cases, we also have the de facto storage of type information that makes it into binaries (e.g. discriminated union types).

You don't need any type information at runtime if your type-system is strong enough. You need only types at runtime to do reflective checks, and you need those only if your type-system can't give the needed guaranties statically at compile time.