This is an example of Typescript kinda sorta have some of what Dependent Types will give you. The problem is that the Typescript team hasn’t fully embraced this

This is an example of Typescript kinda sorta have some of what Dependent Types will give you. The problem is that the Typescript team hasn’t fully embraced this. So instead of implementing Dependent Types (see Agda/Idris/LEAN), the team is kinda sorta implementing parts of it piece wise, inventing different syntax for each feature as they add it. A bit like templates in C++ ended up kinda sorta implementing a Turing complete functional programming language with the worlds worst syntax. It looks as if Typescript is going down the same road. It’s a bit of a mess compared with Dependently Typed languages (Agda/Idris/…)