singletons-2.2: A framework for generating singleton types

Data.Singletons.Decide

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) MethodstestCoercion :: f a -> f b -> Maybe (Coercion (k :~: a) a b) # TestEquality k ((:~:) k a) MethodstestEquality :: f a -> f b -> Maybe (((k :~: a) :~: a) b) # (~) k a b => Bounded ((:~:) k a b) MethodsminBound :: (k :~: a) b #maxBound :: (k :~: a) b # (~) k a b => Enum ((:~:) k a b) Methodssucc :: (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) Methodsgfoldl :: (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) Methodscompare :: (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) MethodsreadsPrec :: Int -> ReadS ((k :~: a) b) #readList :: ReadS [(k :~: a) b] #readPrec :: ReadPrec ((k :~: a) b) #readListPrec :: ReadPrec [(k :~: a) b] # Show ((:~:) k a b) MethodsshowsPrec :: 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

 Methods(==) :: Void -> Void -> Bool #(/=) :: Void -> Void -> Bool # Methodsgfoldl :: (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 #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 # Methodscompare :: Void -> Void -> Ordering #(<) :: Void -> Void -> Bool #(<=) :: Void -> Void -> Bool #(>) :: Void -> Void -> Bool #(>=) :: Void -> Void -> Bool #max :: Void -> Void -> Void #min :: Void -> Void -> Void # Reading a Void value is always a parse error, considering Void as a data type with no constructors. Methods MethodsshowsPrec :: Int -> Void -> ShowS #show :: Void -> String #showList :: [Void] -> ShowS # Methodsrange :: (Void, Void) -> [Void] #index :: (Void, Void) -> Void -> Int #unsafeIndex :: (Void, Void) -> Void -> IntinRange :: (Void, Void) -> Void -> Bool #rangeSize :: (Void, Void) -> Int #unsafeRangeSize :: (Void, Void) -> Int Associated Typestype Rep Void :: * -> * # Methodsfrom :: Void -> Rep Void x #to :: Rep Void x -> Void # Methods(<>) :: Void -> Void -> Void #stimes :: Integral b => b -> Void -> Void # Methods 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 # MethodstestEquality :: f a -> f b -> Maybe ((Sing k2 :~: a) b) #