TypeScript does not have dependent types. It has type-level constants and surprisingly powerful type manipulation facilities, including string manipulation on s

TypeScript does not have dependent types. It has type-level constants and surprisingly powerful type manipulation facilities, including string manipulation on string type constants. But there's no way to operate on types at the "dynamic" expression level - they're deliberately erased, to the point that transforming TypeScript to JavaScript is almost trivial. For example, take the very first example of a dependent type in the Idris tutorial - a function `isSingleton` that consumes a `Bool` and produces `Nat` if you give it `True` and `List Nat` if you give it `False`; it then uses `isSingleton` as part of the type of `mkSingle`, a function that consumes a `Bool` called `x` and produces an `isSingleton x` - that is, a `Nat` if `x` is `True` and a `List Nat` if `x` is `False`. There's no way to write this in TypeScript. You could have `isSingleton` return dynamic constructors instead, but you can't use that `isSingleton` as part of the type of `mkSingle` to generate a return type. Your `mkSingle` would be stuck with the signature `(x: boolean): number | number[]`; which branch of the return type you end up with depends on `x`, but there's no way to make TypeScript properly understand the connection.