написание функций в haskell, которые работают только с ассоциированными типами - PullRequest
Новая
       30

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

12 голосов
/ 09 октября 2011

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

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 Ответ

8 голосов
/ 09 октября 2011

Проблема в том, что из 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 ....

...