| 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 a6989586621679381437. (~>) a6989586621679381437 ((~>) a6989586621679381437 Bool)
- data (==@#@$$) (x6989586621679381438 :: a6989586621679381437) :: (~>) a6989586621679381437 Bool
- type (==@#@$$$) (x6989586621679381438 :: a6989586621679381437) (y6989586621679381439 :: a6989586621679381437) = (==) x6989586621679381438 y6989586621679381439
- data (/=@#@$) :: forall a6989586621679381437. (~>) a6989586621679381437 ((~>) a6989586621679381437 Bool)
- data (/=@#@$$) (x6989586621679381440 :: a6989586621679381437) :: (~>) a6989586621679381437 Bool
- type (/=@#@$$$) (x6989586621679381440 :: a6989586621679381437) (y6989586621679381441 :: a6989586621679381437) = (/=) x6989586621679381440 y6989586621679381441
- data DefaultEqSym0 :: forall k6989586621679381431. (~>) k6989586621679381431 ((~>) k6989586621679381431 Bool)
- data DefaultEqSym1 (a6989586621679381432 :: k6989586621679381431) :: (~>) k6989586621679381431 Bool
- type DefaultEqSym2 (a6989586621679381432 :: k6989586621679381431) (b6989586621679381433 :: k6989586621679381431) = DefaultEq a6989586621679381432 b6989586621679381433
Documentation
The promoted analogue of Eq. If you supply no definition for '(==)',
then it defaults to a use of DefaultEq.
Instances
| PEq Bool # | |
| PEq Ordering # | |
| PEq Nat # | |
| PEq Symbol # | |
| PEq () # | |
| PEq Void # | |
| PEq All # | |
| PEq Any # | |
| PEq [a] # | |
| PEq (Maybe a) # | |
| PEq (TYPE rep) # | |
| PEq (Min a) # | |
| PEq (Max a) # | |
| PEq (First a) # | |
| PEq (Last a) # | |
| PEq (WrappedMonoid m) # | |
| PEq (Option a) # | |
| PEq (Identity a) # | |
| PEq (First a) # | |
| PEq (Last a) # | |
| PEq (Dual a) # | |
| PEq (Sum a) # | |
| PEq (Product a) # | |
| PEq (Down a) # | |
| PEq (NonEmpty a) # | |
| PEq (Either a b) # | |
| PEq (a, b) # | |
| PEq (Arg a b) # | |
| PEq (a, b, c) # | |
| PEq (Const a b) # | |
| PEq (a, b, c, d) # | |
| PEq (a, b, c, d, e) # | |
| PEq (a, b, c, d, e, f) # | |
| PEq (a, b, c, d, e, f, g) # | |
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 #
Boolean equality on singletons
(%/=) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a /= b) infix 4 #
Boolean disequality on singletons
(%/=) :: forall (a :: k) (b :: k). (a /= b) ~ Not (a == b) => Sing a -> Sing b -> Sing (a /= b) infix 4 #
Boolean disequality on singletons
Instances
| SEq Bool # | |
| SEq Ordering # | |
| SEq Nat # | |
| SEq Symbol # | |
| SEq () # | |
| SEq Void # | |
| SEq Bool => SEq All # | |
| SEq Bool => SEq Any # | |
| (SEq a, SEq [a]) => SEq [a] # | |
| SEq a => SEq (Maybe a) # | |
| SEq (TYPE rep) # | |
| SEq a => SEq (Min a) # | |
| SEq a => SEq (Max a) # | |
| SEq a => SEq (First a) # | |
| SEq a => SEq (Last a) # | |
| SEq m => SEq (WrappedMonoid m) # | |
| SEq (Maybe a) => SEq (Option a) # | |
| SEq a => SEq (Identity a) # | |
| SEq (Maybe a) => SEq (First a) # | |
| SEq (Maybe a) => SEq (Last a) # | |
| SEq a => SEq (Dual a) # | |
| SEq a => SEq (Sum a) # | |
| SEq a => SEq (Product a) # | |
| SEq a => SEq (Down a) # | |
| (SEq a, SEq [a]) => SEq (NonEmpty a) # | |
| (SEq a, SEq b) => SEq (Either a b) # | |
| (SEq a, SEq b) => SEq (a, b) # | |
| SEq a => SEq (Arg a b) # | |
| (SEq a, SEq b, SEq c) => SEq (a, b, c) # | |
| SEq a => SEq (Const a b) # | |
| (SEq a, SEq b, SEq c, SEq d) => SEq (a, b, c, d) # | |
| (SEq a, SEq b, SEq c, SEq d, SEq e) => SEq (a, b, c, d, e) # | |
| (SEq a, SEq b, SEq c, SEq d, SEq e, SEq f) => SEq (a, b, c, d, e, f) # | |
| (SEq a, SEq b, SEq c, SEq d, SEq e, SEq f, SEq g) => SEq (a, b, c, d, e, f, g) # | |
type family DefaultEq (a :: k) (b :: k) :: Bool where ... #
A sensible way to compute Boolean equality for types of any kind. Note
that this definition is slightly different from the '(DTE.==)' type family
from Data.Type.Equality in base, as '(DTE.==)' attempts to distinguish
applications of type constructors from other types. As a result,
a == a does not reduce to True for every a, but DefaultEq a aTrue for every a. The latter behavior is more desirable
for singletons' purposes, so we use it instead of '(DTE.==)'.
Defunctionalization symbols
data (==@#@$) :: forall a6989586621679381437. (~>) a6989586621679381437 ((~>) a6989586621679381437 Bool) infix 4 #
Instances
| SEq a => SingI ((==@#@$) :: TyFun a (a ~> Bool) -> Type) # | |
Defined in Data.Singletons.Prelude.Eq | |
| SuppressUnusedWarnings ((==@#@$) :: TyFun a6989586621679381437 (a6989586621679381437 ~> Bool) -> Type) # | |
Defined in Data.Singletons.Prelude.Eq Methods suppressUnusedWarnings :: () # | |
| type Apply ((==@#@$) :: TyFun a6989586621679381437 (a6989586621679381437 ~> Bool) -> Type) (x6989586621679381438 :: a6989586621679381437) # | |
data (==@#@$$) (x6989586621679381438 :: a6989586621679381437) :: (~>) a6989586621679381437 Bool infix 4 #
Instances
| (SEq a, SingI x) => SingI ((==@#@$$) x :: TyFun a Bool -> Type) # | |
Defined in Data.Singletons.Prelude.Eq | |
| SuppressUnusedWarnings ((==@#@$$) x6989586621679381438 :: TyFun a6989586621679381437 Bool -> Type) # | |
Defined in Data.Singletons.Prelude.Eq Methods suppressUnusedWarnings :: () # | |
| type Apply ((==@#@$$) x6989586621679381438 :: TyFun a Bool -> Type) (y6989586621679381439 :: a) # | |
type (==@#@$$$) (x6989586621679381438 :: a6989586621679381437) (y6989586621679381439 :: a6989586621679381437) = (==) x6989586621679381438 y6989586621679381439 #
data (/=@#@$) :: forall a6989586621679381437. (~>) a6989586621679381437 ((~>) a6989586621679381437 Bool) infix 4 #
Instances
| SEq a => SingI ((/=@#@$) :: TyFun a (a ~> Bool) -> Type) # | |
Defined in Data.Singletons.Prelude.Eq | |
| SuppressUnusedWarnings ((/=@#@$) :: TyFun a6989586621679381437 (a6989586621679381437 ~> Bool) -> Type) # | |
Defined in Data.Singletons.Prelude.Eq Methods suppressUnusedWarnings :: () # | |
| type Apply ((/=@#@$) :: TyFun a6989586621679381437 (a6989586621679381437 ~> Bool) -> Type) (x6989586621679381440 :: a6989586621679381437) # | |
data (/=@#@$$) (x6989586621679381440 :: a6989586621679381437) :: (~>) a6989586621679381437 Bool infix 4 #
Instances
| (SEq a, SingI x) => SingI ((/=@#@$$) x :: TyFun a Bool -> Type) # | |
Defined in Data.Singletons.Prelude.Eq | |
| SuppressUnusedWarnings ((/=@#@$$) x6989586621679381440 :: TyFun a6989586621679381437 Bool -> Type) # | |
Defined in Data.Singletons.Prelude.Eq Methods suppressUnusedWarnings :: () # | |
| type Apply ((/=@#@$$) x6989586621679381440 :: TyFun a Bool -> Type) (y6989586621679381441 :: a) # | |
type (/=@#@$$$) (x6989586621679381440 :: a6989586621679381437) (y6989586621679381441 :: a6989586621679381437) = (/=) x6989586621679381440 y6989586621679381441 #
data DefaultEqSym0 :: forall k6989586621679381431. (~>) k6989586621679381431 ((~>) k6989586621679381431 Bool) #
Instances
| SuppressUnusedWarnings (DefaultEqSym0 :: TyFun k6989586621679381431 (k6989586621679381431 ~> Bool) -> Type) # | |
Defined in Data.Singletons.Prelude.Eq Methods suppressUnusedWarnings :: () # | |
| type Apply (DefaultEqSym0 :: TyFun k6989586621679381431 (k6989586621679381431 ~> Bool) -> Type) (a6989586621679381432 :: k6989586621679381431) # | |
Defined in Data.Singletons.Prelude.Eq type Apply (DefaultEqSym0 :: TyFun k6989586621679381431 (k6989586621679381431 ~> Bool) -> Type) (a6989586621679381432 :: k6989586621679381431) = DefaultEqSym1 a6989586621679381432 | |
data DefaultEqSym1 (a6989586621679381432 :: k6989586621679381431) :: (~>) k6989586621679381431 Bool #
Instances
| SuppressUnusedWarnings (DefaultEqSym1 a6989586621679381432 :: TyFun k6989586621679381431 Bool -> Type) # | |
Defined in Data.Singletons.Prelude.Eq Methods suppressUnusedWarnings :: () # | |
| type Apply (DefaultEqSym1 a6989586621679381432 :: TyFun k Bool -> Type) (b6989586621679381433 :: k) # | |
Defined in Data.Singletons.Prelude.Eq | |
type DefaultEqSym2 (a6989586621679381432 :: k6989586621679381431) (b6989586621679381433 :: k6989586621679381431) = DefaultEq a6989586621679381432 b6989586621679381433 #