Copyright	(C) 2013 Richard Eisenberg
License	BSD-style (see LICENSE)
Maintainer	Richard Eisenberg (rae@cs.brynmawr.edu)
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

Data.Singletons.Decide

Contents

The SDecide class
Supporting definitions
Orphan instances

Description

Defines the class SDecide, allowing for decidable equality over singletons.

Synopsis

class SDecide k where
data (a :: k) :~: (b :: k) :: forall k. k -> k -> * where
- Refl :: a :~: a
data Void
type Refuted a = a -> Void
data Decision a
- = Proved a
- | Disproved (Refuted a)

The SDecide class

class SDecide k where #

Members of the SDecide "kind" class support decidable equality. Instances of this class are generated alongside singleton definitions for datatypes that derive an Eq instance.

Minimal complete definition

(%~)

Methods

(%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b) infix 4 #

Compute a proof or disproof of equality, given two singletons.

Instances

SDecide Bool #
Instance details Defined in Data.Singletons.Prelude.Instances Methods (%~) :: Sing a -> Sing b -> Decision (a :~: b) #
SDecide Ordering #
Instance details Defined in Data.Singletons.Prelude.Instances Methods (%~) :: Sing a -> Sing b -> Decision (a :~: b) #
SDecide Type #
Instance details Defined in Data.Singletons.TypeRepStar Methods (%~) :: Sing a -> Sing b -> Decision (a :~: b) #
SDecide Nat #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods (%~) :: Sing a -> Sing b -> Decision (a :~: b) #
SDecide Symbol #
Instance details Defined in Data.Singletons.TypeLits.Internal Methods (%~) :: Sing a -> Sing b -> Decision (a :~: b) #
SDecide () #
Instance details Defined in Data.Singletons.Prelude.Instances Methods (%~) :: Sing a -> Sing b -> Decision (a :~: b) #
SDecide Void #
Instance details Defined in Data.Singletons.Prelude.Instances Methods (%~) :: Sing a -> Sing b -> Decision (a :~: b) #
(SDecide a, SDecide [a]) => SDecide [a] #
Instance details Defined in Data.Singletons.Prelude.Instances Methods (%~) :: Sing a0 -> Sing b -> Decision (a0 :~: b) #
SDecide a => SDecide (Maybe a) #
Instance details Defined in Data.Singletons.Prelude.Instances Methods (%~) :: Sing a0 -> Sing b -> Decision (a0 :~: b) #
(SDecide a, SDecide [a]) => SDecide (NonEmpty a) #
Instance details Defined in Data.Singletons.Prelude.Instances Methods (%~) :: Sing a0 -> Sing b -> Decision (a0 :~: b) #
(SDecide a, SDecide b) => SDecide (Either a b) #
Instance details Defined in Data.Singletons.Prelude.Instances Methods (%~) :: Sing a0 -> Sing b0 -> Decision (a0 :~: b0) #
(SDecide a, SDecide b) => SDecide (a, b) #
Instance details Defined in Data.Singletons.Prelude.Instances Methods (%~) :: Sing a0 -> Sing b0 -> Decision (a0 :~: b0) #
(SDecide a, SDecide b, SDecide c) => SDecide (a, b, c) #
Instance details Defined in Data.Singletons.Prelude.Instances Methods (%~) :: Sing a0 -> Sing b0 -> Decision (a0 :~: b0) #
(SDecide a, SDecide b, SDecide c, SDecide d) => SDecide (a, b, c, d) #
Instance details Defined in Data.Singletons.Prelude.Instances Methods (%~) :: Sing a0 -> Sing b0 -> Decision (a0 :~: b0) #
(SDecide a, SDecide b, SDecide c, SDecide d, SDecide e) => SDecide (a, b, c, d, e) #
Instance details Defined in Data.Singletons.Prelude.Instances Methods (%~) :: Sing a0 -> Sing b0 -> Decision (a0 :~: b0) #
(SDecide a, SDecide b, SDecide c, SDecide d, SDecide e, SDecide f) => SDecide (a, b, c, d, e, f) #
Instance details Defined in Data.Singletons.Prelude.Instances Methods (%~) :: Sing a0 -> Sing b0 -> Decision (a0 :~: b0) #
(SDecide a, SDecide b, SDecide c, SDecide d, SDecide e, SDecide f, SDecide g) => SDecide (a, b, c, d, e, f, g) #
Instance details Defined in Data.Singletons.Prelude.Instances Methods (%~) :: Sing a0 -> Sing b0 -> Decision (a0 :~: b0) #

