Непонятное сообщение об ошибке с семействами типов

Я пытаюсь понять семьи типов без особого успеха. Вот минимальный пример:

{-# LANGUAGE TypeFamilies #-}

class Object obj where
  type Unit obj :: *
  unit :: Unit obj

instance (Object obj, Object obj') => Object (obj, obj') where
  type Unit (obj, obj') = (Unit obj, Unit obj')
  unit = (unit, unit)

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

Это дает мне:

objs.hs:10:10:
    Could not deduce (Unit obj' ~ Unit obj1)
    from the context (Object obj, Object obj')
      bound by the instance declaration at objs.hs:8:10-56
    NB: `Unit' is a type function, and may not be injective
    The type variable `obj1' is ambiguous
    Possible fix: add a type signature that fixes these type variable(s)
    Expected type: Unit (obj, obj')
      Actual type: (Unit obj0, Unit obj1)
    In the expression: (unit, unit)
    In an equation for `unit': unit = (unit, unit)
    In the instance declaration for `Object (obj, obj')'

Я попытался добавить сигнатуры типов:

unit = (unit :: Unit obj, unit :: Unit obj')

но это только ухудшает ситуацию.

Следующая модификация компилируется:

{-# LANGUAGE TypeFamilies #-}

class Object obj where
  type Unit obj :: *
  unit :: obj -> Unit obj

instance (Object obj, Object obj') => Object (obj, obj') where
  type Unit (obj, obj') = (Unit obj, Unit obj')
  unit (o, o') = (unit o, unit o')

но мне не нравится лишний аргумент для unit.

Можно ли определить без аргумента unit?

Ответы

Ответ 1

То, что вы пытаетесь сделать, сложно для GHC, потому что, как говорит GHC в сообщении об ошибке, типам семейств действительно не нужно быть инъективными.

Что означает инъективность?

Функция типа F называется инъективной, если F x ~ F y означает x ~ y. Если F является конструктором нормального типа, определенным через data, тогда это всегда верно. Однако для семейств типов это не выполняется.

Например, нет никаких проблем при определении следующих экземпляров, учитывая ваше определение Object:

instance Object Int where
  type Unit Int = Int
  unit = 0

instance Object Char where
  type Unit Char = Int
  unit = 1

Теперь, если вы пишете unit :: Int, то как GHC может определить, следует ли оценивать его до 0 или 1? Даже запись unit :: Unit Int делает это более понятным, потому что

Unit Int ~ Int ~ Unit Char

поэтому все три типа должны быть взаимозаменяемыми. Поскольку Unit не гарантируется быть инъективным, просто невозможно однозначно заключить из знания Unit x знание x...

Следствием является то, что Unit можно определить, но не использовать.

Решение 1: аргументы Dummy или proxy

Вы указали наиболее распространенный способ исправления этой проблемы. Добавьте аргумент, который помогает GHC фактически определить аргумент типа, о котором идет речь, путем изменения сигнатуры типа на

unit :: obj -> Unit obj

или

unit :: Proxy obj -> Unit obj

для подходящего определения Proxy, например просто

data Proxy a

Решение 2: Ручная проверка обратимости

Возможно, менее известный вариант заключается в том, что вы можете фактически доказать GHC, что ваша функция типа обратима.

Способ сделать это - определить семейство обратного типа

type family UnUnit obj :: *

и сделать обратимость суперклассовым ограничением класса типа:

class (UnUnit (Unit obj) ~ obj) => Object obj where
  type Unit obj :: *
  unit :: Unit obj

Теперь вам нужно сделать дополнительную работу. Для каждого экземпляра класса необходимо определить фактический инверсный Unit правильно. Например,

instance (Object obj, Object obj') => Object (obj, obj') where
  type Unit (obj, obj') = (Unit obj, Unit obj')
  unit = (unit, unit)

type instance UnUnit (obj, obj') = (UnUnit obj, UnUnit obj')

Но с учетом этой модификации определение typechecks. Теперь, если GHC встречает вызов Unit в определенном типе T и хочет определить тип S, такой как Unit S ~ T, он может применить ограничение суперкласса, чтобы сделать вывод, что

S ~ UnUnit (Unit S) ~ UnUnit T

Если бы мы попытались определить неверные экземпляры, как указано выше, для Object Int и Object Char, которые оба отображают Unit Int и Unit Char как Int, это не сработает, потому что мы должны решить, должно ли UnObject Int быть Int или Char, но не могло иметь обоих...

Ответ 2

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

class Valuable o where
  type Value o :: *
  value :: Value o

data Pearl
data Diamond

instance Valuable Pearl where
  type Value Pearl = Int
  value = 1000

instance Valuable Diamond where
  type Value Diamond = Int
  value = 10000

Обратите внимание, что Value a ~ Value b не подразумевает a ~ b, поскольку оно имеет инъективность. Таким образом, теперь он двусмыслен относительно того, что такое значение value. Это даже не помогает, если мы сжимаем тип value :: Int с Value Pearl ~ Value Diamond ~ Int.

Тем не менее, в коде есть очень приятный parallelism.

import Control.Arrow

class Object obj where
  type Unit obj :: *
  unit :: obj -> Unit obj

instance (Object obj, Object obj') => Object (obj, obj') where
  type Unit (obj, obj') = (Unit obj, Unit obj')
  unit = unit *** unit