Data.Type.Equality

Лицензия	В стиле BSD (см. файл LICENSE в дистрибутиве)
Сопровождающий	libraries@haskell.org
Стабильность	стабильная
Переносимость	непереносимый
Безопасный Haskell	Безопасный
Язык	Haskell2010

Содержание

Типы равенства
Работа с равенством
Выведение равенства из других типов
Равенство на уровне типов с булевыми значениями

Описание

Определение пропозиционального равенства (:~:). Сопоставление с образцом для переменной типа (a :~: b) даёт доказательство того, что a ~ b.

Начиная с: base-4.7.0.0

Типы равенства

class a ~# b => (a :: k) ~ (b :: k) infix 4 Исходный код

Поднятое однородное равенство. Под «поднятым» подразумевается, что оно может быть фиктивным (отложенная ошибка типа). Под «однородным» подразумевается, что типы a и b должны иметь один и тот же вид.

class a ~# b => (a :: k0) ~~ (b :: k1) infix 4 Исходный код

Поднятое разнородное равенство. Под «поднятым» подразумевается, что оно может быть фиктивным (отложенная ошибка типа). Под «разнородным» подразумевается, что типы a и b могут иметь разные виды. Поскольку ~~ может неожиданно появляться в сообщениях об ошибках для пользователей, которым не важна разница между разнородным равенством ~~ и однородным равенством ~, оно выводится как ~, если не задан -fprint-equality-relations.

В 0.7.0 фиксированность была задана как infix 4, чтобы соответствовать фиксированности :~~:.

data (a :: k) :~: (b :: k) where infix 4 Исходный код

Пропозициональное равенство. Если a :~: b содержит некоторое завершающееся значение, то тип a совпадает с типом b. Чтобы использовать это равенство на практике, выполните сопоставление с образцом для a :~: b, чтобы получить конструктор Refl; в теле сопоставления с образцом компилятор знает, что a ~ b.

Начиная с: base-4.7.0.0

Конструкторы

Refl :: forall {k} (a :: k). a :~: a

Экземпляры

Подробности об экземплярах

