Тип данных.Равенство

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

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

data a :~: b where infix 4 Источник

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

С: 4.7.0.0

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

sym :: (a :~: b) -> b :~: a Источник

Симметрия равенства

trans :: (a :~: b) -> (b :~: c) -> a :~: c Источник

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

castWith :: (a :~: b) -> a -> b Источник

Безопасное преобразование типов, использующее пропозициональное равенство

gcastWith :: (a :~: b) -> ((a ~ b) => r) -> r Источник

Обобщённая форма безопасного преобразования типов с использованием пропозиционального равенства

apply :: (f :~: g) -> (a :~: b) -> f a :~: g b Источник

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

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

class TestEquality f where Источник

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

Равенство на уровне типов Bool

type family a == b :: Bool infix 4 Источник

Семейство типов для вычисления булевого равенства. Экземпляры предоставляются только для открытых видов, таких как * и видов функций. Экземпляры также предоставляются для типов данных, экспортированных из base. Поликинетический экземпляр не предоставляется, так как рекурсивное определение для алгебраических видов обычно более полезно.