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