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

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

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

Edit:

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

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

Ответ 1

Вам, вероятно, будет интересен этот документ: Следующие 700 языков описания данных (PDF), Кэтлин Фишер, Ицхак Мандельбаум и Дэвид Уолкер, 2006 г.

Основная цель этой статьи - начать понимать семейство специальные языки обработки данных. Мы делаем это, как сделал Ландин, разработка семантической основы для определения, сравнения и контрастные языки в нашем домене. Эта семантическая структура вращается вокруг определения исчисления описания данных (DDC ^ α). Эта исчисление использует типы из зависимой теории типов для описания различных формы специальных данных: базовые типы для описания атомных фрагментов данных и чтобы описать более богатые структуры. Мы показываем, как давать денотационная семантика для DDC ^ α путем интерпретации типов в качестве синтаксического анализа функции, которые отображают внешние представления (биты) в структуры данных в типизированном лямбда-исчислении. Точнее, эти парсеры производят оба внутренние представления внешних данных и дескрипторы разбора это точные ошибки в исходном источнике.

Короче: да, зависимые типы необходимы, если вы хотите статически кодировать мелкозернистые инварианты о ваших данных. Являясь более выразительными, чем алгебраические типы данных и GADT, они также позволяют выразить их и связанные с ними конструкции (например, сочетание немаркированного объединения и помеченного продукта), имея возможность быть каким-то языком ассемблера описания данных, даже если спецификация, ориентированная на пользователя, напрямую не раскрывает зависимости сроков.

Остерегайтесь, однако, что такой формальный подход стоит за счет более крутой кривой обучения и более высокой сложности перед запуском, даже если теоретически он окупается с более легкими, безопасными, лучшими спецификациями, инструментами манипуляции и т.д. Практикующие в этой области чаще будут игнорировать всю эту красоту системы и отказываться от неверно определенных альтернатив. XML теряет JSON, по другим причинам, потому что указание схем является скучным, и люди не видят, какие преимущества они приносят. Да, позже вы можете указать статическую структуру принятого JSON API (и для этого вам могут понадобиться зависимые типы, поскольку сложность легко вписывается в такие форматы эволюции, а не в дизайне), но это малопригодно, если никто не заботится об этом, не использует его, не понимает и, что более важно, его поддерживает.

(На вторичном фронте относительно вашего троллического введения: пожалуйста, идите вперед и играйте с ATS, Guru или Agda, они предназначены для относительно практического программирования. идти по маршруту франкенштайн, есть также SHE; Coq не предназначен для "практической разработки программного обеспечения", но, как известно, он подвергается насилию таким образом - я бы не советовал его для навязчивого программирования, но он хорош для не очень-зависимого программирования плюс сопроводительные доказательства правильности - - и если вы хотите продать свою душу, в ближайшее время также будет F *.

Ответ 2

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

Это не обязательно прерыватель транзакций, если поведение проверяющего типа можно сделать простым и интуитивно понятным. Избегание бесконечных циклов во время компиляции может стать просто частью программирования для такого языка, так же как избежать бесконечных циклов во время выполнения.

Однако то, что эффективно добавило бы, это "компилировать временный уровень" для вашего программирования, выполняя полное вычисление Turing в совершенно другом режиме для обычной программы. Я считаю, что это уже можно сделать в некоторых местах; Мета-программирование шаблона С++ - это, по-моему, завершение Turing, а система типа Scala может кодировать исчисление SKI в соответствии с блоком, который я читал один раз.

Но на самом деле программирование таких систем ужасно. На языке программирования с хорошей системой типов существует система типов, упрощающая программирование; он вводит в действие инварианты, предупреждает нас, когда изменения одной части программы влияют на другую, и предоставляет документацию о том, как использовать код библиотеки (часто можно сделать довольно хорошее предположение от имени и типа в точности, что делает функция Haskell). Но когда вы программируете систему типов в, у вас нет этой помощи, если кто-то не добавит мета-тип системы. Опять же, они действительно существуют для некоторых языков (я считаю, что Haskell и Scala оба имеют концепцию типов типов), но они не предназначены для того, чтобы иметь одинаковое отношение к мета-программированию системы, поскольку система регулярного типа должна регулярно программировать.

Лично я жду, чтобы узнать, будет ли развиваться язык, который пытается решить все эти проблемы удобным образом. Однако я вообще не задумываюсь, почему такие вещи еще не существуют; это кровавый трудный комплекс проблем!