Перекрывающиеся многопараметрические экземпляры и специфичность экземпляров

Question

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
module OverlappingSpecificsError where

class EqM a b where
    (===) :: a -> b -> Bool

instance {-# OVERLAPPABLE #-} Eq a => EqM a a where
    a === b = a == b

instance {-# OVERLAPPABLE #-} EqM a b where
    a === b = False

aretheyreallyeq :: (Eq a, Eq b) => Either a b -> Either a b -> Bool
aretheyreallyeq (Left a1) (Right b2) = a1 == b2

aretheyeq :: (Eq a, Eq b) => Either a b -> Either a b -> Bool
aretheyeq (Left a1) (Right b2) = a1 === b2

Не компилируется ни aretheyreallyeq, ни aretheyeq, но ошибка для aretheyreallyeq имеет для меня смысл, а также говорит, что aretheyeq не должно выдавать ошибку: один из примеров, который предлагает GHCi, возможно для EqM в aretheyeq должно быть невозможно из-за той же ошибки на aretheyreallyeq. Что происходит?

Дело в том, что GHCi настаивает на том, что оба экземпляра EqM применимы в aretheyeq. Но a1 относится к типу a, а b2 относится к типу b, поэтому для того, чтобы первый экземпляр был применим, он должен иметь типы a и b unify.

Но это не должно быть возможным, поскольку они объявляются как переменные типа в сигнатуре функции (то есть использование первого экземпляра EqM приведет к возникновению функции типа Either a a -> Either a a -> Bool, а ошибка в aretheyreallyeq говорит мне, что GHCi не допустит этого (что я и ожидал).

Я что-то упустил, или это ошибка в проверке перекрывающихся экземпляров с классами многопараметрических типов?

Я думаю, может быть, это связано с тем фактом, что a и b могут быть позже созданы, до точки, где они равны, вне aretheyeq, а затем в первом экземпляре будет действительным? Но то же самое верно для aretheyreallyeq. Единственное отличие состоит в том, что если они не объединяются, у нас есть опция для aretheyeq, но мы не для aretheyreallyeq. В любом случае Haskell делает не иметь динамическую c рассылку по множеству веских и очевидных причин, так в чем же опасение при совершении экземпляра, который всегда будет работать независимо от того, будут ли впоследствии a и b разборчивы? Может быть, есть какой-то способ представить это, что позволило бы каким-либо образом сделать выбор экземпляра при вызове функции?

Стоит отметить, что если я удаляю второй экземпляр, то функция, очевидно, все равно не компилируется, заявляя, что экземпляр EqM a b не может быть найден. Так что, если у меня нет этого экземпляра, то ни один не работает, но когда тот работает, вдруг другой тоже, и у меня перекрытие? Пахнет мне жуком за много миль.

Answer 1

Соответствие экземпляров для переменных * generic c работает таким образом, чтобы предотвратить некоторые потенциально запутанные (и опасные) сценарии ios.

Если компилятор поддался вашей интуиции и выбрал EqM a b Например, при компиляции aretheyeq (поскольку a и b не обязательно объединяют, как вы говорите), следующий вызов:

x = aretheyeq (Left 'z') (Right 'z')

вернет False, что противоречит интуиции .

Q : подождите секунду! Но в этом случае a ~ Char и b ~ Char, и у нас также есть Eq a и Eq b, что означает Eq Char, что должно позволить выбрать экземпляр EqM a a, не так ли?

Ну, да, я полагаю, что может происходить в теории, но Haskell просто так не работает. Экземпляры класса - это просто дополнительные параметры, передаваемые в функции (как словари методов), поэтому для того, чтобы существовал экземпляр, он должен быть однозначно выбран внутри самой функции, или , который должен быть передан из Потребитель.

Первый (однозначно выбираемый экземпляр) обязательно требует наличия только одного экземпляра. И действительно, если вы удаляете экземпляр EqM a a, ваша функция компилируется и всегда возвращает False.

Последнее (передача экземпляра от потребителя) означает ограничение на функцию, например:

aretheyeq :: EqM a b => Either a b -> Either a b -> Bool

Что вы спрашиваете, так это то, что Haskell по существу имеет две разные версии этой функции: одна требует a ~ b и выбирает экземпляр EqM a a, а другая не требует этого и выбирает EqM a b экземпляр.

И тогда компилятор ловко выберет «правильную» версию. Так что если я вызываю aretheyeq (Left 'z') (Right 'z'), вызывается первая версия, а если я звоню aretheyeq (Left 'z') (Right 42) - вторая.

Но теперь подумайте дальше: есть ли две версии aretheyeq и какая выбор зависит от того, равны ли типы, а затем подумайте:

dummy :: a -> b -> Bool
dummy a b = aretheyeq (Left a) (Right b)

Как dummy узнает, какую версию aretheyeq выбрать? Так что теперь должно быть две версии dummy: одна для случая a ~ b и другая для других случаев.

И так далее. Эффект пульсации продолжается, пока не появятся конкретные типы.

Q : подождите секунду! Почему две версии? Разве не может быть только одной версии, которая затем решает, что делать, основываясь на том, в какие аргументы передаются?

Ах, но это невозможно! Это потому, что типы стираются во время компиляции. К тому времени, когда функция начинает работать, она уже скомпилирована, и информации о типе больше нет. Таким образом, все должно быть решено во время компиляции: какой экземпляр выбрать, и волновой эффект от него.

Answer 2

Это не ошибка в смысле работы точно так, как задокументировано . Начиная с

Теперь предположим, что в некотором клиентском модуле мы ищем экземпляр целевого ограничения (C ty1 .. tyn). Поиск работает так:

Первый этап поиска вариантов-кандидатов работает так, как вы ожидаете; EqM a b является единственным кандидатом и, следовательно, главным кандидатом. Но последний шаг -

Теперь найдите все экземпляры или заданные ограничения в области, которые объединяются с целевым ограничением, но не совпадают с ним. Такие экземпляры, не являющиеся кандидатами, могут совпадать при дальнейшем создании целевого ограничения. Если все они являются непоследовательными экземплярами верхнего уровня, поиск завершается успешно, возвращая основного кандидата. В противном случае поиск завершится неудачей.

Экземпляр EqM a a попадает в эту категорию и не является непоследовательным, поэтому поиск не выполняется. И вы можете добиться желаемого поведения, пометив его как {-# INCOHERENT #-} вместо перекрывающегося.

Answer 3

Чтобы дополнительно завершить ответ Алексея, который действительно дал мне подсказку о том, что я должен сделать, чтобы добиться желаемого поведения, я скомпилировал следующий минимальный рабочий пример немного другой ситуации, более похожей на мой реальный вариант использования (который должен делать с ExistentialQuantification):

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ExistentialQuantification #-}
module ExistentialTest where

class Class1 a b where
    foo :: a -> b

instance {-# INCOHERENT #-} Monoid a => Class1 a (Either b a) where
    foo x = Right (x <> x)

instance {-# INCOHERENT #-} Monoid a => Class1 a (Either a b) where
    foo x = Left x

data Bar a = Dir a | forall b. Class1 b a => FromB b

getA :: Bar a -> a
getA (Dir a) = a
getA (FromB b) = foo b

createBar :: Bar (Either String t)
createBar = FromB "abc"

createBar2 :: Bar (Either t String)
createBar2 = FromB "def"

Если вы удалите аннотации {-# INCOHERENT #-}, вы получите те же ошибки компиляции, что и в моем исходном примере как для createBar, так и createBar2, и точка то же самое: в createBar ясно, что единственным подходящим экземпляром является второй, тогда как в createBar2 единственным подходящим является первый, но Haskell отказывается компилировать из-за этой очевидной путаницы, которую он может создать, когда используя его, , пока вы не аннотируете их INCOHERENT.

И затем код работает точно так, как вы ожидаете: getA createBar возвращает Left "abc", тогда как getA createBar2 возвращает Right "defdef", что является единственной вещью, которая может произойти в разумной системе типов.

Итак, мой вывод: аннотация INCOHERENT предназначена именно для Что бы я хотел сделать с самого начала, без Haskell жалоб на потенциально запутанные случаи и действительно на выбор единственного, который имеет смысл. Остается сомнение в том, может ли INCOHERENT сделать так, чтобы экземпляры, которые действительно остаются перекрывающимися, даже после учета всего компилируемого, используя произвольный (который, очевидно, плох и опасен). Итак, вывод к моему выводу таков: используйте INCOHERENT только тогда, когда вам абсолютно необходимо и абсолютно убеждены, что действительно есть только один действительный экземпляр.

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

Answer 4

aretheyreallyeq терпит неудачу, потому что в области видимости есть две переменные типа. В

aretheyreallyeq :: (Eq a, Eq b) => Either a b -> Either a b -> Bool
aretheyreallyeq (Left a1) (Right b2) = a1 == b2

a1 :: a и b2 :: b нет метода для сравнения значений потенциально разных типов (так как они объявлены), поэтому это не получается. Это, конечно, не имеет ничего общего ни с одним из включенных расширений или прагм.

aretheyeq терпит неудачу, потому что есть два случая, которые могут соответствовать, а не то, что они определенно делают. Я не уверен, какую версию GH C вы используете, но вот сообщение об исключении, которое я вижу, и оно мне кажется достаточно ясным:

    • Overlapping instances for EqM a b arising from a use of ‘===’
      Matching instances:
        instance [overlappable] EqM a b -- Defined at /home/tmp.hs:12:31
        instance [overlappable] Eq a => EqM a a
          -- Defined at /home/tmp.hs:9:31
      (The choice depends on the instantiation of ‘a, b’
       To pick the first instance above, use IncoherentInstances
       when compiling the other instance declarations)
    • In the expression: a1 === b2
      In an equation for ‘aretheyeq’:
          aretheyeq (Left a1) (Right b2) = a1 === b2

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