Экзистенциальное количественное определение Haskell в деталях

Question

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

Вопрос: Есть ли какие-нибудь хорошие ресурсы, объясняющие, как экзистенциальная количественная оценка реализована в GHC? * 1007 Т.е. *

• Как работает унификация на экзистенциальных типах - что можно унифицировать, а что нет?
• В каком порядке выполняются последующие операции над типами?

Моя цель - лучше понять сообщения об ошибках, которые выдает мне GHC. Сообщения обычно говорят что-то вроде "this type using forall and this other type don't match", однако они не объясняют, почему это так.

Answer 1

Мельчайшие подробности описаны в статьях Саймона Пейтона-Джонса, хотя для их понимания требуется немало технических знаний. Если вы хотите прочитать статью о том, как работает вывод типов из Haskell, вам следует прочитать об обобщенных алгебраических типах данных (GADT), которые сочетают экзистенциальные типы с рядом других функций. Я предлагаю «Полный и разрешаемый вывод типа для ГАДЦ», в списке статей на http://research.microsoft.com/en-us/people/simonpj/.

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

data Univ a = Univ a
data Exis = forall a. Exis a

toUniv :: a -> Univ a
toUniv = Univ

toExis :: a -> Exis
toExis = Exis

useUniv :: (a -> b) -> Univ a -> b
useUniv f (Univ x) = f x

useExis :: (forall a. a -> b) -> Exis -> b
useExis f (Exis x) = f x

Во-первых, обратите внимание, что toUniv и toExis почти одинаковы. У них обоих есть параметр свободного типа a, потому что оба конструктора данных полиморфны. Но хотя a появляется в типе возврата toUniv, оно не появляется в типе возврата toExis. Когда дело доходит до ошибок типа, которые вы можете получить, используя конструктор данных, между экзистенциальными и универсальными типами нет большой разницы.

Во-вторых, обратите внимание на тип ранга 2 forall a. a -> b в useExis. Это большая разница в выводе типов. Экзистенциальный тип, взятый из сопоставления с шаблоном (Exis x), действует как дополнительная скрытая переменная типа, передаваемая в тело функции, и его нельзя объединять с другими типами. Чтобы сделать это более понятным, вот несколько неправильных объявлений двух последних функций, в которых мы пытаемся объединить типы, которые не должны быть объединены. В обоих случаях мы принудительно объединяем тип x с не связанной переменной типа. В useUniv переменная типа является частью типа функции. В useExis это экзистенциальный тип из структуры данных.

useUniv' :: forall a b c. (c -> b) -> Univ a -> b
useUniv' f (Univ x) = f x -- Error, can't unify 'a' with 'c'
                          -- Variable 'a' is there in the function type

useExis' :: forall b c. (c -> b) -> Exis -> b
useExis' f (Exis x) = f x -- Error, can't unify 'a' with 'c'.
                          -- Variable 'a' comes from the pattern "Exis x",
                          -- via the existential in "data Exis = forall a. Exis a".