6.4.9.2. Семейства синонимов
Семейства типов представлены в трех вариантах: (1) они могут быть определены как открытые семейства на верхнем уровне, (2) они могут быть определены как закрытые семейства на верхнем уровне или (3) они могут появляться внутри типов классов (в этом случае они известны как связанные синонимы типов). Семейства на верхнем уровне более общие, так как не требуют совпадения индексов типов с параметрами класса. Однако связанные синонимы типов могут привести к более структурированному коду и предупреждениям компилятора, если некоторые экземпляры типов были - возможно, случайно - опушены. В дальнейшем мы всегда сначала обсудим общие формы на верхнем уровне, а затем рассмотрим дополнительные ограничения, наложенные на связанные типы. Обратите внимание, что закрытые связанные синонимы типов не существуют.
6.4.9.2.1. Декларации семейств типов
Открытые индексированные семейства типов вводятся с помощью сигнатуры, например
type family Elem c :: Type
Специальный family отличает семейства от стандартных деклараций типов. Аннотация вида результата необязательна и, как обычно, по умолчанию равна Type при ее отсутствии. Пример:
type family Elem c
Параметры также могут быть заданы с явными сигнатурами вида, если это необходимо. Мы называем количество параметров в декларации семейства типов арифметикой семейства, и все применения семейства типов должны быть полностью насыщены относительно этой арифметики. Это требование отличается от обычных синонимов типов, и это подразумевает, что вид семейства типов недостаточен для определения арифметики семейства и, следовательно, вообще недостаточен для определения того, является ли применение семейства типов корректным. В качестве примера рассмотрим следующую декларацию:
type family F a b :: Type -> Type
-- F's arity is 2,
-- although its overall kind is Type -> Type -> Type -> Type
Учитывая эту декларацию, вот примеры корректных и некорректных типов:
F Char [Int] -- OK! Kind: Type -> Type
F Char [Int] Bool -- OK! Kind: Type
F IO Bool -- WRONG: kind mismatch in the first argument
F Bool -- WRONG: unsaturated application
Аннотация вида результата необязательна и по умолчанию равна Type (как и виды аргументов) при ее отсутствии. Поливидные семейства типов могут быть объявлены с помощью параметра в аннотации вида:
type family F a :: k
В этом случае параметр вида k фактически является неявным параметром семейства типов.
В месте определения арифметика определяет, какие входные данные могут быть сопоставлены:
data PT (a :: Type)
type family F1 :: k -> Type
type instance F1 = PT
-- OK, 'k' can be matched on.
type family F0 :: forall k. k -> Type
type instance F0 = PT
-- Error:
-- • Expected kind ‘forall k. k -> Type’,
-- but ‘PT’ has kind ‘Type -> Type’
-- • In the type ‘PT’
-- In the type instance declaration for ‘F0’
Оба F1 и F0 имеют вид forall k. k -> Type, но их арифметика отличается.
В местах использования арифметика определяет, может ли определение использоваться в сценарии высшего порядка:
type HRK (f :: forall k. k -> Type) = (f Int, f Maybe, f True)
type H1 = HRK F0 -- OK
type H2 = HRK F1
-- Error:
-- • Expected kind ‘forall k. k -> Type’,
-- but ‘F1’ has kind ‘k0 -> Type’
-- • In the first argument of ‘HRK’, namely ‘F1’
-- In the type ‘HRK F1’
-- In the type declaration for ‘H2’
Это следствие требования, чтобы все применения семейства типов были полностью насыщены относительно их арифметики.
6.4.9.2.2. Декларации экземпляров типов
Декларации экземпляров семейств типов очень похожи на стандартные декларации синонимов типов. Единственные два отличия заключаются в том, что ключевое слово type следует за instance и что некоторые или все аргументы типов могут быть типами без переменных, но не могут содержать типов forall или семейств синонимов типов. Однако семейства данных, как правило, разрешены, а синонимы типов разрешены, только если они полностью применены и раскрыты до типа, который допустим — это те же самые требования, что и для экземпляров данных. Например, экземпляр [e] для Elem это
type instance Elem [e] = e
Аргументы типов можно заменить подчеркиванием (_), если имена аргументов не имеют значения. Это то же самое, что писать переменные типа с уникальными именами. Неиспользуемые аргументы типов можно заменить или префиксровать подчеркиванием, чтобы избежать предупреждений, когда включен флаг -Wunused-type-patterns. Применяются те же правила, что и для Деклараций экземпляров данных.
Также так же, как и для Деклараций экземпляров данных, при включении ExplicitForAll переменные типа и вида могут быть явно связаны в декларации экземпляра типа.
Декларации экземпляров семейств типов допустимы только при наличии соответствующей декларации семейства в области видимости — так же, как экземпляры классов требуют видимости декларации класса. Более того, каждая декларация экземпляра должна соответствовать виду, определяемому его декларацией семейства, и количество параметров типа в декларации экземпляра должно совпадать с количеством параметров типа в декларации семейства. Наконец, правая часть экземпляра типа должна быть монотипом (т. е. она не может включать forall), и после расширения всех насыщенных синонимов типов vanilla, никаких синонимов, кроме синонимов семейств, не должно остаться.
6.4.9.2.3. Закрытые семейства типов
Семейство типов также можно объявить с помощью where-записи, определяющей полный набор уравнений для этого семейства. Например:
type family F a where
F Int = Double
F Bool = Char
F a = String
Уравнения закрытого семейства типов перебираются по порядку сверху вниз при упрощении применения семейства типов. В этом примере мы объявляем экземпляр для F, так что F Int упрощается до Double, F Bool упрощается до Char, и для любого другого типа a, который не является Int или Bool, F a упрощается до String. Обратите внимание, что GHC должен быть уверен, что a не может быть унифицировано с Int или Bool в этом последнем случае; если программист укажет только F a в своем коде, GHC не сможет упростить тип. В конце концов, a позже может быть проинициализирован значением Int.
Уравнения закрытого семейства типов имеют те же ограничения и расширения, что и уравнения для экземпляров открытых семейств типов. Например, при включении ExplicitForAll переменные типа или вида, используемые в левой части уравнения, могут быть явно связаны, например, в:
type family R a where
forall t a. R (t a) = [a]
forall a. R a = a
Закрытое семейство типов может быть объявлено без уравнений. Такие закрытые семейства типов представляют собой неявные определения на уровне типов, которые никогда не будут сокращены, не обязательно являются инъективными (в отличие от пустых типов данных) и не могут быть присвоены экземпляры.
В файле hs-boot, закрытые семейства типов должны либо иметь те же уравнения, что и в исходном файле, либо вы можете использовать следующий синтаксис для пропуска уравнений (обратите внимание на буквальное ..)
type family R a where ..
В этом случае закрытое семейство типов R с этой декларацией «запуска» может иметь любое количество уравнений, заданных в исходном файле hs (включая ноль). Дополнительную информацию о взаимно рекурсивных модулях с hs-boot модулями (включая семейства типов) см. в Взаимно рекурсивные модули и файлы hs-boot.
6.4.9.2.4. Примеры семейств типов
Вот несколько примеров допустимых и недопустимых экземпляров типов:
type family F a :: Type
type instance F [Int] = Int -- OK!
type instance F String = Char -- OK!
type instance F (F a) = a -- WRONG: type parameter mentions a type family
type instance
F (forall a. (a, b)) = b -- WRONG: a forall type appears in a type parameter
type instance
F Float = forall a.a -- WRONG: right-hand side may not be a forall type
type family H a where -- OK!
H Int = Int
H Bool = Bool
H a = String
type instance H Char = Char -- WRONG: cannot have instances of closed family
type family K a where -- OK!
type family G a b :: Type -> Type
type instance G Int = (,) -- WRONG: must be two type parameters
type instance G Int Char Float = Double -- WRONG: must be two type parameters
6.4.9.2.5. Совместимость и различие уравнений семейств типов
Должны быть некоторые ограничения на уравнения семейств типов, чтобы мы не определили неоднозначную систему переписывания. Итак, уравнения открытых семейств типов ограничены совместимостью. Два шаблона типов совместимы, если
- все соответствующие типы и неявные виды в шаблонах различны, или
- два шаблона унифицируются, создавая подстановку, и правые части равны при этой подстановке.
Два типа считаются различными, если для всех возможных подстановок типы не могут быть сведены к одному редукту.
Первый пункт «совместимости» более прямой. Он утверждает, что шаблоны двух разных экземпляров семейств типов не могут перекрываться. Например, следующее запрещено:
type instance F Int = Bool
type instance F Int = Char
Второй пункт немного интереснее. Он утверждает, что два перекрывающихся экземпляра семейств типов разрешены, если правые части совпадают в области перекрытия. Некоторые примеры помогут здесь:
type instance F (a, Int) = [a]
type instance F (Int, b) = [b] -- overlap permitted
type instance G (a, Int) = [a]
type instance G (Char, a) = [a] -- ILLEGAL overlap, as [Char] /= [Int]
Обратите внимание, что это условие совместимости не зависит от того, является ли семейство типов связанным или нет, и это не только вопрос согласованности, но и вопрос безопасности типов.
Для поливидного семейства типов виды проверяются на различие так же, как и типы. Например, следующее принимается:
type family J a :: k
type instance J Int = Bool
type instance J Int = Maybe
Эти экземпляры совместимы, потому что они отличаются своим неявным параметром вида; первый использует Type, а второй использует Type -> Type.
Определение «совместимости» использует понятие «различие», определение которого в свою очередь опирается на редукцию семейства типов. Это условие «различия», как заявлено, невозможно проверить, поэтому мы используем эту консервативную аппроксимацию: два типа считаются различными, когда два типа не могут быть унифицированы, даже бесконечным унификатором. Разрешение бесконечного унификатора запрещает следующую пару экземпляров:
type instance H x x = Int
type instance H [x] x = Bool
Шаблоны типов в этой паре равны, если x заменяется бесконечным вложением списков. Отклонение таких экземпляров необходимо для безопасности типа.
Совместимость также влияет на закрытые семейства типов. При упрощении применения закрытого семейства типов GHC будет выбирать уравнение только тогда, когда он уверен, что ни одно несовместимое предыдущее уравнение никогда не будет применено. Вот несколько примеров:
type family F a where
F Int = Bool
F a = Char
type family G a where
G Int = Int
G a = a
В определении для F, два уравнения несовместимы — их шаблоны не различны, и тем не менее их правые части не совпадают. Таким образом, прежде чем GHC выберет второе уравнение, он должен быть уверен, что первое никогда не будет применено. Поэтому тип F a не упрощается; только тип, такой как F Double упростится до Char. В G, с другой стороны, два уравнения совместимы. Таким образом, GHC может игнорировать первое уравнение при рассмотрении второго. Поэтому G a упростится до a.
Несовместимости между уравнениями закрытых семейств типов могут быть отображены в :info, когда включен -fprint-axiom-incomps.
Однако см. Декларации типов, классов и других для правил перекрытия в GHCi.
