parameterized-utils-2.1.11.0: Classes and data structures for working with data-kind indexed types

Safe Haskell | Safe-Inferred
Language | Haskell2010

Data.Parameterized.BoolRepr

Contents

- Re-exports

Synopsis

- module Data.Type.Bool
- data BoolRepr (b :: Bool) where
  - FalseRepr :: BoolRepr 'False
  - TrueRepr :: BoolRepr 'True
- ifRepr :: forall (a :: Bool) (b :: Bool) (c :: Bool). BoolRepr a -> BoolRepr b -> BoolRepr c -> BoolRepr (If a b c)
- notRepr :: forall (b :: Bool). BoolRepr b -> BoolRepr (Not b)
- (%&&) :: forall (a :: Bool) (b :: Bool). BoolRepr a -> BoolRepr b -> BoolRepr (a && b)
- (%||) :: forall (a :: Bool) (b :: Bool). 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
  - Refl :: forall {k} (a :: k). a :~: a
- data Some (f :: k -> Type)

# Documentation

module Data.Type.Bool

data BoolRepr (b :: Bool) where Source #

A Boolean flag

Constructors

FalseRepr :: BoolRepr 'False |
TrueRepr :: BoolRepr 'True |

#### Instances

Instances details

TestEquality BoolRepr Source # |
Instance details Defined in Data.Parameterized.BoolRepr Methods testEquality :: forall (a :: Bool) (b :: Bool). BoolRepr a -> BoolRepr b -> Maybe (a :~: b) Source #
EqF BoolRepr Source # |
Instance details Defined in Data.Parameterized.BoolRepr Methods eqF :: forall (a :: Bool). BoolRepr a -> BoolRepr a -> Bool Source #
HashableF BoolRepr Source # |
Instance details Defined in Data.Parameterized.BoolRepr Methods hashWithSaltF :: forall (tp :: Bool). Int -> BoolRepr tp -> Int Source # hashF :: forall (tp :: Bool). BoolRepr tp -> Int Source #
OrdF BoolRepr Source # |

Instance details

Defined in Data.Parameterized.BoolRepr

Methods

compareF :: forall (x :: Bool) (y :: Bool). BoolRepr x -> BoolRepr y -> OrderingF x y Source #

leqF :: forall (x :: Bool) (y :: Bool). BoolRepr x -> BoolRepr y -> Bool Source #

ltF :: forall (x :: Bool) (y :: Bool). BoolRepr x -> BoolRepr y -> Bool Source #

geqF :: forall (x :: Bool) (y :: Bool). BoolRepr x -> BoolRepr y -> Bool Source #

gtF :: forall (x :: Bool) (y :: Bool). BoolRepr x -> BoolRepr y -> Bool Source #

ShowF BoolRepr Source # |
Instance details Defined in Data.Parameterized.BoolRepr Methods withShow :: forall p q (tp :: Bool) a. p BoolRepr -> q tp -> (Show (BoolRepr tp) => a) -> a Source # showF :: forall (tp :: Bool). BoolRepr tp -> String Source # showsPrecF :: forall (tp :: Bool). Int -> BoolRepr tp -> String -> String Source #
DecidableEq BoolRepr Source # |
Instance details Defined in Data.Parameterized.BoolRepr Methods decEq :: forall (a :: Bool) (b :: Bool). BoolRepr a -> BoolRepr b -> Either (a :~: b) ((a :~: b) -> Void) Source #
IsRepr BoolRepr Source # |
Instance details Defined in Data.Parameterized.WithRepr Methods withRepr :: forall (a :: Bool) r. 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 #
Show (BoolRepr m) Source # |
Instance details Defined in Data.Parameterized.BoolRepr Methods showsPrec :: Int -> BoolRepr m -> ShowS Source # show :: BoolRepr m -> String Source # showList :: [BoolRepr m] -> ShowS Source #
Eq (BoolRepr m) Source # |
Instance details Defined in Data.Parameterized.BoolRepr Methods (==) :: BoolRepr m -> BoolRepr m -> Bool Source # (/=) :: BoolRepr m -> BoolRepr m -> Bool Source #
Hashable (BoolRepr n) Source # |
Instance details Defined in Data.Parameterized.BoolRepr Methods hashWithSalt :: Int -> BoolRepr n -> Int Source # hash :: BoolRepr n -> Int Source #
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 :: forall (a :: Bool) (b :: Bool) (c :: Bool). BoolRepr a -> BoolRepr b -> BoolRepr c -> BoolRepr (If a b c) Source #

