First of all, I don’t really know what’s wrong with dependent types and why we don’t see them implemented in existing languages for practical programming, instead of inventing all kind of tricks (patterns!) to bypass the limitations of current type systems which at best has very simple and limited generalization.
But my question is about Dependent types for data not a program, how or can we use them for structured data validation? Meaning, like json or xml or any kind of structured data , is it possible to verify them efficiently using some dependent type system?
Edit:
I meant by dependent types it’s most wide definition “type that depends on a value”, and not necessary those theorem prover and CoC staff. I don’t know them and I don’t want to go that road, I don’t believe those the only nor ‘the ultimate’ way to get decent dependent types. In FP, coders write their most complex logic everyday in very elegant, constructive way with all simplicity and having no problem at all. I believe they will have their ultimate “elegant” dependent typing.
However, my question was about pure Data , unlike in code when a lot of checking can be just unnecessary, and can just hiding in program flow and logic, even dynamic typing can work fine that way. In data, it’s not the case when you want to check some document correctness and give clear error messages. In another hand data does not have the complexity problem when you have to deal with “functions” in very extreme dependent type system (of CoC family).