Supporting definitions

data (a :: k) :~: (b :: k) :: forall k. k -> k -> * where infix 4 #

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

Constructors

Refl :: a :~: a

Instances

TestCoercion ((:~:) a :: k -> *)	Since: base-4.7.0.0
Instance details Defined in Data.Type.Coercion Methods testCoercion :: (a :~: a0) -> (a :~: b) -> Maybe (Coercion a0 b) #
TestEquality ((:~:) a :: k -> *)	Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods testEquality :: (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) #
a ~ b => Bounded (a :~: b)	Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods minBound :: a :~: b # maxBound :: a :~: b #
a ~ b => Enum (a :~: b)	Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods succ :: (a :~: b) -> a :~: b # pred :: (a :~: b) -> a :~: b # toEnum :: Int -> a :~: b # fromEnum :: (a :~: b) -> Int # enumFrom :: (a :~: b) -> [a :~: b] # enumFromThen :: (a :~: b) -> (a :~: b) -> [a :~: b] # enumFromTo :: (a :~: b) -> (a :~: b) -> [a :~: b] # enumFromThenTo :: (a :~: b) -> (a :~: b) -> (a :~: b) -> [a :~: b] #
Eq (a :~: b)
Instance details Defined in Data.Type.Equality Methods (==) :: (a :~: b) -> (a :~: b) -> Bool # (/=) :: (a :~: b) -> (a :~: b) -> Bool #
(a ~ b, Data a) => Data (a :~: b)	Since: base-4.7.0.0
Instance details Defined in Data.Data Methods gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> (a :~: b) -> c (a :~: b) # gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (a :~: b) # toConstr :: (a :~: b) -> Constr # dataTypeOf :: (a :~: b) -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (a :~: b)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (a :~: b)) # gmapT :: (forall b0. Data b0 => b0 -> b0) -> (a :~: b) -> a :~: b # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r # gmapQ :: (forall d. Data d => d -> u) -> (a :~: b) -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> (a :~: b) -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) #
Ord (a :~: b)
Instance details Defined in Data.Type.Equality Methods compare :: (a :~: b) -> (a :~: b) -> Ordering # (<) :: (a :~: b) -> (a :~: b) -> Bool # (<=) :: (a :~: b) -> (a :~: b) -> Bool # (>) :: (a :~: b) -> (a :~: b) -> Bool # (>=) :: (a :~: b) -> (a :~: b) -> Bool # max :: (a :~: b) -> (a :~: b) -> a :~: b # min :: (a :~: b) -> (a :~: b) -> a :~: b #
a ~ b => Read (a :~: b)	Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods readsPrec :: Int -> ReadS (a :~: b) # readList :: ReadS [a :~: b] # readPrec :: ReadPrec (a :~: b) # readListPrec :: ReadPrec [a :~: b] #
Show (a :~: b)
Instance details Defined in Data.Type.Equality Methods showsPrec :: Int -> (a :~: b) -> ShowS # show :: (a :~: b) -> String # showList :: [a :~: b] -> ShowS #

data Void #

Uninhabited data type

Since: base-4.8.0.0

Instances

