3 ms·
A dependent type system can do both.
by CMCDragonkai 9y ago
A dependent type system can do both.
- zbentley 9y ago...yes it can? 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?
- CMCDragonkai 9y agoNot in an HN comment, but here's a paper called Power of Pi https://cs.ru.nl/~wouters/Publications/ThePowerOfPi.pdf 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.