Copyright | (C) 2013 Richard Eisenberg |
---|---|
License | BSD-style (see LICENSE) |
Maintainer | Ryan Scott |
Stability | experimental |
Portability | non-portable |
Safe Haskell | None |
Language | Haskell2010 |
Data.Singletons.Prelude.Eq
Contents
Description
Defines the SEq singleton version of the Eq type class.
Synopsis
- class PEq a where
- class SEq k where
- type family DefaultEq (a :: k) (b :: k) :: Bool where ...
- data (==@#@$) :: forall a6989586621679375750. (~>) a6989586621679375750 ((~>) a6989586621679375750 Bool)
- data (==@#@$$) (x6989586621679375751 :: a6989586621679375750) :: (~>) a6989586621679375750 Bool
- type (==@#@$$$) (x6989586621679375751 :: a6989586621679375750) (y6989586621679375752 :: a6989586621679375750) = (==) x6989586621679375751 y6989586621679375752
- data (/=@#@$) :: forall a6989586621679375750. (~>) a6989586621679375750 ((~>) a6989586621679375750 Bool)
- data (/=@#@$$) (x6989586621679375753 :: a6989586621679375750) :: (~>) a6989586621679375750 Bool
- type (/=@#@$$$) (x6989586621679375753 :: a6989586621679375750) (y6989586621679375754 :: a6989586621679375750) = (/=) x6989586621679375753 y6989586621679375754
- data DefaultEqSym0 :: forall k6989586621679375744. (~>) k6989586621679375744 ((~>) k6989586621679375744 Bool)
- data DefaultEqSym1 (a6989586621679375745 :: k6989586621679375744) :: (~>) k6989586621679375744 Bool
- type DefaultEqSym2 (a6989586621679375745 :: k6989586621679375744) (b6989586621679375746 :: k6989586621679375744) = DefaultEq a6989586621679375745 b6989586621679375746
Documentation
The promoted analogue of Eq
. If you supply no definition for (==)
,
then it defaults to a use of DefaultEq
.
Associated Types
type (x :: a) == (y :: a) :: Bool infix 4 Source #
type (==) (x :: a) (y :: a) = x `DefaultEq` y Source #
Instances
PEq Bool Source # | |
PEq Ordering Source # | |
PEq Nat Source # | |
PEq Symbol Source # | |
PEq () Source # | |
PEq Void Source # | |
PEq All Source # | |
PEq Any Source # | |
PEq [a] Source # | |
PEq (Maybe a) Source # | |
PEq (TYPE rep) Source # | |
PEq (NonEmpty a) Source # | |
PEq (Down a) Source # | |
PEq (Identity a) Source # | |
PEq (First a) Source # | |
PEq (Last a) Source # | |
PEq (Max a) Source # | |
PEq (Min a) Source # | |
PEq (Option a) Source # | |
PEq (WrappedMonoid m) Source # | |
PEq (Dual a) Source # | |
PEq (Product a) Source # | |
PEq (Sum a) Source # | |
PEq (First a) Source # | |
PEq (Last a) Source # | |
PEq (Either a b) Source # | |
PEq (a, b) Source # | |
PEq (Arg a b) Source # | |
PEq (a, b, c) Source # | |
PEq (Const a b) Source # | |
PEq (a, b, c, d) Source # | |
PEq (a, b, c, d, e) Source # | |
PEq (a, b, c, d, e, f) Source # | |
PEq (a, b, c, d, e, f, g) Source # | |
The singleton analogue of Eq
. Unlike the definition for Eq
, it is required
that instances define a body for (%==)
. You may also supply a body for (%/=)
.
Minimal complete definition
Methods
(%==) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a == b) infix 4 Source #
Boolean equality on singletons
(%/=) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a /= b) infix 4 Source #
Boolean disequality on singletons
Instances
SEq Bool Source # | |
SEq Ordering Source # | |
SEq Nat Source # | |
SEq Symbol Source # | |
SEq () Source # | |
SEq Void Source # | |
SEq Bool => SEq All Source # | |
SEq Bool => SEq Any Source # | |
(SEq a, SEq [a]) => SEq [a] Source # | |
SEq a => SEq (Maybe a) Source # | |
SEq (TYPE rep) Source # | |
(SEq a, SEq [a]) => SEq (NonEmpty a) Source # | |
SEq a => SEq (Down a) Source # | |
SEq a => SEq (Identity a) Source # | |
SEq a => SEq (First a) Source # | |
SEq a => SEq (Last a) Source # | |
SEq a => SEq (Max a) Source # | |
SEq a => SEq (Min a) Source # | |
SEq (Maybe a) => SEq (Option a) Source # | |
SEq m => SEq (WrappedMonoid m) Source # | |
SEq a => SEq (Dual a) Source # | |
SEq a => SEq (Product a) Source # | |
SEq a => SEq (Sum a) Source # | |
SEq (Maybe a) => SEq (First a) Source # | |
SEq (Maybe a) => SEq (Last a) Source # | |
(SEq a, SEq b) => SEq (Either a b) Source # | |
(SEq a, SEq b) => SEq (a, b) Source # | |
SEq a => SEq (Arg a b) Source # | |
(SEq a, SEq b, SEq c) => SEq (a, b, c) Source # | |
SEq a => SEq (Const a b) Source # | |
(SEq a, SEq b, SEq c, SEq d) => SEq (a, b, c, d) Source # | |
(SEq a, SEq b, SEq c, SEq d, SEq e) => SEq (a, b, c, d, e) Source # | |
(SEq a, SEq b, SEq c, SEq d, SEq e, SEq f) => SEq (a, b, c, d, e, f) Source # | |
(SEq a, SEq b, SEq c, SEq d, SEq e, SEq f, SEq g) => SEq (a, b, c, d, e, f, g) Source # | |
type family DefaultEq (a :: k) (b :: k) :: Bool where ... Source #
A sensible way to compute Boolean equality for types of any kind. Note
that this definition is slightly different from the (==)
type family
from Data.Type.Equality in base
, as (==)
attempts to distinguish
applications of type constructors from other types. As a result,
a == a
does not reduce to True
for every a
, but
does reduce to DefaultEq
a aTrue
for every a
. The latter behavior is more desirable
for singletons
' purposes, so we use it instead of (==)
.
Defunctionalization symbols
data (==@#@$) :: forall a6989586621679375750. (~>) a6989586621679375750 ((~>) a6989586621679375750 Bool) infix 4 Source #
Instances
SEq a => SingI ((==@#@$) :: TyFun a (a ~> Bool) -> Type) Source # | |
SuppressUnusedWarnings ((==@#@$) :: TyFun a6989586621679375750 (a6989586621679375750 ~> Bool) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Eq Methods suppressUnusedWarnings :: () Source # | |
type Apply ((==@#@$) :: TyFun a6989586621679375750 (a6989586621679375750 ~> Bool) -> Type) (x6989586621679375751 :: a6989586621679375750) Source # | |
data (==@#@$$) (x6989586621679375751 :: a6989586621679375750) :: (~>) a6989586621679375750 Bool infix 4 Source #
Instances
(SEq a, SingI x) => SingI ((==@#@$$) x :: TyFun a Bool -> Type) Source # | |
SuppressUnusedWarnings ((==@#@$$) x6989586621679375751 :: TyFun a6989586621679375750 Bool -> Type) Source # | |
Defined in Data.Singletons.Prelude.Eq Methods suppressUnusedWarnings :: () Source # | |
type Apply ((==@#@$$) x6989586621679375751 :: TyFun a Bool -> Type) (y6989586621679375752 :: a) Source # | |
Defined in Data.Singletons.Prelude.Eq |
type (==@#@$$$) (x6989586621679375751 :: a6989586621679375750) (y6989586621679375752 :: a6989586621679375750) = (==) x6989586621679375751 y6989586621679375752 Source #
data (/=@#@$) :: forall a6989586621679375750. (~>) a6989586621679375750 ((~>) a6989586621679375750 Bool) infix 4 Source #
Instances
SEq a => SingI ((/=@#@$) :: TyFun a (a ~> Bool) -> Type) Source # | |
SuppressUnusedWarnings ((/=@#@$) :: TyFun a6989586621679375750 (a6989586621679375750 ~> Bool) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Eq Methods suppressUnusedWarnings :: () Source # | |
type Apply ((/=@#@$) :: TyFun a6989586621679375750 (a6989586621679375750 ~> Bool) -> Type) (x6989586621679375753 :: a6989586621679375750) Source # | |
data (/=@#@$$) (x6989586621679375753 :: a6989586621679375750) :: (~>) a6989586621679375750 Bool infix 4 Source #
Instances
(SEq a, SingI x) => SingI ((/=@#@$$) x :: TyFun a Bool -> Type) Source # | |
SuppressUnusedWarnings ((/=@#@$$) x6989586621679375753 :: TyFun a6989586621679375750 Bool -> Type) Source # | |
Defined in Data.Singletons.Prelude.Eq Methods suppressUnusedWarnings :: () Source # | |
type Apply ((/=@#@$$) x6989586621679375753 :: TyFun a Bool -> Type) (y6989586621679375754 :: a) Source # | |
Defined in Data.Singletons.Prelude.Eq |
type (/=@#@$$$) (x6989586621679375753 :: a6989586621679375750) (y6989586621679375754 :: a6989586621679375750) = (/=) x6989586621679375753 y6989586621679375754 Source #
data DefaultEqSym0 :: forall k6989586621679375744. (~>) k6989586621679375744 ((~>) k6989586621679375744 Bool) Source #
Instances
SuppressUnusedWarnings (DefaultEqSym0 :: TyFun k6989586621679375744 (k6989586621679375744 ~> Bool) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Eq Methods suppressUnusedWarnings :: () Source # | |
type Apply (DefaultEqSym0 :: TyFun k6989586621679375744 (k6989586621679375744 ~> Bool) -> Type) (a6989586621679375745 :: k6989586621679375744) Source # | |
Defined in Data.Singletons.Prelude.Eq type Apply (DefaultEqSym0 :: TyFun k6989586621679375744 (k6989586621679375744 ~> Bool) -> Type) (a6989586621679375745 :: k6989586621679375744) = DefaultEqSym1 a6989586621679375745 |
data DefaultEqSym1 (a6989586621679375745 :: k6989586621679375744) :: (~>) k6989586621679375744 Bool Source #
Instances
SuppressUnusedWarnings (DefaultEqSym1 a6989586621679375745 :: TyFun k6989586621679375744 Bool -> Type) Source # | |
Defined in Data.Singletons.Prelude.Eq Methods suppressUnusedWarnings :: () Source # | |
type Apply (DefaultEqSym1 a6989586621679375745 :: TyFun k Bool -> Type) (b6989586621679375746 :: k) Source # | |
Defined in Data.Singletons.Prelude.Eq type Apply (DefaultEqSym1 a6989586621679375745 :: TyFun k Bool -> Type) (b6989586621679375746 :: k) = DefaultEq a6989586621679375745 b6989586621679375746 |
type DefaultEqSym2 (a6989586621679375745 :: k6989586621679375744) (b6989586621679375746 :: k6989586621679375744) = DefaultEq a6989586621679375745 b6989586621679375746 Source #