Safe Haskell	Safe
Language	Haskell98

Data.Parameterized.BoolRepr

Contents

Re-exports

Synopsis

module Data.Type.Bool
data BoolRepr (b :: Bool) where
- FalseRepr :: BoolRepr False
- TrueRepr :: BoolRepr True
ifRepr :: BoolRepr a -> BoolRepr b -> BoolRepr c -> BoolRepr (If a b c)
notRepr :: BoolRepr b -> BoolRepr (Not b)
(%&&) :: BoolRepr a -> BoolRepr b -> BoolRepr (a && b)
(%||) :: BoolRepr a -> BoolRepr b -> BoolRepr (a || b)
type KnownBool = KnownRepr BoolRepr
someBool :: Bool -> Some BoolRepr
class TestEquality (f :: k -> Type) where
- testEquality :: f a -> f b -> Maybe (a :~: b)
data (a :: k) :~: (b :: k) :: forall k. k -> k -> Type where
- Refl :: forall k (a :: k) (b :: k). a :~: a
data Some (f :: k -> *)

Documentation

module Data.Type.Bool

data BoolRepr (b :: Bool) where Source #

Constructors

FalseRepr :: BoolRepr False
TrueRepr :: BoolRepr True

Instances

TestEquality BoolRepr Source #
Instance details Defined in Data.Parameterized.BoolRepr Methods testEquality :: BoolRepr a -> BoolRepr b -> Maybe (a :~: b) #
HashableF BoolRepr Source #
Instance details Defined in Data.Parameterized.BoolRepr Methods hashWithSaltF :: Int -> BoolRepr tp -> Int Source # hashF :: BoolRepr tp -> Int Source #
ShowF BoolRepr Source #
Instance details Defined in Data.Parameterized.BoolRepr Methods withShow :: p BoolRepr -> q tp -> (Show (BoolRepr tp) -> a) -> a Source # showF :: BoolRepr tp -> String Source # showsPrecF :: Int -> BoolRepr tp -> String -> String Source #
OrdF BoolRepr Source #
Instance details Defined in Data.Parameterized.BoolRepr Methods compareF :: BoolRepr x -> BoolRepr y -> OrderingF x y Source # leqF :: BoolRepr x -> BoolRepr y -> Bool Source # ltF :: BoolRepr x -> BoolRepr y -> Bool Source # geqF :: BoolRepr x -> BoolRepr y -> Bool Source # gtF :: BoolRepr x -> BoolRepr y -> Bool Source #
DecidableEq BoolRepr Source #
Instance details Defined in Data.Parameterized.BoolRepr Methods decEq :: BoolRepr a -> BoolRepr b -> Either (a :~: b) ((a :~: b) -> Void) Source #
IsRepr BoolRepr Source #
Instance details Defined in Data.Parameterized.WithRepr Methods withRepr :: BoolRepr a -> (KnownRepr BoolRepr a -> r) -> r Source #
KnownRepr BoolRepr False Source #
Instance details Defined in Data.Parameterized.BoolRepr Methods knownRepr :: BoolRepr False Source #
KnownRepr BoolRepr True Source #
Instance details Defined in Data.Parameterized.BoolRepr Methods knownRepr :: BoolRepr True Source #
Eq (BoolRepr m) Source #
Instance details Defined in Data.Parameterized.BoolRepr Methods (==) :: BoolRepr m -> BoolRepr m -> Bool # (/=) :: BoolRepr m -> BoolRepr m -> Bool #
Show (BoolRepr m) Source #
Instance details Defined in Data.Parameterized.BoolRepr Methods showsPrec :: Int -> BoolRepr m -> ShowS # show :: BoolRepr m -> String # showList :: [BoolRepr m] -> ShowS #
Hashable (BoolRepr n) Source #
Instance details Defined in Data.Parameterized.BoolRepr Methods hashWithSalt :: Int -> BoolRepr n -> Int # hash :: BoolRepr n -> Int #
PolyEq (BoolRepr m) (BoolRepr n) Source #
Instance details Defined in Data.Parameterized.BoolRepr Methods polyEqF :: BoolRepr m -> BoolRepr n -> Maybe (BoolRepr m :~: BoolRepr n) Source # polyEq :: BoolRepr m -> BoolRepr n -> Bool Source #

ifRepr :: BoolRepr a -> BoolRepr b -> BoolRepr c -> BoolRepr (If a b c) Source #

conditional

notRepr :: BoolRepr b -> BoolRepr (Not b) Source #

negation

(%&&) :: BoolRepr a -> BoolRepr b -> BoolRepr (a && b) infixr 3 Source #

Conjunction

(%||) :: BoolRepr a -> BoolRepr b -> BoolRepr (a || b) infixr 2 Source #

Disjunction

type KnownBool = KnownRepr BoolRepr Source #

someBool :: Bool -> Some BoolRepr Source #

Re-exports

class TestEquality (f :: k -> Type) where #

This class contains types where you can learn the equality of two types from information contained in terms. Typically, only singleton types should inhabit this class.

Methods

testEquality :: f a -> f b -> Maybe (a :~: b) #

Conditionally prove the equality of a and b.

Instances