conditional

notRepr :: forall (b :: Bool). BoolRepr b -> BoolRepr (Not b) Source #

negation

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

Conjunction

(%||) :: forall (a :: Bool) (b :: Bool). 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 Source #

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) Source #

Conditionally prove the equality of `a` and `b`.

#### Instances

Instances details

TestEquality SNat | Since: base-4.18.0.0
Instance details Defined in GHC.Internal.TypeNats Methods testEquality :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b) Source #
TestEquality NatRepr Source # |
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods testEquality :: forall (a :: Nat) (b :: Nat). NatRepr a -> NatRepr b -> Maybe (a :~: b) Source #
TestEquality PeanoRepr Source # |
Instance details Defined in Data.Parameterized.Peano Methods testEquality :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> Maybe (a :~: b) Source #
TestEquality BoolRepr Source # |
Instance details Defined in Data.Parameterized.BoolRepr Methods testEquality :: forall (a :: Bool) (b :: Bool). BoolRepr a -> BoolRepr b -> Maybe (a :~: b) Source #
TestEquality SChar | Since: base-4.18.0.0
Instance details Defined in GHC.Internal.TypeLits Methods testEquality :: forall (a :: Char) (b :: Char). SChar a -> SChar b -> Maybe (a :~: b) Source #
TestEquality SSymbol | Since: base-4.18.0.0
Instance details Defined in GHC.Internal.TypeLits Methods testEquality :: forall (a :: Symbol) (b :: Symbol). SSymbol a -> SSymbol b -> Maybe (a :~: b) Source #
TestEquality SymbolRepr Source # |
Instance details Defined in Data.Parameterized.SymbolRepr Methods testEquality :: forall (a :: Symbol) (b :: Symbol). SymbolRepr a -> SymbolRepr b -> Maybe (a :~: b) Source #
TestEquality (TypeRep :: k -> Type) |
Instance details Defined in GHC.Internal.Data.Typeable.Internal Methods testEquality :: forall (a :: k) (b :: k). TypeRep a -> TypeRep b -> Maybe (a :~: b) Source #
TestEquality (Nonce :: k -> Type) Source # |
Instance details Defined in Data.Parameterized.Nonce.Unsafe Methods testEquality :: forall (a :: k) (b :: k). Nonce a -> Nonce b -> Maybe (a :~: b) Source #
TestEquality ((:~:) a :: k -> Type) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods testEquality :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) Source #
TestEquality (Index ctx :: k -> Type) Source # |
Instance details Defined in Data.Parameterized.Context.Unsafe Methods testEquality :: forall (a :: k) (b :: k). Index ctx a -> Index ctx b -> Maybe (a :~: b) Source #
TestEquality (Index l :: k -> Type) Source # |
Instance details Defined in Data.Parameterized.List Methods testEquality :: forall (a :: k) (b :: k). Index l a -> Index l b -> Maybe (a :~: b) Source #
TestEquality (Nonce s :: k -> Type) Source # |
Instance details Defined in Data.Parameterized.Nonce Methods testEquality :: forall (a :: k) (b :: k). Nonce s a -> Nonce s b -> Maybe (a :~: b) Source #
TestEquality ((:~~:) a :: k -> Type) | Since: base-4.10.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods testEquality :: forall (a0 :: k) (b :: k). (a :~~: a0) -> (a :~~: b) -> Maybe (a0 :~: b) Source #
TestEquality f => TestEquality (Compose f g :: k2 -> Type) | The deduction (via generativity) that if `g x :~: g y` then `x :~: y`. Since: base-4.14.0.0
Instance details Defined in Data.Functor.Compose Methods testEquality :: forall (a :: k2) (b :: k2). Compose f g a -> Compose f g b -> Maybe (a :~: b) Source #
TestEquality f => TestEquality (Assignment f :: Ctx k -> Type) Source # |
Instance details Defined in Data.Parameterized.Context.Unsafe Methods testEquality :: forall (a :: Ctx k) (b :: Ctx k). Assignment f a -> Assignment f b -> Maybe (a :~: b) Source #
TestEquality f => TestEquality (List f :: [k] -> Type) Source # |
Instance details Defined in Data.Parameterized.List Methods testEquality :: forall (a :: [k]) (b :: [k]). List f a -> List f b -> Maybe (a :~: b) Source #
(TestEquality f, TestEquality g) => TestEquality (PairRepr f g :: (k1, k2) -> Type) Source # |
Instance details Defined in Data.Parameterized.DataKind Methods testEquality :: forall (a :: (k1, k2)) (b :: (k1, k2)). PairRepr f g a -> PairRepr f g b -> Maybe (a :~: b) Source #

