Блог

Я пытаюсь найти более элегантный способ написания следующего кода.

 class C c where
    type E c :: * -> *

class C c => A c where
    g :: E c a -> E c a

class (C c, A c) => D c where
    f :: E c a -> E c a

instance A c => D c where
    f = g
  

Это приводит к ошибке.

 Test.hs:58:9:
    Could not deduce (E c0 ~ E c)
    from the context (A c)
      bound by the instance declaration at Test.hs:57:10-19
    NB: `E' is a type function, and may not be injective
    Expected type: E c a
      Actual type: E c0 a
    Expected type: E c a -> E c a
      Actual type: E c0 a -> E c0 a
    In the expression: g
    In an equation for `f': f = g
Failed, modules loaded: none.
  

Мое текущее решение — добавить фиктивную переменную, из которой он может вывести
, какой конкретный C используется.

 class C c where
    type E c :: * -> *

class C c => A c where
    g_inner :: c -> E c a -> E c a
g = g_inner undefined

class (C c, A c) => D c where
    f_inner :: c -> E c a -> E c a
f = f_inner undefined

instance A c => D c where
    f_inner = g_inner
  

Я знаю, что это еще один случай, когда связанные типы не являются инъективными,
но я не могу в этом разобраться. Конечно, E может быть не инъективным, но,
похоже, где-то информация о том, что g будет работать с конкретным
(E c), на который ссылается класс D, была потеряна.

Любые объяснения и, что более важно, более эффективные обходные пути будут высоко оценены. Спасибо!

Редактировать

Хорошо, я вижу, что переключение type на data заставляет код работать.

Я пытаюсь понять, как это может работать. Каждый c создает новый тип данных E c . В контексте экземпляра мы должны forall a. ((E) c) a -> ((E) c) a соответствовать forall a. ((E) c) a -> ((E) c) a . Обозначая F = E c , мы затем сопоставляем forall a. F a -> F a с самим собой.

Мне трудно понять, где что-то нарушается в случае синонимов типов (связанных типов). Конечно, можно определить два экземпляра A , оба из которых имеют подпись (E c) a -> (E c) a . Но почему было бы неправильно использовать определение из экземпляра A c , который находится в области видимости?

Спасибо!!

Проблема E c a -> E c a в том, что компилятор просто не знает, какой экземпляр C выбрать.

Связанные семейства типов — это просто синонимы типов. Итак, класс

 class C c => A c where
    g :: E c a -> E c a
  

с точки зрения проверки типов также может быть

 class C c => A c where
    g :: m a -> m a
  

Поскольку переменная класса c не упоминается, нет способа определить, какой экземпляр словаря следует использовать для выбора функции. Хотя это связано с тем, что семейства типов не являются инъективными, я согласен, что из сообщения об ошибке не очевидно, что это проблема.

Использование семейства данных, как предлагает Даниэль Вагнер, может быть самым элегантным решением. Иногда мне удавалось инвертировать свои семейства типов, так что вместо того, чтобы получать E c для конкретного c , я вместо этого выбираю c на основе E c . В этом случае это дало бы:

 class E (e :: * -> *) where
    type C e :: *

class E e => A e where
    g :: e a -> e a

class (A e) => D e where
    f :: e a -> e a

instance A e => D e where
    f = g
  

В зависимости от того, что еще вы делаете, это может сработать для вас.

Если оставить в стороне эту проблему, наличие отдельного экземпляра не имеет особого смысла. Поскольку A доступно как ограничение суперкласса, вы можете просто установить f = g в качестве метода по умолчанию. Это будет намного меньше проблем; вы, вероятно, на самом деле не хотите instance D e where ... .