| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Data.Parameterized.BoolRepr
Contents
Synopsis
- module Data.Type.Bool
- data BoolRepr (b :: Bool) where
- 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 :: forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b)
- data (a :: k) :~: (b :: k) where
- data Some (f :: k -> Type)
Documentation
module Data.Type.Bool
data BoolRepr (b :: Bool) where Source #
A Boolean flag
Instances
| TestEquality BoolRepr Source # | |
Defined in Data.Parameterized.BoolRepr | |
| HashableF BoolRepr Source # | |
| OrdF BoolRepr Source # | |
Defined in Data.Parameterized.BoolRepr Methods compareF :: forall (x :: k) (y :: k). BoolRepr x -> BoolRepr y -> OrderingF x y Source # leqF :: forall (x :: k) (y :: k). BoolRepr x -> BoolRepr y -> Bool Source # ltF :: forall (x :: k) (y :: k). BoolRepr x -> BoolRepr y -> Bool Source # geqF :: forall (x :: k) (y :: k). BoolRepr x -> BoolRepr y -> Bool Source # gtF :: forall (x :: k) (y :: k). BoolRepr x -> BoolRepr y -> Bool Source # | |
| ShowF BoolRepr Source # | |
| DecidableEq BoolRepr Source # | |
| IsRepr BoolRepr Source # | |
| KnownRepr BoolRepr 'False Source # | |
| KnownRepr BoolRepr 'True Source # | |
| Show (BoolRepr m) Source # | |
| Eq (BoolRepr m) Source # | |
| Hashable (BoolRepr n) Source # | |
Defined in Data.Parameterized.BoolRepr | |
| PolyEq (BoolRepr m) (BoolRepr n) 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 :: forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b) #
Conditionally prove the equality of a and b.
Instances
data (a :: k) :~: (b :: 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: base-4.7.0.0
Instances
| Category ((:~:) :: k -> k -> Type) | Since: base-4.7.0.0 |
| TestEquality ((:~:) a :: k -> Type) | Since: base-4.7.0.0 |
Defined in Data.Type.Equality | |
| NFData2 ((:~:) :: Type -> Type -> Type) | Since: deepseq-1.4.3.0 |
Defined in Control.DeepSeq | |
| NFData1 ((:~:) a) | Since: deepseq-1.4.3.0 |
Defined in Control.DeepSeq | |
| (a ~ b, Data a) => Data (a :~: b) | Since: base-4.7.0.0 |
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 :: forall r r'. (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) # | |
| a ~ b => Bounded (a :~: b) | Since: base-4.7.0.0 |
| a ~ b => Enum (a :~: b) | Since: base-4.7.0.0 |
Defined in Data.Type.Equality Methods succ :: (a :~: b) -> a :~: b # pred :: (a :~: b) -> 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] # | |
| a ~ b => Read (a :~: b) | Since: base-4.7.0.0 |
| Show (a :~: b) | Since: base-4.7.0.0 |
| NFData (a :~: b) | Since: deepseq-1.4.3.0 |
Defined in Control.DeepSeq | |
| Eq (a :~: b) | Since: base-4.7.0.0 |
| Ord (a :~: b) | Since: base-4.7.0.0 |
Defined in Data.Type.Equality | |
| HasDict (a ~ b) (a :~: b) | |
Defined in Data.Constraint | |
data Some (f :: k -> Type) Source #
Instances
| OrdC (Some :: (k -> Type) -> Type) Source # | |
| TestEqualityC (Some :: (k -> Type) -> Type) Source # | This instance demonstrates where the above class is useful: namely, in types with existential quantification. |
Defined in Data.Parameterized.ClassesC | |
| FoldableF (Some :: (k -> Type) -> Type) Source # | |
Defined in Data.Parameterized.Some Methods foldMapF :: Monoid m => (forall (s :: k0). e s -> m) -> Some e -> m Source # foldrF :: (forall (s :: k0). e s -> b -> b) -> b -> Some e -> b Source # foldlF :: (forall (s :: k0). b -> e s -> b) -> b -> Some e -> b Source # foldrF' :: (forall (s :: k0). e s -> b -> b) -> b -> Some e -> b Source # foldlF' :: (forall (s :: k0). b -> e s -> b) -> b -> Some e -> b Source # toListF :: (forall (tp :: k0). f tp -> a) -> Some f -> [a] Source # | |
| FunctorF (Some :: (k -> Type) -> Type) Source # | |
| TraversableF (Some :: (k -> Type) -> Type) Source # | |
Defined in Data.Parameterized.Some | |
| ShowF f => Show (Some f) Source # | |
| TestEquality f => Eq (Some f) Source # | |
| OrdF f => Ord (Some f) Source # | |
| (HashableF f, TestEquality f) => Hashable (Some f) Source # | |
Defined in Data.Parameterized.Some | |