Category ((:~:) :: k -> k -> Type) Исходный код	Начиная с: base-4.7.0.0
Подробности об экземпляре Определён в GHC.Internal.Control.Category Методы id :: forall (a :: k). a :~: a Исходный код (.) :: forall (b :: k) (c :: k) (a :: k). (b :~: c) -> (a :~: b) -> a :~: c Исходный код
TestCoercion ((:~:) a :: k -> Type) Исходный код	Начиная с: base-4.7.0.0
Подробности об экземпляре Определён в GHC.Internal.Data.Type.Coercion Методы testCoercion :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (Coercion a0 b) Исходный код
TestEquality ((:~:) a :: k -> Type) Исходный код	Начиная с: base-4.7.0.0
Подробности об экземпляре Определён в GHC.Internal.Data.Type.Equality Методы testEquality :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) Исходный код
Eq (a :~: b) Исходный код	Начиная с: base-4.7.0.0
Подробности об экземпляре Определён в GHC.Internal.Data.Type.Equality Методы (==) :: (a :~: b) -> (a :~: b) -> Bool Исходный код (/=) :: (a :~: b) -> (a :~: b) -> Bool Исходный код
Ord (a :~: b) Исходный код	Начиная с: base-4.7.0.0
Подробности об экземпляре Определён в GHC.Internal.Data.Type.Equality Методы compare :: (a :~: b) -> (a :~: b) -> Ordering Исходный код (<) :: (a :~: b) -> (a :~: b) -> Bool Исходный код (<=) :: (a :~: b) -> (a :~: b) -> Bool Исходный код (>) :: (a :~: b) -> (a :~: b) -> Bool Исходный код (>=) :: (a :~: b) -> (a :~: b) -> Bool Исходный код max :: (a :~: b) -> (a :~: b) -> a :~: b Исходный код min :: (a :~: b) -> (a :~: b) -> a :~: b Исходный код
(a ~ b, Data a) => Data (a :~: b) Исходный код	Начиная с: base-4.7.0.0
Подробности об экземпляре Определён в GHC.Internal.Data.Data Методы gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> (a :~: b) -> c (a :~: b) Исходный код gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (a :~: b) Исходный код toConstr :: (a :~: b) -> Constr Исходный код dataTypeOf :: (a :~: b) -> DataType Исходный код dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (a :~: b)) Исходный код dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (a :~: b)) Исходный код gmapT :: (forall b0. Data b0 => b0 -> b0) -> (a :~: b) -> a :~: b Исходный код gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r Исходный код gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r Исходный код gmapQ :: (forall d. Data d => d -> u) -> (a :~: b) -> [u] Исходный код gmapQi :: Int -> (forall d. Data d => d -> u) -> (a :~: b) -> u Исходный код gmapM :: Monad m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) Исходный код gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) Исходный код gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) Исходный код
a ~ b => Bounded (a :~: b) Исходный код	Начиная с: base-4.7.0.0
Подробности об экземпляре Определён в GHC.Internal.Data.Type.Equality Методы minBound :: a :~: b Исходный код maxBound :: a :~: b Исходный код
a ~ b => Enum (a :~: b) Исходный код	Начиная с: base-4.7.0.0
Подробности об экземпляре Определён в GHC.Internal.Data.Type.Equality Методы succ :: (a :~: b) -> a :~: b Исходный код pred :: (a :~: b) -> a :~: b Исходный код toEnum :: Int -> a :~: b Исходный код fromEnum :: (a :~: b) -> Int Исходный код enumFrom :: (a :~: b) -> [a :~: b] Исходный код enumFromThen :: (a :~: b) -> (a :~: b) -> [a :~: b] Исходный код enumFromTo :: (a :~: b) -> (a :~: b) -> [a :~: b] Исходный код enumFromThenTo :: (a :~: b) -> (a :~: b) -> (a :~: b) -> [a :~: b] Исходный код
a ~ b => Read (a :~: b) Исходный код	Начиная с: base-4.7.0.0
Подробности об экземпляре Определён в GHC.Internal.Data.Type.Equality Методы readsPrec :: Int -> ReadS (a :~: b) Исходный код readList :: ReadS [a :~: b] Исходный код readPrec :: ReadPrec (a :~: b) Исходный код readListPrec :: ReadPrec [a :~: b] Исходный код
Show (a :~: b) Исходный код	Начиная с: base-4.7.0.0
Подробности об экземпляре Определён в GHC.Internal.Data.Type.Equality Методы showsPrec :: Int -> (a :~: b) -> ShowS Исходный код show :: (a :~: b) -> String Исходный код showList :: [a :~: b] -> ShowS Исходный код

data (a :: k1) :~~: (b :: k2) where infix 4 Исходный код

Гетерогенное пропозициональное равенство на уровне типов. Как и :~:, a :~~: b содержит завершающее значение тогда и только тогда, когда a — тот же тип, что и b.

Начиная с: base-4.10.0.0

Конструкторы

HRefl :: forall {k1} (a :: k1). a :~~: a

Экземпляры

Подробности экземпляров

