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.
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?