Data.Type.Equality (original) (raw)

Contents

• The equality types
• Working with equality
• Inferring equality from other types
• Boolean type-level equality

Description

Definition of propositional equality (`[:~:](Data-Type-Equality.html#t::-126-: "Data.Type.Equality")`). Pattern-matching on a variable of type (a `[:~:](Data-Type-Equality.html#t::-126-: "Data.Type.Equality")` b) produces a proof that a `~` b.

Since: base-4.7.0.0

Synopsis

• data a :~: b where
  • Refl :: a :~: a
• class a ~# b => (a :: k0) ~~ (b :: k1)
• data a :~~: b where
  • HRefl :: a :~~: a
• 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
• inner :: (f a :~: g b) -> a :~: b
• outer :: (f a :~: g b) -> f :~: g
• class TestEquality f where
  • testEquality :: f a -> f b -> Maybe (a :~: b)
• type family a == b where ...

The equality types

data a :~: b where infix 4 Source #

Propositional equality. If a :~: b is inhabited by some terminating value, then the type a is the same as the type b. To use this equality in practice, pattern-match on the a :~: b to get out the Refl constructor; in the body of the pattern-match, the compiler knows that a ~ b.

Since: base-4.7.0.0

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

Lifted, heterogeneous equality. By lifted, we mean that it can be bogus (deferred type error). By heterogeneous, the two types a and b might have different kinds. Because ~~ can appear unexpectedly in error messages to users who do not care about the difference between heterogeneous equality ~~ and homogeneous equality ~, this is printed as ~ unless-fprint-equality-relations is set.

In 0.7.0, the fixity was set to infix 4 to match the fixity of [:~~:](Data-Type-Equality.html#v::-126--126-: "Data.Type.Equality").

data a :~~: b where infix 4 Source #

Kind heterogeneous propositional equality. Like [:~:](Data-Type-Equality.html#t::-126-: "Data.Type.Equality"), a :~~: b is inhabited by a terminating value if and only if a is the same type as b.

Since: base-4.10.0.0

Working with equality

gcastWith :: (a :~: b) -> (a ~ b => r) -> r Source #

Generalized form of type-safe cast using propositional equality

inner :: (f a :~: g b) -> a :~: b Source #

Extract equality of the arguments from an equality of applied types

outer :: (f a :~: g b) -> f :~: g Source #

Extract equality of type constructors from an equality of applied types

Inferring equality from other types

class TestEquality f where Source #

This class contains types where you can learn the equality of two types from information contained in terms. Typically, only singleton types should inhabit this class.

Boolean type-level equality

type family a == b where ... infix 4 Source #

A type family to compute Boolean equality.