[perthmad]

> Typescript actually has an insanely powerful type system

I think you are conflating expressivity with complexity here. You do not need a complex type system to get a very expressive language. For instance, the typing rules of dependent type theory are fairly simple compared to the amount of trickery needed to make TypeScript work.

At constant expressivity, a simple type system is always preferable to a complex one. So I am not amazed by the fact that TS needs advanced PLT debauchery to kind of work. It doesn't even give you strong guarantees. There is a reason why Hindley-Milner type systems are called the sweet spot of static typing.

[dwohnitmok]

I think Typescript has both a complex and expressive type system. When I say "advanced" I'm talking about expressiveness. It is more expressive than Scala and (absent a laundry list of GHC extensions) Haskell.

I agree that Typescript certainly seems like a tower of hacks next to Idris.

Yet somehow it's pulled off a reputational miracle: having a more expressive type system than Haskell but not being regarded as an "advanced" language. Unfortunately I think that's mainly due to the ways the type system can be undermined, but it's still a useful nugget I ponder from time to time.

> It doesn't even give you strong guarantees. There is a reason why Hindley-Milner type systems are called the sweet spot of static typing.

HM by itself doesn't give you strong guarantees (see e.g. the ML family of languages which have comparatively weak guarantees next to Haskell). That's really due to other language and standard library decisions acting in concert.

HM type systems are often the sweet spot for static typing not because of the guarantees they offer, but because of the global type inference it yields. More expressive extensions of HM often break global type inference in some way.