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

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

# Supporting definitions

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

Constructors

 Refl :: (:~:) k a a

Instances

data Void :: * #

Uninhabited data type

Since: 4.8.0.0

Instances

 Since: 4.8.0.0 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 # Since: 4.8.0.0 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. | @since 4.8.0.0 Methods Since: 4.8.0.0 MethodsshowsPrec :: Int -> Void -> ShowS #show :: Void -> String #showList :: [Void] -> ShowS # Since: 4.8.0.0 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 # Since: 4.9.0.0 Methods(<>) :: Void -> Void -> Void #stimes :: Integral b => b -> Void -> Void # Since: 4.8.0.0 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 k3 => TestEquality k3 (Sing k3) Source # MethodstestEquality :: f a -> f b -> Maybe ((Sing k3 :~: a) b) #