Spec-Zone.ru › Haskell 9

6.4.25. Роли

Используя GeneralizedNewtypeDeriving (Обобщённые производные экземпляры для newtype), программист может взять существующие экземпляры классов и «поднять» их до экземпляров этого класса для newtype. Однако это не всегда безопасно. Например, рассмотрим следующее:

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.25.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.25.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.25.3. Аннотации ролей

RoleAnnotations
Начиная с:

7.8.1

Статус:

Включено в GHC2024

Разрешает синтаксис аннотаций ролей.

Иногда программисту нужно ограничить процесс вывода. Например, можно рассмотреть тип Set a, представляющий набор данных, упорядоченный согласно экземпляру Ord для a. Хотя обычно было бы безопасно с точки зрения типов считать, что a имеет представительскую роль, у newtype и его базового типа могут быть разные порядки, закодированные в соответствующих экземплярах Ord. Это привело бы к некорректному поведению во время выполнения. Поэтому автор типа данных Set может захотеть назначить его параметру номинальную роль. Для этого используется объявление

type role Set nominal

Аннотации ролей также можно использовать, если программист хочет создать класс с представительской (или фантомной) ролью. Однако, поскольку класс с неноминальными ролями может быстро привести к несогласованности экземпляров классов, для разрешения неноминальных ролей у классов необходимо также указать IncoherentInstances.

Аннотации ролей могут также понадобиться в файлах hs-boot (Взаимно рекурсивные модули и файлы hs-boot), где правые части определений можно опустить. Как обычно, типы и классы, объявленные в файле hs-boot, должны соответствовать определениям в файле hs, включая роли. В файлах hs-boot для типов данных по умолчанию используется представительская роль, что соответствует распространённому случаю.

Аннотации ролей разрешены в объявлениях data, newtype и class. Объявление аннотации роли начинается с type role, за которым следует список ролей для каждого параметра типа. (В это число параметров входят параметры, неявно заданные сигнатурой вида в объявлении data или 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

© 2002–2007 The University Court of the University of Glasgow. All rights reserved.
Licensed under the Glasgow Haskell Compiler License.
https://downloads.haskell.org/~ghc/9.14.1/docs/users_guide/exts/roles.html

Spec-Zone.ru

Настройки Оффлайн Что нового Помощь О нас
Spec-Zone .ru
спецификации, руководства, описания, API