singletons-2.4: 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) infix 4 Source #

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

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: 4.7.0.0

Constructors

 Refl :: a :~: a
Instances

data Void :: * #

Uninhabited data type

Since: 4.8.0.0

Instances
 Since: 4.8.0.0 Instance detailsMethods(==) :: Void -> Void -> Bool #(/=) :: Void -> Void -> Bool # Since: 4.8.0.0 Instance detailsMethodsgfoldl :: (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 Instance detailsMethodscompare :: 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 Instance detailsMethods Since: 4.8.0.0 Instance detailsMethodsshowsPrec :: Int -> Void -> ShowS #show :: Void -> String #showList :: [Void] -> ShowS # Since: 4.8.0.0 Instance detailsMethodsrange :: (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 Instance detailsAssociated Typestype Rep Void :: * -> * # Methodsfrom :: Void -> Rep Void x #to :: Rep Void x -> Void # Since: 4.9.0.0 Instance detailsMethods(<>) :: Void -> Void -> Void #stimes :: Integral b => b -> Void -> Void # Since: 4.8.0.0 Instance detailsMethods Source # Instance detailsAssociated Typestype x == y :: Bool Source #type x /= y :: Bool Source # Source # Instance detailsMethods(%==) :: Sing a -> Sing b -> Sing (a == b) Source #(%/=) :: Sing a -> Sing b -> Sing (a /= b) Source # Source # Instance detailsMethodssCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #(%<=) :: Sing t -> Sing t -> Sing (Apply (Apply (<=@#@$) t) t) Source #(%>) :: Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source #(%>=) :: Sing t -> Sing t -> Sing (Apply (Apply (>=@#@$) t) t) Source #sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source # Source # Instance detailsAssociated Typestype Compare arg arg :: Ordering Source #type arg < arg :: Bool Source #type arg <= arg :: Bool Source #type arg > arg :: Bool Source #type arg >= arg :: Bool Source #type Max arg arg :: a Source #type Min arg arg :: a Source # Source # Instance detailsMethodsshowsSingPrec :: Int -> Sing a -> ShowS Source # Source # Instance detailsMethodssShowsPrec :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ShowsPrecSym0 t) t) t) Source #sShow_ :: Sing t -> Sing (Apply Show_Sym0 t) Source #sShowList :: Sing t -> Sing t -> Sing (Apply (Apply ShowListSym0 t) t) Source # Source # Instance detailsAssociated Typestype ShowsPrec arg arg arg :: Symbol Source #type Show_ arg :: Symbol Source #type ShowList arg arg :: Symbol Source # SuppressUnusedWarnings (AbsurdSym0 :: TyFun Void a6989586621679285232 -> *) Source # Instance detailsMethods type Rep Void Since: 4.8.0.0 Instance detailstype Rep Void = D1 (MetaData "Void" "Data.Void" "base" False) (V1 :: * -> *) type Demote Void Source # Instance detailstype Demote Void = Void data Sing (z :: Void) Source # Instance detailsdata Sing (z :: Void) type Show_ (arg :: Void) Source # Instance detailstype Show_ (arg :: Void) type (a :: Void) == (b :: Void) Source # Instance detailstype (a :: Void) == (b :: Void) type (x :: Void) /= (y :: Void) Source # Instance detailstype (x :: Void) /= (y :: Void) = Not (x == y) type Compare (a1 :: Void) (a2 :: Void) Source # Instance detailstype Compare (a1 :: Void) (a2 :: Void) type (arg1 :: Void) < (arg2 :: Void) Source # Instance detailstype (arg1 :: Void) < (arg2 :: Void) type (arg1 :: Void) <= (arg2 :: Void) Source # Instance detailstype (arg1 :: Void) <= (arg2 :: Void) type (arg1 :: Void) > (arg2 :: Void) Source # Instance detailstype (arg1 :: Void) > (arg2 :: Void) type (arg1 :: Void) >= (arg2 :: Void) Source # Instance detailstype (arg1 :: Void) >= (arg2 :: Void) type Max (arg1 :: Void) (arg2 :: Void) Source # Instance detailstype Max (arg1 :: Void) (arg2 :: Void) type Min (arg1 :: Void) (arg2 :: Void) Source # Instance detailstype Min (arg1 :: Void) (arg2 :: Void) type ShowList (arg1 :: [Void]) arg2 Source # Instance detailstype ShowList (arg1 :: [Void]) arg2 type ShowsPrec a1 (a2 :: Void) a3 Source # Instance detailstype ShowsPrec a1 (a2 :: Void) a3 type Apply (AbsurdSym0 :: TyFun Void k2 -> *) (l :: Void) Source # Instance detailstype Apply (AbsurdSym0 :: TyFun Void k2 -> *) (l :: Void) = (Absurd l :: k2)

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 k => TestCoercion (Sing :: k -> *) Source # Instance detailsMethodstestCoercion :: Sing a -> Sing b -> Maybe (Coercion a b) # SDecide k => TestEquality (Sing :: k -> *) Source # Instance detailsMethodstestEquality :: Sing a -> Sing b -> Maybe (a :~: b) #