| 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.
The result should be Just Refl if and only if the types applied to f are
equal:
testEquality (x :: f a) (y :: f b) = Just Refl ⟺ a = b
Typically, only singleton types should inhabit this class. In that case type argument equality coincides with term equality:
testEquality (x :: f a) (y :: f b) = Just Refl ⟺ a = b ⟺ x = y
isJust (testEquality x y) = x == y
Singleton types are not required, however, and so the latter two would-be laws are not in fact valid in general.
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) | |
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 | |