Функции записи в haskell, которые работают только с связанными типами

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

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, который находится в области видимости?

Спасибо!!

Ответ 1

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

Семейства ассоциированных типов - это просто синонимы типов. Таким образом, класс

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

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

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 ....