Category ((:~~:) :: k -> k -> Type) Исходный код	Начиная с: base-4.10.0.0
Подробности экземпляра Определён в GHC.Internal.Control.Category Методы id :: forall (a :: k). a :~~: a Исходный код (.) :: forall (b :: k) (c :: k) (a :: k). (b :~~: c) -> (a :~~: b) -> a :~~: c Исходный код
TestCoercion ((:~~:) a :: k -> Type) Исходный код	Начиная с: base-4.10.0.0
Подробности экземпляра Определён в GHC.Internal.Data.Type.Coercion Методы testCoercion :: forall (a0 :: k) (b :: k). (a :~~: a0) -> (a :~~: b) -> Maybe (Coercion a0 b) Исходный код
TestEquality ((:~~:) a :: k -> Type) Исходный код	Начиная с: base-4.10.0.0
Подробности экземпляра Определён в GHC.Internal.Data.Type.Equality Методы testEquality :: forall (a0 :: k) (b :: k). (a :~~: a0) -> (a :~~: b) -> Maybe (a0 :~: b) Исходный код
Eq (a :~~: b) Исходный код	Начиная с: base-4.10.0.0
Подробности экземпляра Определён в GHC.Internal.Data.Type.Equality Методы (==) :: (a :~~: b) -> (a :~~: b) -> Bool Исходный код (/=) :: (a :~~: b) -> (a :~~: b) -> Bool Исходный код
Ord (a :~~: b) Исходный код	Начиная с: base-4.10.0.0
Подробности экземпляра Определён в GHC.Internal.Data.Type.Equality Методы compare :: (a :~~: b) -> (a :~~: b) -> Ordering Исходный код (<) :: (a :~~: b) -> (a :~~: b) -> Bool Исходный код (<=) :: (a :~~: b) -> (a :~~: b) -> Bool Исходный код (>) :: (a :~~: b) -> (a :~~: b) -> Bool Исходный код (>=) :: (a :~~: b) -> (a :~~: b) -> Bool Исходный код max :: (a :~~: b) -> (a :~~: b) -> a :~~: b Исходный код min :: (a :~~: b) -> (a :~~: b) -> a :~~: b Исходный код
(Typeable i, Typeable j, Typeable a, Typeable b, a ~~ b) => Data (a :~~: b) Исходный код	Начиная с: base-4.10.0.0
Подробности экземпляра Определён в GHC.Internal.Data.Data Методы gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> (a :~~: b) -> c (a :~~: b) Исходный код gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (a :~~: b) Исходный код toConstr :: (a :~~: b) -> Constr Исходный код dataTypeOf :: (a :~~: b) -> DataType Исходный код dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (a :~~: b)) Исходный код dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (a :~~: b)) Исходный код gmapT :: (forall b0. Data b0 => b0 -> b0) -> (a :~~: b) -> a :~~: b Исходный код gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~~: b) -> r Исходный код gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (a :~~: b) -> r Исходный код gmapQ :: (forall d. Data d => d -> u) -> (a :~~: b) -> [u] Исходный код gmapQi :: Int -> (forall d. Data d => d -> u) -> (a :~~: b) -> u Исходный код gmapM :: Monad m => (forall d. Data d => d -> m d) -> (a :~~: b) -> m (a :~~: b) Исходный код gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~~: b) -> m (a :~~: b) Исходный код gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~~: b) -> m (a :~~: b) Исходный код
a ~~ b => Bounded (a :~~: b) Исходный код	Начиная с: base-4.10.0.0
Подробности экземпляра Определён в GHC.Internal.Data.Type.Equality Методы minBound :: a :~~: b Исходный код maxBound :: a :~~: b Исходный код
a ~~ b => Enum (a :~~: b) Исходный код	Начиная с: base-4.10.0.0
Подробности экземпляра Определён в GHC.Internal.Data.Type.Equality Методы succ :: (a :~~: b) -> a :~~: b Исходный код pred :: (a :~~: b) -> a :~~: b Исходный код toEnum :: Int -> a :~~: b Исходный код fromEnum :: (a :~~: b) -> Int Исходный код enumFrom :: (a :~~: b) -> [a :~~: b] Исходный код enumFromThen :: (a :~~: b) -> (a :~~: b) -> [a :~~: b] Исходный код enumFromTo :: (a :~~: b) -> (a :~~: b) -> [a :~~: b] Исходный код enumFromThenTo :: (a :~~: b) -> (a :~~: b) -> (a :~~: b) -> [a :~~: b] Исходный код
a ~~ b => Read (a :~~: b) Исходный код	Начиная с: base-4.10.0.0
Подробности экземпляра Определён в GHC.Internal.Data.Type.Equality Методы readsPrec :: Int -> ReadS (a :~~: b) Исходный код readList :: ReadS [a :~~: b] Исходный код readPrec :: ReadPrec (a :~~: b) Исходный код readListPrec :: ReadPrec [a :~~: b] Исходный код
Show (a :~~: b) Исходный код	Начиная с: base-4.10.0.0
Подробности экземпляра Определён в GHC.Internal.Data.Type.Equality Методы showsPrec :: Int -> (a :~~: b) -> ShowS Исходный код show :: (a :~~: b) -> String Исходный код showList :: [a :~~: b] -> ShowS Исходный код

Работа с равенством

sym :: forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a Исходный код

Симметричность равенства

trans :: forall {k} (a :: k) (b :: k) (c :: k). (a :~: b) -> (b :~: c) -> a :~: c Исходный код

Транзитивность равенства

castWith :: (a :~: b) -> a -> b Исходный код