data (a :: k) :~: (b :: k) where infix 4 Source #

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). a :~: a |

#### Instances

Instances details

Category ((:~:) :: k -> k -> Type) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Control.Category Methods id :: forall (a :: k). a :~: a Source # (.) :: forall (b :: k) (c :: k) (a :: k). (b :~: c) -> (a :~: b) -> a :~: c Source #
TestEquality ((:~:) a :: k -> Type) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods testEquality :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) Source #
NFData2 ((:~:) :: Type -> Type -> Type) | Since: deepseq-1.4.3.0
Instance details Defined in Control.DeepSeq Methods liftRnf2 :: (a -> ()) -> (b -> ()) -> (a :~: b) -> () Source #
NFData1 ((:~:) a) | Since: deepseq-1.4.3.0
Instance details Defined in Control.DeepSeq Methods liftRnf :: (a0 -> ()) -> (a :~: a0) -> () Source #
NFData (a :~: b) | Since: deepseq-1.4.3.0
Instance details Defined in Control.DeepSeq Methods rnf :: (a :~: b) -> () Source #
(a ~ b, Data a) => Data (a :~: b) | Since: base-4.7.0.0

Instance details

Defined in GHC.Internal.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) Source #

gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (a :~: b) Source #

toConstr :: (a :~: b) -> Constr Source #

dataTypeOf :: (a :~: b) -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (a :~: b)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (a :~: b)) Source #

gmapT :: (forall b0. Data b0 => b0 -> b0) -> (a :~: b) -> a :~: b Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> (a :~: b) -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> (a :~: b) -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) Source #

a ~ b => Bounded (a :~: b) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods minBound :: a :~: b Source # maxBound :: a :~: b Source #
a ~ b => Enum (a :~: b) | Since: base-4.7.0.0

Instance details

Defined in GHC.Internal.Data.Type.Equality

Methods

succ :: (a :~: b) -> a :~: b Source #

pred :: (a :~: b) -> a :~: b Source #

toEnum :: Int -> a :~: b Source #

fromEnum :: (a :~: b) -> Int Source #

enumFrom :: (a :~: b) -> [a :~: b] Source #

enumFromThen :: (a :~: b) -> (a :~: b) -> [a :~: b] Source #

enumFromTo :: (a :~: b) -> (a :~: b) -> [a :~: b] Source #

enumFromThenTo :: (a :~: b) -> (a :~: b) -> (a :~: b) -> [a :~: b] Source #

