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

Maintainer | libraries@haskell.org |

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: 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: 4.7.0.0

class (~#) j k a b => (j ~~ k) a b 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.

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 a 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 k ((:~:) k a) | |

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

A type family to compute Boolean equality. Instances are provided only for *open* kinds, such as `*`

and function kinds. Instances are also provided for datatypes exported from base. A poly-kinded instance is *not* provided, as a recursive definition for algebraic kinds is generally more useful.

type (==) Bool a b | |

type (==) Ordering a b | |

type (==) * a b | |

type (==) Nat a b | |

type (==) Symbol a b | |

type (==) () a b | |

type (==) [k] a b | |

type (==) (Maybe k) a b | |

type (==) (k1 -> k2) a b | |

type (==) (Either k k1) a b | |

type (==) (k, k1) a b | |

type (==) (k, k1, k2) a b | |

type (==) (k, k1, k2, k3) a b | |

type (==) (k, k1, k2, k3, k4) a b | |

type (==) (k, k1, k2, k3, k4, k5) a b | |

type (==) (k, k1, k2, k3, k4, k5, k6) a b | |

type (==) (k, k1, k2, k3, k4, k5, k6, k7) a b | |

type (==) (k, k1, k2, k3, k4, k5, k6, k7, k8) a b | |

type (==) (k, k1, k2, k3, k4, k5, k6, k7, k8, k9) a b | |

type (==) (k, k1, k2, k3, k4, k5, k6, k7, k8, k9, k10) a b | |

type (==) (k, k1, k2, k3, k4, k5, k6, k7, k8, k9, k10, k11) a b | |

type (==) (k, k1, k2, k3, k4, k5, k6, k7, k8, k9, k10, k11, k12) a b | |

type (==) (k, k1, k2, k3, k4, k5, k6, k7, k8, k9, k10, k11, k12, k13) a b | |

type (==) (k, k1, k2, k3, k4, k5, k6, k7, k8, k9, k10, k11, k12, k13, k14) a b | |

© The University of Glasgow and others

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

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