Повторные тивары в экземплярах голов: привязка или ссылка? - PullRequest
Новая
       19

Повторные тивары в экземплярах голов: привязка или ссылка?

2 голосов
/ 19 июня 2019

Моя ментальная модель голов экземпляров - это сопоставление с образцом на уровне типов с привязкой тиваров, как связывание переменных. С FlexibleInstances вы можете повторять tyvars в экземплярах голов. Но вы не можете сделать это на уровне терминов. Рассмотрим 

class (Eq a, Eq b) => C a b  where
  foo :: a -> b -> String

instance C a a  where              -- repeated `a'
  -- the args are same type so we can compare them
  foo ...   = "equal"              -- see below
  foo _x _y = "not equal"

instance {-# OVERLAPPABLE #-} C a b  where
  foo _  _  = "not comparable"

Для этого "equal" случая я бы хотел написать 

foo  x   x  = "equal"

Но повторяющиеся переменные недопустимы в шаблонах: отклонено Conflicting definitions for 'x'. И это потому, что каждая переменная должна быть однозначно связана с аргументами foo , тогда мы можем ссылаться на них. Вместо этого идите 

foo  x   y  | x == y = "equal"

Так почему же повторный тыварский бизнес работает на примерах? В instance C a a, какой из a s является сайтом связывания, какой ссылочный сайт? Делает ли компилятор под прикрытием что-то эквивалентное связыванию с тиварами с разными именами и затем применяет охрану?

1 Ответ

1 голос
/ 22 июня 2019

Выбор экземпляра в основном происходит в ghc/compiler/types/InstEnv.hs, и в нем используется «сопоставление», ограниченная форма объединения, где шаблон с переменными объединяется с другим типом путем замены этих переменных шаблона.

Итак, когдаGHC решает, что ему нужен словарь экземпляров для C Int Int, он пытается сопоставить / объединить C Int Int с шаблонами C a a и C a b в этом порядке (т. Е. Путем определения путем применения функции tcMatchTys из ghc/compiler/types/Unify.hs если есть замена для переменных a и / или b, которая позволяет одному из этих шаблонов соответствовать C Int Int).

Это деталь реализации в tcMatchTys, но она выглядитдля меня, как C Int Int будет соответствовать шаблону C a a путем привязки a к Int на основе первого a и последующей проверки того, что a связан с Int на основе второго a, поэтому я предполагаю, что первый a является сайтом привязки, а второй a является ссылочным сайтом, хотя было бы точнее сказать, что они оба объединены / совпадаютсайты.Семантика не изменится, если вы измените порядок.

После этого процесса сопоставления происходит обработка перекрывающихся экземпляров.Полный список подходящих шаблонов генерируется и затем складывается в insert_overlapping в lookupInstEnv: 

-- in function `lookupInstEnv`, file `InstEnv.hs`
final_matches = foldr insert_overlapping [] all_matches

Функция insert_overlapping отфильтровывает строго более общие случаи, где разрешено перекрытие (а также обрабатывает несогласованныеэкземпляры).Затем окончательный список сопоставляется с одноэлементным списком, и это ошибка, если совпадает либо ноль, либо несколько шаблонов.

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

gack :: [t] -> String
gack xs = foo xs xs

использует тот же процесс сопоставления, чтобы определить, что C [t] [t] соответствует шаблону C a a при замене a := [t].(Это также соответствует C a b при заменах a := [t], b := [t], но доминирующее совпадение выигрывает.)

...