Фундепс и ГАДЦ: когда разрешается проверка типов?

Question

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

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

Спасибо!

Answer 1

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

Answer 2

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