Фундепс и GADT:Когда проверка типов разрешима?

Question

Я читал исследовательскую работу о Haskell и о том, как реализован HList, и задавался вопросом, когда описанные методы разрешимы, а когда нет для средства проверки типов.Кроме того, поскольку с помощью GADT можно делать аналогичные вещи, мне было интересно, всегда ли разрешима проверка типов GADT.

Я бы предпочел цитаты, если они у вас есть, чтобы я мог прочитать/понять объяснения.

Спасибо!

Answer 1

Я считаю, что проверка типов GADT всегда разрешима;это неразрешимый вывод, поскольку он требует объединения более высокого порядка.Но программа проверки типа GADT — это ограниченная форма проверки доказательств, которую вы видите, например.Coq, где конструкторы создают доказательство.Например, классический пример внедрения лямбда-исчисления в GADT имеет конструктор для каждого правило сокращения, поэтому, если вы хотите найти нормальную форму термина, вы должны указать ему, какие конструкторы приведут вас к нему.Проблема остановки была передана в руки пользователя :-)

Answer 2

Вы, наверное, уже видели это, но в исследовательском центре Microsoft есть сборник статей по этой проблеме: Тип Проверка документов.Первый описывает разрешимый алгоритм, фактически используемый в компиляторе Glasgow Haskell.