Fundeps и GADT: когда становится решаемой проверка типов?
Я читал исследовательскую статью о Haskell и о том, как реализован HList, и задавался вопросом, когда описанные методы являются, а когда нет, разрешимы для средства проверки типов. Кроме того, поскольку вы можете делать аналогичные вещи с GADT, мне было интересно, всегда ли проверка типа GADT разрешима.
Я бы предпочел цитаты, если они у вас есть, чтобы я мог читать / понимать объяснения.
Спасибо!
Я считаю такое отношение (что теоретические вопросы не имеют отношения к прагматическому форуму) вредно и устарело. Прагматические подходы должны быть открыты для новых технологий, потому что эти технологии, вероятно, могут улучшить повседневную деятельность в ближайшем будущем. например: функциональные возможности в C# / python.
Тем не менее, комментарий Чирса, вероятно, верен с практической точки зрения. Я бы хотел, чтобы этого не было.
Ркресвик: Я не думаю, что этот вопрос не имеет значения. Я просто не думаю, что сообщество Stack Overflow может дать удовлетворительный ответ.
Ответы 2
Вы, наверное, уже видели это, но в исследовании Microsoft есть сборник статей по этой проблеме: Тип Проверочные документы. Первый описывает разрешимый алгоритм, фактически используемый в компиляторе Glasgow Haskell.
Статьи, на которые есть ссылки, являются хорошими статьями, но, похоже, они не отвечают на мой вопрос.
Я считаю, что проверка типов GADT всегда разрешима; это вывод, который неразрешим, поскольку требует унификации более высокого порядка. Но средство проверки типа GADT - это ограниченная форма проверок проверки, которую вы видите, например. Coq, где конструкторы создают срок доказательства. Например, классический пример встраивания лямбда-исчисления в GADT имеет конструктор для каждого правило редукции, поэтому, если вы хотите найти нормальную форму термина, вы должны указать ему, какие конструкторы приведут вас к нему. Проблема с остановкой перешла в руки пользователя :-)
Неплохо подмечено. Так что я думаю, меня интересует, когда GHC-вывод типа GADT разрешим.
Этот вопрос лучше задать авторам исследования. Это немного эзотерично для Stack Overflow. (Мне всегда удавалось с большим успехом связываться с исследователями для получения комментариев. Обычно они в восторге, кто-нибудь читает их работы.)