| Copyright | (C) 2013 Richard Eisenberg |
|---|---|
| License | BSD-style (see LICENSE) |
| Maintainer | Richard Eisenberg (eir@cis.upenn.edu) |
| Stability | experimental |
| Portability | non-portable |
| Safe Haskell | None |
| Language | Haskell2010 |
Data.Singletons.Types
Description
Defines and exports types that are useful when working with singletons.
Some of these are re-exports from Data.Type.Equality.
Documentation
data KProxy t
A concrete, promotable proxy type, for use at the kind level There are no instances for this because it is intended at the kind level only
Constructors
| KProxy |
data Proxy t
A concrete, poly-kinded proxy type
Constructors
| Proxy |
Instances
| Monad (Proxy *) | |
| Functor (Proxy *) | |
| Applicative (Proxy *) | |
| Bounded (Proxy k s) | |
| Enum (Proxy k s) | |
| Eq (Proxy k s) | |
| Data t => Data (Proxy * t) | |
| Ord (Proxy k s) | |
| Read (Proxy k s) | |
| Show (Proxy k s) | |
| Ix (Proxy k s) | |
| Generic (Proxy * t) | |
| Monoid (Proxy * s) | |
| Typeable (k -> *) (Proxy k) | |
| type Rep (Proxy k t) = D1 D1Proxy (C1 C1_0Proxy U1) |
data a :~: b where
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
gcastWith :: (:~:) k a b -> ((~) k a b -> r) -> r
Generalized form of type-safe cast using propositional equality
class TestEquality f where
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.
Methods
testEquality :: f a -> f b -> Maybe ((:~:) k a b)
Conditionally prove the equality of a and b.
Instances
| SDecide k (KProxy k) => TestEquality k (Sing k) | |
| TestEquality k ((:~:) k a) |
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.
Instances
| type (==) Bool a b = EqBool a b | |
| type (==) Ordering a b = EqOrdering a b | |
| type (==) * a b = EqStar a b | |
| type (==) Nat a b = EqNat a b | |
| type (==) Symbol a b = EqSymbol a b | |
| type (==) () a b = EqUnit a b | |
| type (==) [k] a b = EqList k a b | |
| type (==) (Maybe k) a b = EqMaybe k a b | |
| type (==) (k -> k1) a b = EqArrow k k1 a b | |
| type (==) (Either k k1) a b = EqEither k k1 a b | |
| type (==) ((,) k k1) a b = Eq2 k k1 a b | |
| type (==) ((,,) k k1 k2) a b = Eq3 k k1 k2 a b | |
| type (==) ((,,,) k k1 k2 k3) a b = Eq4 k k1 k2 k3 a b | |
| type (==) ((,,,,) k k1 k2 k3 k4) a b = Eq5 k k1 k2 k3 k4 a b | |
| type (==) ((,,,,,) k k1 k2 k3 k4 k5) a b = Eq6 k k1 k2 k3 k4 k5 a b | |
| type (==) ((,,,,,,) k k1 k2 k3 k4 k5 k6) a b = Eq7 k k1 k2 k3 k4 k5 k6 a b | |
| type (==) ((,,,,,,,) k k1 k2 k3 k4 k5 k6 k7) a b = Eq8 k k1 k2 k3 k4 k5 k6 k7 a b | |
| type (==) ((,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8) a b = Eq9 k k1 k2 k3 k4 k5 k6 k7 k8 a b | |
| type (==) ((,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9) a b = Eq10 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 = Eq11 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 = Eq12 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 = Eq13 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 = Eq14 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 = Eq15 k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12 k13 k14 a b |