Используя GeneralizedNewtypeDeriving (Обобщенные производные экземпляры для newtypes), программист может взять существующие экземпляры классов и «поднять» их в экземпляры этого класса для нового типа. Однако это не всегда безопасно. Например, рассмотрим следующее:
newtype Age = MkAge { unAge :: Int }
type family Inspect x
type instance Inspect Age = Int
type instance Inspect Int = Bool
class BadIdea a where
bad :: a -> Inspect a
instance BadIdea Int where
bad = (> 0)
deriving instance BadIdea Age -- not allowed!
Если бы производный экземпляр был разрешен, каким был бы тип его метода bad? Похоже, это было бы Age -> Inspect Age, что эквивалентно Age -> Int, согласно семейству типов Inspect. Однако, если мы просто адаптируем реализацию из экземпляра для Int, реализация для bad создает Bool, и у нас возникают трудности.
Способ определить такие ситуации — назначить роли переменным типов для типов данных, классов и синонимов типов.
Роли, как реализованы в GHC, представляют собой упрощенную версию работы, описанной в Generative type abstraction and type-level computation, опубликованной на POPL 2011.
6.4.24.1. Номинальная, представительная и фантомная
Цель системы ролей — отслеживать, когда два типа имеют одинаковое базовое представление. В приведенном выше примере Age и Int имеют одинаковое представление. Но соответствующие экземпляры BadIdea не будут иметь одинаковое представление, поскольку типы реализаций bad будут разными.
Предположим, у нас есть два использования конструктора типа, каждый из которых применяется к тем же параметрам, за исключением одного различия. (Например, T Age Bool c и T Int Bool c для некоторого типа T.) Роль параметра типа указывает, что нам нужно знать о двух отличающихся аргументах типа, чтобы знать, что два внешних типа имеют одинаковое представление (в примере, что должно быть истинно для Age и Int для демонстрации того, что T Age Bool c имеет такое же представление, как T Int Bool c).
GHC поддерживает три различные роли для параметров типа: номинальную, представительную и фантомную. Если параметр типа имеет номинальную роль, то два отличающихся типа фактически не должны отличаться: они должны быть идентичными (после сокращения семейства типов). Если параметр типа имеет представительную роль, то два типа должны иметь одинаковое представление. (Если роль первого параметра T — представительная, то T Age Bool c и T Int Bool c будут иметь одинаковое представление, потому что Age и Int имеют одинаковое представление.) Если параметр типа имеет фантомную роль, то нам не нужна дополнительная информация.
Вот несколько примеров:
data Simple a = MkSimple a -- a has role representational type family F type instance F Int = Bool type instance F Age = Char data Complex a = MkComplex (F a) -- a has role nominal data Phant a = MkPhant Bool -- a has role phantom
Тип Simple имеет свой параметр с представительной ролью, что, как правило, является наиболее распространенным случаем. Simple Age будет иметь такое же представление, как Simple Int. Тип Complex, с другой стороны, имеет свой параметр с номинальной ролью, потому что Complex Age и Complex Int не одинаковы. Наконец, Phant Age и Phant Bool имеют одинаковое представление, даже если Age и Bool не связаны.
6.4.24.2. Вывод ролей
Какой роль должен иметь данный параметр типа? GHC выполняет вывод ролей, чтобы определить правильную роль для каждого параметра. Он начинает с нескольких базовых фактов: (->) имеет два параметра с представительной ролью; (~) имеет два параметра с номинальной ролью; все параметры семейств типов — номинальные; и все параметры типа GADT — номинальные. Затем эти факты распространяются на все места, где используются эти типы. По умолчанию роль для типов данных и синонимов — фантомная; по умолчанию роль для классов — номинальная. Таким образом, для типов данных и синонимов любые параметры, не используемые в правой части (или используемые только в других типах в фантомных позициях), будут фантомными. Всякий раз, когда параметр используется в представительной позиции (то есть используется в качестве аргумента типа конструктору, соответствующая переменная которого имеет представительную роль), его роль повышается с фантомной до представительной. Аналогично, когда параметр используется в номинальной позиции, его роль повышается до номинальной. Мы никогда не понижаем роль с номинальной на фантомную или представительную, или с представительной на фантомную. Таким образом, мы выводим наиболее общую роль для каждого параметра.
Классы имеют роль по умолчанию — номинальная, чтобы способствовать связности экземпляров класса. Если бы C Int хранилось в типе данных, было бы очень плохо, если бы это каким-то образом изменилось на C Age где-то, особенно если другой C Age был объявлен!
Существует один особенно сложный случай, который следует объяснить:
data Tricky a b = MkTricky (a b)
Какими должны быть роли Tricky? На первый взгляд, кажется, что и a и b должны иметь роль представительную, поскольку оба используются в правой части и ни один из них не участвует в семействе типов. Однако это будет неправильно, как показывает следующий пример:
data Nom a = MkNom (F a) -- type family F from example above
Является ли Tricky Nom Age представлением Tricky Nom Int? Нет! Первый хранит Char, а второй — Bool. Решение заключается в том, чтобы потребовать, чтобы все параметры переменных типа имели номинальную роль. Таким образом, GHC выведет роль представительную для a и номинальную для b.
6.4.24.3. Аннотации ролей
-
RoleAnnotations -
- Since:
-
7.8.1
- Status:
-
Включено в
GHC2024
Разрешить синтаксис аннотаций ролей.
Иногда программист хочет ограничить процесс вывода. Например, мы можем рассмотреть тип Set a, который представляет собой набор данных, упорядоченных по экземпляру a Ord. Хотя в целом безопасно считать, что a имеет представительную роль, возможно, что у newtype и его базового типа разные порядки, закодированные в их соответствующих экземплярах Ord. Это приведет к некорректной работе во время выполнения. Поэтому автор типа данных Set хотел бы, чтобы его параметр имел номинальную роль. Это можно сделать с объявлением
type role Set nominal
Аннотации ролей также могут быть использованы, если программист хочет написать класс с представительной (или фантомной) ролью. Однако, поскольку класс с неноминальными ролями может быстро привести к несогласованности экземпляров класса, необходимо также указать IncoherentInstances, чтобы разрешить неноминальные роли для классов.
Другое место, где могут потребоваться аннотации ролей, — в файлах hs-boot (Взаимно рекурсивные модули и файлы hs-boot), где правые части определений могут быть пропущены. Как обычно, типы/классы, объявленные в файле hs-boot , должны совпадать с определениями в файле hs , в том числе до ролей. По умолчанию роль для типов данных — представительная в файлах hs-boot , что соответствует общему случаю использования.
Аннотации ролей разрешены в объявлениях данных, newtype и классов. Объявление аннотации роли начинается с type role и за ним следует один список ролей для каждого параметра типа. (Этот счетчик параметров включает параметры, неявно указанные сигнатурой типа в объявлении типа данных или newtype в стиле GADT). Каждый список ролей представляет собой роль (nominal, representational, или phantom), или _. Использование _ означает, что GHC должен вывести эту роль. Аннотация роли может быть расположена где угодно в том же модуле, что и определение типа данных или класса (похоже на сигнатуру типа на уровне значений). Вот несколько примеров:
type role T1 _ phantom data T1 a b = MkT1 a -- b is not used; annotation is fine but unnecessary type role T2 _ phantom data T2 a b = MkT2 b -- ERROR: b is used and cannot be phantom type role T3 _ nominal data T3 a b = MkT3 a -- OK: nominal is higher than necessary, but safe type role T4 nominal data T4 a = MkT4 (a Int) -- OK, but nominal is higher than necessary type role C representational _ -- OK, with -XIncoherentInstances class C a b where ... -- OK, b will get a nominal role type role X nominal type X a = ... -- ERROR: role annotations not allowed for type synonyms
