License | BSD-style (see the LICENSE file in the distribution) |
---|---|

Maintainer | [email protected] |

Stability | experimental |

Portability | not portable |

Safe Haskell | Trustworthy |

Language | Haskell2010 |

Definition of propositional equality `(:~:)`

. Pattern-matching on a variable of type `(a :~: b)`

produces a proof that `a ~ b`

.

Since: base-4.7.0.0

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

Category ((:~:) :: k -> k -> Type) | Since: base-4.7.0.0 |

TestEquality ((:~:) a :: k -> Type) | Since: base-4.7.0.0 |

Defined in Data.Type.Equality | |

TestCoercion ((:~:) a :: k -> Type) | Since: base-4.7.0.0 |

Defined in Data.Type.Coercion | |

a ~ b => Bounded (a :~: b) | Since: base-4.7.0.0 |

a ~ b => Enum (a :~: b) | Since: base-4.7.0.0 |

Defined in Data.Type.Equality ## Methodssucc :: (a :~: b) -> a :~: b Source pred :: (a :~: b) -> a :~: b Source toEnum :: Int -> a :~: b Source fromEnum :: (a :~: b) -> Int Source enumFrom :: (a :~: b) -> [a :~: b] Source enumFromThen :: (a :~: b) -> (a :~: b) -> [a :~: b] Source enumFromTo :: (a :~: b) -> (a :~: b) -> [a :~: b] Source enumFromThenTo :: (a :~: b) -> (a :~: b) -> (a :~: b) -> [a :~: b] Source | |

Eq (a :~: b) | Since: base-4.7.0.0 |

(a ~ b, Data a) => Data (a :~: b) | Since: base-4.7.0.0 |

Defined in Data.Data ## Methodsgfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> (a :~: b) -> c (a :~: b) Source gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (a :~: b) Source toConstr :: (a :~: b) -> Constr Source dataTypeOf :: (a :~: b) -> DataType Source dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (a :~: b)) Source dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (a :~: b)) Source gmapT :: (forall b0. Data b0 => b0 -> b0) -> (a :~: b) -> a :~: b Source gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r Source gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r Source gmapQ :: (forall d. Data d => d -> u) -> (a :~: b) -> [u] Source gmapQi :: Int -> (forall d. Data d => d -> u) -> (a :~: b) -> u Source gmapM :: Monad m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) Source gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) Source gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) Source | |

Ord (a :~: b) | Since: base-4.7.0.0 |

Defined in Data.Type.Equality | |

a ~ b => Read (a :~: b) | Since: base-4.7.0.0 |

Show (a :~: b) | Since: base-4.7.0.0 |

class a ~# b => (a :: k0) ~~ (b :: k1) 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.

data (a :: k1) :~~: (b :: k2) where infix 4 Source

Kind heterogeneous propositional equality. Like `:~:`

, `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

Category ((:~~:) :: k -> k -> Type) | Since: base-4.10.0.0 |

TestEquality ((:~~:) a :: k -> Type) | Since: base-4.10.0.0 |

Defined in Data.Type.Equality | |

TestCoercion ((:~~:) a :: k -> Type) | Since: base-4.10.0.0 |

Defined in Data.Type.Coercion | |

a ~~ b => Bounded (a :~~: b) | Since: base-4.10.0.0 |

a ~~ b => Enum (a :~~: b) | Since: base-4.10.0.0 |

Defined in Data.Type.Equality ## Methodssucc :: (a :~~: b) -> a :~~: b Source pred :: (a :~~: b) -> a :~~: b Source toEnum :: Int -> a :~~: b Source fromEnum :: (a :~~: b) -> Int Source enumFrom :: (a :~~: b) -> [a :~~: b] Source enumFromThen :: (a :~~: b) -> (a :~~: b) -> [a :~~: b] Source enumFromTo :: (a :~~: b) -> (a :~~: b) -> [a :~~: b] Source enumFromThenTo :: (a :~~: b) -> (a :~~: b) -> (a :~~: b) -> [a :~~: b] Source | |

Eq (a :~~: b) | Since: base-4.10.0.0 |

(Typeable i, Typeable j, Typeable a, Typeable b, a ~~ b) => Data (a :~~: b) | Since: base-4.10.0.0 |

Defined in Data.Data ## Methodsgfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> (a :~~: b) -> c (a :~~: b) Source gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (a :~~: b) Source toConstr :: (a :~~: b) -> Constr Source dataTypeOf :: (a :~~: b) -> DataType Source dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (a :~~: b)) Source dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (a :~~: b)) Source gmapT :: (forall b0. Data b0 => b0 -> b0) -> (a :~~: b) -> a :~~: b Source gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~~: b) -> r Source gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (a :~~: b) -> r Source gmapQ :: (forall d. Data d => d -> u) -> (a :~~: b) -> [u] Source gmapQi :: Int -> (forall d. Data d => d -> u) -> (a :~~: b) -> u Source gmapM :: Monad m => (forall d. Data d => d -> m d) -> (a :~~: b) -> m (a :~~: b) Source gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~~: b) -> m (a :~~: b) Source gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~~: b) -> m (a :~~: b) Source | |

Ord (a :~~: b) | Since: base-4.10.0.0 |

Defined in Data.Type.Equality ## Methodscompare :: (a :~~: b) -> (a :~~: b) -> Ordering Source (<) :: (a :~~: b) -> (a :~~: b) -> Bool Source (<=) :: (a :~~: b) -> (a :~~: b) -> Bool Source (>) :: (a :~~: b) -> (a :~~: b) -> Bool Source (>=) :: (a :~~: b) -> (a :~~: b) -> Bool Source | |

a ~~ b => Read (a :~~: b) | Since: base-4.10.0.0 |

Show (a :~~: b) | Since: base-4.10.0.0 |

sym :: (a :~: b) -> b :~: a Source

Symmetry of equality

trans :: (a :~: b) -> (b :~: c) -> a :~: c Source

Transitivity of equality

castWith :: (a :~: b) -> a -> b Source

Type-safe cast, using propositional equality

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

Generalized form of type-safe cast using propositional equality

apply :: (f :~: g) -> (a :~: b) -> f a :~: g b Source

Apply one equality to another, respectively

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

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.

testEquality :: f a -> f b -> Maybe (a :~: b) Source

Conditionally prove the equality of `a`

and `b`

.

TestEquality (TypeRep :: k -> Type) | |

Defined in Data.Typeable.Internal | |

TestEquality ((:~:) a :: k -> Type) | Since: base-4.7.0.0 |

Defined in Data.Type.Equality | |

TestEquality ((:~~:) a :: k -> Type) | Since: base-4.10.0.0 |

Defined in Data.Type.Equality |

type family (a :: k) == (b :: k) :: Bool where ... infix 4 Source

A type family to compute Boolean equality.

© The University of Glasgow and others

Licensed under a BSD-style license (see top of the page).

https://downloads.haskell.org/~ghc/8.6.1/docs/html/libraries/base-4.12.0.0/Data-Type-Equality.html