Безопасное приведение типа с использованием пропозиционального равенства

gcastWith :: forall {k} (a :: k) (b :: k) r. (a :~: b) -> (a ~ b => r) -> r Исходный код

Обобщённая форма приведения типов с проверкой типов, использующая пропозициональное равенство

apply :: forall {k1} {k2} (f :: k1 -> k2) (g :: k1 -> k2) (a :: k1) (b :: k1). (f :~: g) -> (a :~: b) -> f a :~: g b Исходный код

Применяет одно равенство к другому, соответственно

inner :: forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (g :: k1 -> k2) (b :: k1). (f a :~: g b) -> a :~: b Исходный код

Извлекает равенство аргументов из равенства применённых типов

outer :: forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (g :: k1 -> k2) (b :: k1). (f a :~: g b) -> f :~: g Исходный код

Извлекает равенство конструкторов типов из равенства применённых типов

Вывод равенства из других типов

class TestEquality (f :: k -> Type) where Исходный код

Этот класс включает типы, для которых равенство двух типов можно определить по информации, содержащейся в термах.

Результат должен быть Just Refl тогда и только тогда, когда типы, применённые к f, равны:

testEquality (x :: f a) (y :: f b) = Just Refl ⟺ a = b

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

testEquality (x :: f a) (y :: f b) = Just Refl ⟺ a = b ⟺ x = y

isJust (testEquality x y) = x == y

Однако синглтонные типы не являются обязательными, поэтому два последних предполагаемых закона в общем случае неверны.

Методы

testEquality :: forall (a :: k) (b :: k). f a -> f b -> :~: b) Исходный код

Условно доказывает равенство a и b.

Экземпляры

Подробная информация об экземплярах

TestEquality SNat Исходный код	С версии: base-4.18.0.0
Подробности экземпляра Определён в GHC.Internal.TypeNats Методы testEquality :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b) Исходный код
TestEquality SChar Исходный код	С версии: base-4.18.0.0
Подробности экземпляра Определён в GHC.Internal.TypeLits Методы testEquality :: forall (a :: Char) (b :: Char). SChar a -> SChar b -> Maybe (a :~: b) Исходный код
TestEquality SSymbol Исходный код	С версии: base-4.18.0.0
Подробности экземпляра Определён в GHC.Internal.TypeLits Методы testEquality :: forall (a :: Symbol) (b :: Symbol). SSymbol a -> SSymbol b -> Maybe (a :~: b) Исходный код
TestEquality (TypeRep :: k -> Type) Исходный код
Подробности экземпляра Определён в GHC.Internal.Data.Typeable.Internal Методы testEquality :: forall (a :: k) (b :: k). TypeRep a -> TypeRep b -> Maybe (a :~: b) Исходный код
TestEquality ((:~:) a :: k -> Type) Исходный код	С версии: base-4.7.0.0
Подробности экземпляра Определён в GHC.Internal.Data.Type.Equality Методы testEquality :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) Исходный код
TestEquality ((:~~:) a :: k -> Type) Исходный код	С версии: base-4.10.0.0
Подробности экземпляра Определён в GHC.Internal.Data.Type.Equality Методы testEquality :: forall (a0 :: k) (b :: k). (a :~~: a0) -> (a :~~: b) -> Maybe (a0 :~: b) Исходный код
TestEquality f => TestEquality (Compose f g :: k2 -> Type) Исходный код	Вывод (с помощью порождаемости): если `g x :~: g y`, то `x :~: y`. С версии: base-4.14.0.0
Подробности экземпляра Определён в Data.Functor.Compose Методы testEquality :: forall (a :: k2) (b :: k2). Compose f g a -> Compose f g b -> Maybe (a :~: b) Исходный код

Булево равенство на уровне типов

type family (a :: k) == (b :: k) :: Bool where ... infix 4 Исходный код

Семейство типов для вычисления булева равенства.

Уравнения

(f a :: k2) == (g b :: k2) = (f == g) && (a == b)
(a :: k) == (a :: k) = 'True
(_1 :: k) == (_2 :: k) = 'False

© The University of Glasgow and others
Licensed under a BSD-style license (see top of the page).
https://downloads.haskell.org/~ghc/9.14.1/docs/libraries/base-4.22.0.0-66f8/Data-Type-Equality.html