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.Decide

Contents

The SDecide class
Supporting definitions
Orphan instances

Description

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

Synopsis

The SDecide class

class SDecide k where Source #

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 b. Sing a -> Sing b -> Decision (a :~: b) Source #

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

Supporting definitions

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

Constructors

Refl :: (:~:) k a a

Instances

TestCoercion k ((:~:) k a)
Methods testCoercion :: f a -> f b -> Maybe (Coercion (k :~: a) a b) #
TestEquality k ((:~:) k a)
Methods testEquality :: f a -> f b -> Maybe (((k :~: a) :~: a) b) #
(~) k a b => Bounded ((:~:) k a b)
Methods minBound :: (k :~: a) b # maxBound :: (k :~: a) b #
(~) k a b => Enum ((:~:) k a b)
Methods succ :: (k :~: a) b -> (k :~: a) b # pred :: (k :~: a) b -> (k :~: a) b # toEnum :: Int -> (k :~: a) b # fromEnum :: (k :~: a) b -> Int # enumFrom :: (k :~: a) b -> [(k :~: a) b] # enumFromThen :: (k :~: a) b -> (k :~: a) b -> [(k :~: a) b] # enumFromTo :: (k :~: a) b -> (k :~: a) b -> [(k :~: a) b] # enumFromThenTo :: (k :~: a) b -> (k :~: a) b -> (k :~: a) b -> [(k :~: a) b] #
Eq ((:~:) k a b)
Methods (==) :: (k :~: a) b -> (k :~: a) b -> Bool # (/=) :: (k :~: a) b -> (k :~: a) b -> Bool #
((~) * a b, Data a) => Data ((:~:) * a b)
Methods gfoldl :: (forall d c. Data d => c (d -> c) -> d -> c c) -> (forall g. g -> c g) -> (* :~: a) b -> c ((* :~: a) b) # gunfold :: (forall c r. Data c => c (c -> 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 c. Data c => c -> c) -> (* :~: 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 ((:~:) k a b)
Methods compare :: (k :~: a) b -> (k :~: a) b -> Ordering # (<) :: (k :~: a) b -> (k :~: a) b -> Bool # (<=) :: (k :~: a) b -> (k :~: a) b -> Bool # (>) :: (k :~: a) b -> (k :~: a) b -> Bool # (>=) :: (k :~: a) b -> (k :~: a) b -> Bool # max :: (k :~: a) b -> (k :~: a) b -> (k :~: a) b # min :: (k :~: a) b -> (k :~: a) b -> (k :~: a) b #
(~) k a b => Read ((:~:) k a b)
Methods readsPrec :: Int -> ReadS ((k :~: a) b) # readList :: ReadS [(k :~: a) b] # readPrec :: ReadPrec ((k :~: a) b) # readListPrec :: ReadPrec [(k :~: a) b] #
Show ((:~:) k a b)
Methods showsPrec :: Int -> (k :~: a) b -> ShowS # show :: (k :~: a) b -> String # showList :: [(k :~: a) b] -> ShowS #

data Void :: * #

Uninhabited data type

Since: 4.8.0.0

Instances

Eq Void
Methods (==) :: Void -> Void -> Bool # (/=) :: Void -> Void -> Bool #
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
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.
Methods readsPrec :: Int -> ReadS Void # readList :: ReadS [Void] # readPrec :: ReadPrec Void # readListPrec :: ReadPrec [Void] #
Show Void
Methods showsPrec :: Int -> Void -> ShowS # show :: Void -> String # showList :: [Void] -> ShowS #
Ix 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
Associated Types type Rep Void :: * -> * # Methods from :: Void -> Rep Void x # to :: Rep Void x -> Void #
Semigroup Void
Methods (<>) :: Void -> Void -> Void # sconcat :: NonEmpty Void -> Void # stimes :: Integral b => b -> Void -> Void #
Exception Void
Methods toException :: Void -> SomeException # fromException :: SomeException -> Maybe Void # displayException :: Void -> String #
type Rep Void
type Rep Void = D1 (MetaData "Void" "Data.Void" "base" False) V1

type Refuted a = a -> Void Source #

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 Source #

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 k2 => TestEquality k2 (Sing k2) Source #
Methods testEquality :: f a -> f b -> Maybe ((Sing k2 :~: a) b) #