Подтвердить что ты не робот

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

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

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

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

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

Ответ 1

Подробные сведения подробно описаны в работах Саймона Пейтона-Джонса, хотя для их понимания требуется много технических знаний. Если вы хотите прочитать документ о том, как работает вывод типа Haskell, вы должны прочитать об обобщенных типах алгебраических данных (GADT), которые объединяют экзистенциальные типы с несколькими другими функциями. Я предлагаю "Полный и разрешимый вывод типа для 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".