Условия Патерсона для проверки типов в Хаскеле - PullRequest
0 голосов
/ 21 февраля 2019

Может ли кто-нибудь объяснить (или дать мне несколько примеров или процесс), почему эти условия необходимы для прекращения процесса разрешения экземпляров в Haskell?Или, по крайней мере, ссылка, где описан этот алгоритм.

Например, я пытался найти какую-то лекцию об этом, но я могу найти только информацию о выводе типов, а не процесс разрешения этого экземпляра.

Я цитирую Руководство пользователя Haskell

Правила таковы:

  1. Условия Патерсона: для каждого ограничения класса (C t1 ... tn) в контексте
    1. Ни одна переменная типа не имеет большего числа вхождений в ограничении, чем в заголовке
    2. Ограничение имеет меньше конструкторов и переменных (взятых вместе и считающих повторы), чем заголовок
    3. Ограничениене упоминает никаких типов функций.Приложение функции типа в принципе может расширяться до типа произвольного размера и поэтому отклоняется из-под контроля
  2. Условие покрытия.Для каждой функциональной зависимости ⟨tvs⟩left -> ⟨tvs⟩ справа от класса каждая переменная типа в S(⟨tvs⟩right) должна появляться в S(⟨tvs⟩left), где S - это замена, отображающая каждую переменную типа в объявлении класса на соответствующий тип в экземпляреруководитель.
...