Зависимые типы для проверки структурированных данных

Во-первых, я действительно не знаю, что не так с зависимыми типами и почему мы не делаем этого » Я не вижу, чтобы они были реализованы на существующих языках для практического программирования, вместо того, чтобы изобретать всевозможные уловки (шаблоны!), чтобы обойти ограничения текущих систем типов, которые в лучшем случае имеют очень простое и ограниченное обобщение.

Но мой вопрос касается зависимых типов. для данных, а не для программы, как и можем ли мы использовать их для проверки структурированных данных? Это означает, что, например, json, xml или любые структурированные данные, можно ли их эффективно проверить с помощью какой-либо системы зависимых типов?

Edit:

Под зависимыми типами я имел в виду это наиболее широкое определение «типа, который зависит от ценность », и не обязательно тех, кто доказывает теоремы и сотрудники CoC.Я их не знаю и не хочу идти по этому пути, я не верю, что это единственный и «окончательный» способ получить достойных иждивенцев. В FP программисты ежедневно пишут свою самую сложную логику очень элегантно, конструктивно, со всей простотой и без каких-либо проблем. Я верю, что у них будет окончательная «элегантная» зависимая типизация.

Однако мой вопрос касался чистых данных, в отличие от кода, когда много проверок может быть просто ненужным и может просто скрываться в потоке программы и логике, даже динамическая типизация может работать нормально. В случае данных это не тот случай, когда вы хотите проверить правильность документа и дать четкие сообщения об ошибках. С другой стороны, данные не имеют проблемы сложности, когда вам приходится иметь дело с «функциями» в очень сильно зависимой системе типов (из семейства CoC).