They certainly introduce nice concepts in TypeScript, I love how they can seem to fit it all in so fast, there's lots of tricky edge-cases. Dependently typed l

They certainly introduce nice concepts in TypeScript, I love how they can seem to fit it all in so fast, there's lots of tricky edge-cases. Dependently typed languages like Agda and Coq can do the conditional types, as typelevel computation is in their very nature. With things like Liquid Haskell there's some spillover to 'normal' functional languages, but it's a bit clunky sometimes and it's not native to the language. I just skimmed over some information on literal types, but think they're just not that interesting to languages that support (G)ADT's, as the overhead of not using primitives is not the case when you're compiled. But for other interpreted languages it might be very interesting!