Eq Void	Since: base-4.8.0.0
Instance details Defined in Data.Void Methods (==) :: Void -> Void -> Bool # (/=) :: Void -> Void -> Bool #
Data Void	Since: base-4.8.0.0
Instance details Defined in Data.Void Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Void -> c Void # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Void # toConstr :: Void -> Constr # dataTypeOf :: Void -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Void) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Void) # gmapT :: (forall b. Data b => b -> b) -> Void -> Void # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Void -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Void -> r # gmapQ :: (forall d. Data d => d -> u) -> Void -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Void -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Void -> m Void # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Void -> m Void # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Void -> m Void #
Ord Void	Since: base-4.8.0.0
Instance details Defined in Data.Void Methods compare :: Void -> Void -> Ordering # (<) :: Void -> Void -> Bool # (<=) :: Void -> Void -> Bool # (>) :: Void -> Void -> Bool # (>=) :: Void -> Void -> Bool # max :: Void -> Void -> Void # min :: Void -> Void -> Void #
Read Void	Reading a `Void` value is always a parse error, considering `Void` as a data type with no constructors. Since: base-4.8.0.0
Instance details Defined in Data.Void Methods readsPrec :: Int -> ReadS Void # readList :: ReadS [Void] # readPrec :: ReadPrec Void # readListPrec :: ReadPrec [Void] #
Show Void	Since: base-4.8.0.0
Instance details Defined in Data.Void Methods showsPrec :: Int -> Void -> ShowS # show :: Void -> String # showList :: [Void] -> ShowS #
Ix Void	Since: base-4.8.0.0
Instance details Defined in Data.Void Methods range :: (Void, Void) -> [Void] # index :: (Void, Void) -> Void -> Int # unsafeIndex :: (Void, Void) -> Void -> Int inRange :: (Void, Void) -> Void -> Bool # rangeSize :: (Void, Void) -> Int # unsafeRangeSize :: (Void, Void) -> Int
Generic Void
Instance details Defined in Data.Void Associated Types type Rep Void :: * -> * # Methods from :: Void -> Rep Void x # to :: Rep Void x -> Void #
Semigroup Void	Since: base-4.9.0.0
Instance details Defined in Data.Void Methods (<>) :: Void -> Void -> Void # sconcat :: NonEmpty Void -> Void # stimes :: Integral b => b -> Void -> Void #
Exception Void	Since: base-4.8.0.0
Instance details Defined in Data.Void Methods toException :: Void -> SomeException # fromException :: SomeException -> Maybe Void # displayException :: Void -> String #
SingKind Void #
Instance details Defined in Data.Singletons.Prelude.Instances Associated Types type Demote Void = (r :: *) # Methods fromSing :: Sing a -> Demote Void # toSing :: Demote Void -> SomeSing Void #
SDecide Void #
Instance details Defined in Data.Singletons.Prelude.Instances Methods (%~) :: Sing a -> Sing b -> Decision (a :~: b) #
PEq Void #
Instance details Defined in Data.Singletons.Prelude.Eq Associated Types type x == y :: Bool # type x /= y :: Bool #
SEq Void #
Instance details Defined in Data.Singletons.Prelude.Eq Methods (%==) :: Sing a -> Sing b -> Sing (a == b) # (%/=) :: Sing a -> Sing b -> Sing (a /= b) #
SOrd Void #
Instance details Defined in Data.Singletons.Prelude.Ord Methods sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) # (%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) # (%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) # (%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) # (%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) # sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) # sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) #
POrd Void #
Instance details Defined in Data.Singletons.Prelude.Ord Associated Types type Compare arg arg :: Ordering # type arg < arg :: Bool # type arg <= arg :: Bool # type arg > arg :: Bool # type arg >= arg :: Bool # type Max arg arg :: a # type Min arg arg :: a #
ShowSing Void #
Instance details Defined in Data.Singletons.ShowSing Methods showsSingPrec :: Int -> Sing a -> ShowS #
SShow Void #
Instance details Defined in Data.Singletons.Prelude.Show Methods sShowsPrec :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ShowsPrecSym0 t) t) t) # sShow_ :: Sing t -> Sing (Apply Show_Sym0 t) # sShowList :: Sing t -> Sing t -> Sing (Apply (Apply ShowListSym0 t) t) #
PShow Void #
Instance details Defined in Data.Singletons.Prelude.Show Associated Types type ShowsPrec arg arg arg :: Symbol # type Show_ arg :: Symbol # type ShowList arg arg :: Symbol #
Show (Sing z) #
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS # show :: Sing z -> String # showList :: [Sing z] -> ShowS #
SuppressUnusedWarnings (AbsurdSym0 :: TyFun Void a6989586621679296691 -> *) #
Instance details Defined in Data.Singletons.Prelude.Void Methods suppressUnusedWarnings :: () #
type Rep Void	Since: base-4.8.0.0
Instance details Defined in Data.Void type Rep Void = D1 (MetaData "Void" "Data.Void" "base" False) (V1 :: * -> *)
type Demote Void #
Instance details Defined in Data.Singletons.Prelude.Instances type Demote Void = Void
data Sing (z :: Void) #
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (z :: Void)
type Show_ (arg :: Void) #
Instance details Defined in Data.Singletons.Prelude.Show type Show_ (arg :: Void)
type (a :: Void) == (b :: Void) #
Instance details Defined in Data.Singletons.Prelude.Eq type (a :: Void) == (b :: Void)
type (x :: Void) /= (y :: Void) #
Instance details Defined in Data.Singletons.Prelude.Eq type (x :: Void) /= (y :: Void) = Not (x == y)
type Compare (a1 :: Void) (a2 :: Void) #
Instance details Defined in Data.Singletons.Prelude.Ord type Compare (a1 :: Void) (a2 :: Void)
type (arg1 :: Void) < (arg2 :: Void) #
Instance details Defined in Data.Singletons.Prelude.Ord type (arg1 :: Void) < (arg2 :: Void)
type (arg1 :: Void) <= (arg2 :: Void) #
Instance details Defined in Data.Singletons.Prelude.Ord type (arg1 :: Void) <= (arg2 :: Void)
type (arg1 :: Void) > (arg2 :: Void) #
Instance details Defined in Data.Singletons.Prelude.Ord type (arg1 :: Void) > (arg2 :: Void)
type (arg1 :: Void) >= (arg2 :: Void) #
Instance details Defined in Data.Singletons.Prelude.Ord type (arg1 :: Void) >= (arg2 :: Void)
type Max (arg1 :: Void) (arg2 :: Void) #
Instance details Defined in Data.Singletons.Prelude.Ord type Max (arg1 :: Void) (arg2 :: Void)
type Min (arg1 :: Void) (arg2 :: Void) #
Instance details Defined in Data.Singletons.Prelude.Ord type Min (arg1 :: Void) (arg2 :: Void)
type ShowList (arg1 :: [Void]) arg2 #
Instance details Defined in Data.Singletons.Prelude.Show type ShowList (arg1 :: [Void]) arg2
type ShowsPrec a1 (a2 :: Void) a3 #
Instance details Defined in Data.Singletons.Prelude.Show type ShowsPrec a1 (a2 :: Void) a3
type Apply (AbsurdSym0 :: TyFun Void k2 -> *) (l :: Void) #
Instance details Defined in Data.Singletons.Prelude.Void type Apply (AbsurdSym0 :: TyFun Void k2 -> *) (l :: Void) = (Absurd l :: k2)

type Refuted a = a -> Void #

Because we can never create a value of type Void, a function that type-checks at a -> Void shows that objects of type a can never exist. Thus, we say that a is Refuted

data Decision a #

A Decision about a type a is either a proof of existence or a proof that a cannot exist.

Constructors

Proved a	Witness for `a`
Disproved (Refuted a)	Proof that no `a` exists

Orphan instances

SDecide k => TestCoercion (Sing :: k -> *) #
Instance details Methods testCoercion :: Sing a -> Sing b -> Maybe (Coercion a b) #
SDecide k => TestEquality (Sing :: k -> *) #
Instance details Methods testEquality :: Sing a -> Sing b -> Maybe (a :~: b) #