Data.Type.Equality

License	BSD-style (see the LICENSE file in the distribution)
Maintainer	libraries@haskell.org
Stability	stable
Portability	not portable
Safe Haskell	Safe
Language	Haskell2010

Содержание

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

Описание

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

Since: base-4.7.0.0

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

class a ~# b => (a :: k) ~ (b :: k) infix 4 Source

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

class a ~# b => (a :: k0) ~~ (b :: k1) infix 4 Source

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

В 0.7.0, фиксация была установлена в infix 4 для соответствия фиксации :~~:.

data (a :: k) :~: (b :: k) where infix 4 Source

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

Since: base-4.7.0.0

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

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

Экземпляры

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

Category ((:~:) :: k -> k -> Type) Source	Since: base-4.7.0.0
Подробности об экземпляре Определено в GHC.Internal.Control.Category Методы id :: forall (a :: k). a :~: a Source (.) :: forall (b :: k) (c :: k) (a :: k). (b :~: c) -> (a :~: b) -> a :~: c Source
TestCoercion ((:~:) a :: k -> Type) Source	Since: base-4.7.0.0
Подробности об экземпляре Определено в GHC.Internal.Data.Type.Coercion Методы testCoercion :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (Coercion a0 b) Source
TestEquality ((:~:) a :: k -> Type) Source	Since: base-4.7.0.0
Подробности об экземпляре Определено в GHC.Internal.Data.Type.Equality Методы testEquality :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) Source
(a ~ b, Data a) => Data (a :~: b) Source	Since: 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 Исходный код
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 Исходный код

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) Исходный код
(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 Исходный код
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 Исходный код

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

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 -> Тип) 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 -> Может быть (a :~: 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.12.1/docs/libraries/base-4.21.0.0-8e62/Data-Type-Equality.html