Блог

 {-# LANGUAGE EmptyDataDecls #-}
module Main where

main :: IO ()
main = pure ()

data P a = P Int 
data D1
data D2

class C a where
instance C D1 where
instance C D2 where

mkP_D1 :: Int -> P D1
mkP_D1 = P

mkP_D2 :: Int -> P D2
mkP_D2 = P

ps :: C a => [P a]
ps = [mkP_D1 1, mkP_D2 2] 

qs :: Num a => [a]
qs = [1, 2]
 

выдает ошибку компилятора

• Не удалось сопоставить тип » a » с » D1 «» a » — это жесткая переменная типа, связанная сигнатурой типа для: ps :: для всех a. C a => [P a]

  Ожидаемый тип: P a Фактический тип: P D1

• В выражении: mkP_D1 1 В выражении: [mkP_D1 1, mkP_D2 2] В уравнении для «ps»: ps = [mkP_D1 1, mkP_D2 2]
• Соответствующие привязки включают ps :: [P a]

  строка 22: ps = [mkP_D1 1, mkP_D2 2]

Почему это qs работает нормально, но все же ps не работает?

Я постараюсь дать некоторую интуицию, немного упростив ситуацию.

ps :: C a => [P a] является договором между реализацией ps и ее пользователем. В соответствии с этим,

• пользователь может выбрать любой a
• пользователь должен доказать, что C a имеет
• затем реализация должна предоставить значение типа [P a] .

Например, пользователь может выбрать a ~ D1 . Затем экземпляр используется для доказательства C D1 , чтобы договор был выполнен. В этом случае реализация должна предоставить значение типа [P D1] .

Ваша реализация такова [mkP_D1 1, mkP_D2 2] . В приведенном выше случае значение mkP_D1 1 следует за контрактом, поскольку оно равно a P D1 . Однако mkP_D2 2 не является P D1 (но является P D2 ), нарушающим контракт.

Поскольку существует экземпляр, в котором пользователь выполняет контракт, но реализация не выполняет, код отклоняется проверкой типов.

Более педантично, проблема здесь в том, что a выбирается пользователем, а не реализация. Если реализация попытается выбрать какой-то определенный тип a , есть вероятность, что пользователь выберет что-то другое, и компилятор в этом случае будет справедливо жаловаться.

Почему это прекрасно qs работает?

 qs :: Num a => [a]
qs = [1, 2]
 

Здесь пользователь выбирает a , но qs не делает этого. Действительно, 1 имеет любой (числовой) тип a , и это так 2 .

Сравните это с ps тем , который пытается выбрать a . Кстати, ps не только пытается выбрать a быть D1 (что уже вызовет ошибку «жесткой переменной»), но и пытается выбрать a быть D2 (что делает ситуацию еще хуже).

Возможной рабочей реализацией является добавление метода в класс:

 class C a where
  mkP :: Int -> P a

instance C D1 where
  mkP = P

instance C D2 where
  mkP = P

ps :: C a => [P a]
ps = [mkP 1, mkP 2] 
 

Обратите внимание, что это только пример. Вы можете использовать P напрямую и не вводить новый метод в класс.

Все элементы списка должны иметь один и тот же тип. qs работает, потому что все его элементы имеют один и тот же тип a . ps не работает, потому что его первый элемент имеет тип P D1 , а второй элемент имеет тип P D2 . Разных типов. Ничего не поделаешь.

Из комментариев стало очевидно, что на самом деле вы ищете, чтобы каждое значение имело другое Dx значение и имело свое собственное ограничение C . Чтобы достичь этого, заверните его в GADT:

 data PP where
  PP :: forall a. C a => P a -> PP

ps :: [PP]
ps = [PP (mkP_D1 1), PP (mkP_D2 2)]
 

Здесь конструктор PP упаковывает в него не только значение P a , но также тип a и соответствующее ему ограничение C a .

В: Оооо, но это так неудобно! Я должен обернуть каждую ценность в PP ! Неужели я не могу обойтись без этого?

Короткий ответ — нет, вы не можете. Как указывалось ранее, все элементы списка должны иметь один и тот же тип, точку. И если вы хотите поместить туда разные типы, вам нужно как-то обернуть их различия, чтобы они больше не были видны.