TestEquality BoolRepr Source #
Instance details Defined in Data.Parameterized.BoolRepr Methods testEquality :: BoolRepr a -> BoolRepr b -> Maybe (a :~: b) #
TestEquality NatRepr Source #
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods testEquality :: NatRepr a -> NatRepr b -> Maybe (a :~: b) #
TestEquality SymbolRepr Source #
Instance details Defined in Data.Parameterized.SymbolRepr Methods testEquality :: SymbolRepr a -> SymbolRepr b -> Maybe (a :~: b) #
TestEquality PeanoRepr Source #
Instance details Defined in Data.Parameterized.Peano Methods testEquality :: PeanoRepr a -> PeanoRepr b -> Maybe (a :~: b) #
TestEquality (Nonce :: k -> Type) Source #
Instance details Defined in Data.Parameterized.Nonce.Unsafe Methods testEquality :: Nonce a -> Nonce b -> Maybe (a :~: b) #
TestEquality (TypeRep :: k -> Type)
Instance details Defined in Data.Typeable.Internal Methods testEquality :: TypeRep a -> TypeRep b -> Maybe (a :~: b) #
TestEquality (Nonce s :: k -> Type) Source #
Instance details Defined in Data.Parameterized.Nonce Methods testEquality :: Nonce s a -> Nonce s b -> Maybe (a :~: b) #
TestEquality ((:~:) a :: k -> Type)	Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods testEquality :: (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) #
TestEquality (Index l :: k -> Type) Source #
Instance details Defined in Data.Parameterized.List Methods testEquality :: Index l a -> Index l b -> Maybe (a :~: b) #
TestEquality (Index ctx :: k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods testEquality :: Index ctx a -> Index ctx b -> Maybe (a :~: b) #
TestEquality (Index ctx :: k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Safe Methods testEquality :: Index ctx a -> Index ctx b -> Maybe (a :~: b) #
TestEquality ((:~~:) a :: k -> Type)	Since: base-4.10.0.0
Instance details Defined in Data.Type.Equality Methods testEquality :: (a :~~: a0) -> (a :~~: b) -> Maybe (a0 :~: b) #
TestEquality f => TestEquality (Compose f g :: k1 -> Type) Source #
Instance details Defined in Data.Parameterized.Compose Methods testEquality :: Compose f g a -> Compose f g b -> Maybe (a :~: b) #
TestEquality f => TestEquality (List f :: [k] -> Type) Source #
Instance details Defined in Data.Parameterized.List Methods testEquality :: List f a -> List f b -> Maybe (a :~: b) #
TestEquality f => TestEquality (Assignment f :: Ctx k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods testEquality :: Assignment f a -> Assignment f b -> Maybe (a :~: b) #
TestEquality f => TestEquality (Assignment f :: Ctx k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Safe Methods testEquality :: Assignment f a -> Assignment f b -> Maybe (a :~: b) #

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

Instances

Category ((:~:) :: k -> k -> Type)	Since: base-4.7.0.0
Instance details Defined in Control.Category Methods id :: a :~: a # (.) :: (b :~: c) -> (a :~: b) -> a :~: c #
TestEquality ((:~:) a :: k -> Type)	Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods testEquality :: (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) #
NFData2 ((:~:) :: Type -> Type -> Type)	Since: deepseq-1.4.3.0
Instance details Defined in Control.DeepSeq Methods liftRnf2 :: (a -> ()) -> (b -> ()) -> (a :~: b) -> () #
NFData1 ((:~:) a)	Since: deepseq-1.4.3.0
Instance details Defined in Control.DeepSeq Methods liftRnf :: (a0 -> ()) -> (a :~: a0) -> () #
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)	Since: base-4.7.0.0
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)	Since: base-4.7.0.0
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)	Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods showsPrec :: Int -> (a :~: b) -> ShowS # show :: (a :~: b) -> String # showList :: [a :~: b] -> ShowS #
NFData (a :~: b)	Since: deepseq-1.4.3.0
Instance details Defined in Control.DeepSeq Methods rnf :: (a :~: b) -> () #

data Some (f :: k -> *) Source #

Instances

OrdC (Some :: (k -> Type) -> Type) Source #
Instance details Defined in Data.Parameterized.ClassesC Methods compareC :: (forall (x :: k0) (y :: k0). f x -> g y -> OrderingF x y) -> Some f -> Some g -> Ordering Source #
TestEqualityC (Some :: (k -> Type) -> Type) Source #	This instance demonstrates where the above class is useful: namely, in types with existential quantification.
Instance details Defined in Data.Parameterized.ClassesC Methods testEqualityC :: (forall (x :: k0) (y :: k0). f x -> f y -> Maybe (x :~: y)) -> Some f -> Some f -> Bool Source #
TestEquality f => Eq (Some f) Source #
Instance details Defined in Data.Parameterized.Some Methods (==) :: Some f -> Some f -> Bool # (/=) :: Some f -> Some f -> Bool #
OrdF f => Ord (Some f) Source #
Instance details Defined in Data.Parameterized.Some Methods compare :: Some f -> Some f -> Ordering # (<) :: Some f -> Some f -> Bool # (<=) :: Some f -> Some f -> Bool # (>) :: Some f -> Some f -> Bool # (>=) :: Some f -> Some f -> Bool # max :: Some f -> Some f -> Some f # min :: Some f -> Some f -> Some f #
ShowF f => Show (Some f) Source #
Instance details Defined in Data.Parameterized.Some Methods showsPrec :: Int -> Some f -> ShowS # show :: Some f -> String # showList :: [Some f] -> ShowS #
HashableF f => Hashable (Some f) Source #
Instance details Defined in Data.Parameterized.Some Methods hashWithSalt :: Int -> Some f -> Int # hash :: Some f -> Int #