Would you expand on how dependent type systems are relevant to the differences between TypeScript/JSON-Schema, or how the use of a DTS could help ameliorate the issues people have in those areas?
Not in an HN comment, but here's a paper called Power of Pi https://cs.ru.nl/~wouters/Publications/ThePowerOfPi.pdf that probably explains it the best. It shows the usage of it for deriving a parser and generator from a single specification, and also crypto protocols and database usage. It uses Agda for its examples, but it can be translated to Idris as well.