a ~ b => Read (a :~: b) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods readsPrec :: Int -> ReadS (a :~: b) Source # readList :: ReadS [a :~: b] Source # readPrec :: ReadPrec (a :~: b) Source # readListPrec :: ReadPrec [a :~: b] Source #
Show (a :~: b) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods showsPrec :: Int -> (a :~: b) -> ShowS Source # show :: (a :~: b) -> String Source # showList :: [a :~: b] -> ShowS Source #
Eq (a :~: b) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods (==) :: (a :~: b) -> (a :~: b) -> Bool Source # (/=) :: (a :~: b) -> (a :~: b) -> Bool Source #
Ord (a :~: b) | Since: base-4.7.0.0

Instance details

Defined in GHC.Internal.Data.Type.Equality

Methods

compare :: (a :~: b) -> (a :~: b) -> Ordering Source #

(<) :: (a :~: b) -> (a :~: b) -> Bool Source #

(<=) :: (a :~: b) -> (a :~: b) -> Bool Source #

(>) :: (a :~: b) -> (a :~: b) -> Bool Source #

(>=) :: (a :~: b) -> (a :~: b) -> Bool Source #

max :: (a :~: b) -> (a :~: b) -> a :~: b Source #

min :: (a :~: b) -> (a :~: b) -> a :~: b Source #

HasDict (a ~ b) (a :~: b) |
Instance details Defined in Data.Constraint Methods evidence :: (a :~: b) -> Dict (a ~ b) Source #

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

#### Instances

Instances details

OrdC (Some :: (k -> Type) -> Type) Source # |
Instance details Defined in Data.Parameterized.ClassesC Methods compareC :: (forall (x :: k) (y :: k). 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 :: k) (y :: k). f x -> f y -> Maybe (x :~: y)) -> Some f -> Some f -> Bool Source #
FoldableF (Some :: (k -> Type) -> Type) Source # |

Instance details

Defined in Data.Parameterized.Some

Methods

foldMapF :: Monoid m => (forall (s :: k). e s -> m) -> Some e -> m Source #

foldrF :: (forall (s :: k). e s -> b -> b) -> b -> Some e -> b Source #

foldlF :: (forall (s :: k). b -> e s -> b) -> b -> Some e -> b Source #

foldrF' :: (forall (s :: k). e s -> b -> b) -> b -> Some e -> b Source #

foldlF' :: (forall (s :: k). b -> e s -> b) -> b -> Some e -> b Source #

toListF :: (forall (tp :: k). f tp -> a) -> Some f -> [a] Source #

FunctorF (Some :: (k -> Type) -> Type) Source # |
Instance details Defined in Data.Parameterized.Some Methods fmapF :: (forall (x :: k). f x -> g x) -> Some f -> Some g Source #
TraversableF (Some :: (k -> Type) -> Type) Source # |
Instance details Defined in Data.Parameterized.Some Methods traverseF :: Applicative m => (forall (s :: k). e s -> m (f s)) -> Some e -> m (Some f) Source #
ShowF f => Show (Some f) Source # |
Instance details Defined in Data.Parameterized.Some Methods showsPrec :: Int -> Some f -> ShowS Source # show :: Some f -> String Source # showList :: [Some f] -> ShowS Source #
TestEquality f => Eq (Some f) Source # |
Instance details Defined in Data.Parameterized.Some Methods (==) :: Some f -> Some f -> Bool Source # (/=) :: Some f -> Some f -> Bool Source #
OrdF f => Ord (Some f) Source # |
Instance details Defined in Data.Parameterized.Some Methods compare :: Some f -> Some f -> Ordering Source # (<) :: Some f -> Some f -> Bool Source # (<=) :: Some f -> Some f -> Bool Source # (>) :: Some f -> Some f -> Bool Source # (>=) :: Some f -> Some f -> Bool Source # max :: Some f -> Some f -> Some f Source # min :: Some f -> Some f -> Some f Source #
(HashableF f, TestEquality f) => Hashable (Some f) Source # |
Instance details Defined in Data.Parameterized.Some Methods hashWithSalt :: Int -> Some f -> Int Source # hash :: Some f -> Int Source #