Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Exists

Contents

Data Types
Type Classes
Higher Rank Classes
More Type Classes
Sing Type Classes
Functions

Description

Data types and type classes for working with existentially quantified values. When Quantified Class Constraints land in GHC 8.6, the BarForall classes will be considered obsolete. When Dependent Haskell lands, the BarForeach classes will also be obsolete. The benefit that most of the typeclasses in this module provide is that they help populate the instances of Exists and Rec.

Synopsis

data Exists (f :: k -> Type) = forall a. Exists !(f a)
data Exists2 (f :: k -> j -> Type) = forall a b. Exists2 !(f a b)
data Exists3 (f :: k -> j -> l -> Type) = forall a b c. Exists3 !(f a b c)
data Some (f :: k -> Type) = forall a. Some !(Sing a) !(f a)
data DependentPair (f :: k -> Type) (g :: k -> Type) = forall a. DependentPair (f a) (g a)
data WitnessedEquality (a :: k) (b :: k) where
- WitnessedEqualityEqual :: WitnessedEquality a a
- WitnessedEqualityUnequal :: WitnessedEquality a b
data WitnessedOrdering (a :: k) (b :: k) where
- WitnessedOrderingLT :: WitnessedOrdering a b
- WitnessedOrderingEQ :: WitnessedOrdering a a
- WitnessedOrderingGT :: WitnessedOrdering a b
newtype ApplyForall f a = ApplyForall {
- getApplyForall :: f a
}
newtype ApplyForeach f a = ApplyForeach {
- getApplyForeach :: f a
}
newtype ApplyLifted f a = ApplyLifted {
- getApplyLifted :: f a
}
class EqForall f where
- eqForall :: f a -> f a -> Bool
class EqForall f => EqForallPoly f where
- eqForallPoly :: f a -> f b -> WitnessedEquality a b
class EqForeach f where
- eqForeach :: Sing a -> f a -> f a -> Bool
class EqForall f => OrdForall f where
- compareForall :: f a -> f a -> Ordering
class (OrdForall f, EqForallPoly f) => OrdForallPoly f where
- compareForallPoly :: f a -> f b -> WitnessedOrdering a b
class EqForeach f => OrdForeach f where
- compareForeach :: Sing a -> f a -> f a -> Ordering
class ShowForall f where
- showsPrecForall :: Int -> f a -> ShowS
class ShowForeach f where
- showsPrecForeach :: Sing a -> Int -> f a -> ShowS
class ReadExists f where
- readPrecExists :: ReadPrec (Exists f)
class EnumForall f where
- toEnumForall :: Int -> f a
- fromEnumForall :: f a -> Int
class EnumExists f where
- toEnumExists :: Int -> Exists f
- fromEnumExists :: Exists f -> Int
class BoundedExists f where
- minBoundExists :: Exists f
- maxBoundExists :: Exists f
class SemigroupForall f where
- appendForall :: f a -> f a -> f a
class SemigroupForeach f where
- appendForeach :: Sing a -> f a -> f a -> f a
class SemigroupForall f => MonoidForall f where
- emptyForall :: f a
class SemigroupForeach f => MonoidForeach f where
- emptyForeach :: Sing a -> f a
class HashableForall f where
- hashWithSaltForall :: Int -> f a -> Int
class HashableForeach f where
- hashWithSaltForeach :: Sing a -> Int -> f a -> Int
class PathPieceExists f where
- fromPathPieceForall :: Text -> Maybe (Exists f)
- toPathPieceForall :: Exists f -> Text
class StorableForeach (f :: k -> Type) where
- peekForeach :: Sing a -> Ptr (f a) -> IO (f a)
- pokeForeach :: Sing a -> Ptr (f a) -> f a -> IO ()
- sizeOfForeach :: forall (a :: k). Proxy f -> Sing a -> Int
class StorableForall (f :: k -> Type) where
- peekForall :: Ptr (f a) -> IO (f a)
- pokeForall :: Ptr (f a) -> f a -> IO ()
- sizeOfForall :: Proxy f -> Int
class PrimForall (f :: k -> Type) where
- sizeOfForall# :: Proxy# f -> Int#
- alignmentForall# :: Proxy# f -> Int#
- indexByteArrayForall# :: ByteArray# -> Int# -> f a
- readByteArrayForall# :: MutableByteArray# s -> Int# -> State# s -> (# State# s, f a #)
- writeByteArrayForall# :: MutableByteArray# s -> Int# -> f a -> State# s -> State# s
- setByteArrayForall# :: MutableByteArray# s -> Int# -> Int# -> f a -> State# s -> State# s
- indexOffAddrForall# :: Addr# -> Int# -> f a
- readOffAddrForall# :: Addr# -> Int# -> State# s -> (# State# s, f a #)
- writeOffAddrForall# :: Addr# -> Int# -> f a -> State# s -> State# s
- setOffAddrForall# :: Addr# -> Int# -> Int# -> f a -> State# s -> State# s
class BinaryExists (f :: k -> Type) where
- putExists :: Exists f -> Put
- getExists :: Get (Exists f)
class BinaryForeach (f :: k -> Type) where
- putForeach :: Sing a -> f a -> Put
- getForeach :: Sing a -> Get (f a)
class EqForall2 f where
- eqForall2 :: f a b -> f a b -> Bool
class EqForallPoly2 (f :: k -> j -> Type) where
- eqForallPoly2 :: forall (a :: k) (b :: j) (c :: k) (d :: j). f a b -> f c d -> WitnessedEquality '(a, b) '(c, d)
class ShowForall2 f where
- showsPrecForall2 :: Int -> f a b -> ShowS
class ShowForeach2 f where
- showsPrecForeach2 :: Sing a -> Sing b -> Int -> f a b -> ShowS
class BinaryExists2 (f :: k -> j -> Type) where
- putExists2 :: Exists2 f -> Put
- getExists2 :: Get (Exists2 f)
type family Sing = (r :: k -> Type) | r -> k
data SingList :: forall (k :: Type). [k] -> Type where
- SingListNil :: SingList '[]
- SingListCons :: Sing r -> SingList rs -> SingList (r ': rs)
data SingMaybe :: Maybe k -> Type where
- SingMaybeJust :: Sing a -> SingMaybe ('Just a)
- SingMaybeNothing :: SingMaybe 'Nothing
class Reify a where
- reify :: Sing a
class Unreify k where
- unreify :: forall (a :: k) b. Sing a -> (Reify a => b) -> b
class EqSing k where
- eqSing :: forall (a :: k) (b :: k). Sing a -> Sing b -> Maybe (a :~: b)
class EqSing k => OrdSing k where
- compareSing :: forall (a :: k) (b :: k). Sing a -> Sing b -> WitnessedOrdering a b
class ShowSing k where
- showsPrecSing :: forall (a :: k). Int -> Sing a -> ShowS
class ToSing (f :: k -> Type) where
- toSing :: f a -> Sing a
class SingKind k where
- demoteSing :: Sing (a :: k) -> k
- promoteSing :: k -> Exists (Sing :: k -> Type)
showsForall :: ShowForall f => f a -> ShowS
showsForeach :: ShowForeach f => Sing a -> f a -> ShowS
showForall :: ShowForall f => f a -> String
showListForall :: ShowForall f => [f a] -> ShowS
showListForeach :: ShowForeach f => Sing a -> [f a] -> ShowS
showsForall2 :: ShowForall2 f => f a b -> ShowS
showForall2 :: ShowForall2 f => f a b -> String
defaultEqForallPoly :: (TestEquality f, EqForall f) => f a -> f b -> WitnessedEquality a b
defaultCompareForallPoly :: (TestEquality f, OrdForall f) => f a -> f b -> Ordering
weakenEquality :: WitnessedEquality a b -> Bool
weakenOrdering :: WitnessedOrdering a b -> Ordering
strengthenEquality :: Bool -> WitnessedEquality a a
strengthenOrdering :: Ordering -> WitnessedOrdering a a
strengthenUnequalOrdering :: Ordering -> WitnessedOrdering a b
unreifyList :: forall (k :: Type) (as :: [k]) (b :: Type). Unreify k => SingList as -> (Reify as => b) -> b

Data Types

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

Hide a type parameter.

Constructors

forall a. Exists !(f a)

Instances

Instances details

BoundedExists f => Bounded (Exists f) Source #
Instance details Defined in Data.Exists Methods minBound :: Exists f # maxBound :: Exists f #
EnumExists f => Enum (Exists f) Source #
Instance details Defined in Data.Exists Methods succ :: Exists f -> Exists f # pred :: Exists f -> Exists f # toEnum :: Int -> Exists f # fromEnum :: Exists f -> Int # enumFrom :: Exists f -> [Exists f] # enumFromThen :: Exists f -> Exists f -> [Exists f] # enumFromTo :: Exists f -> Exists f -> [Exists f] # enumFromThenTo :: Exists f -> Exists f -> Exists f -> [Exists f] #
ReadExists f => Read (Exists f) Source #
Instance details Defined in Data.Exists Methods readsPrec :: Int -> ReadS (Exists f) # readList :: ReadS [Exists f] # readPrec :: ReadPrec (Exists f) # readListPrec :: ReadPrec [Exists f] #
ShowForall f => Show (Exists f) Source #
Instance details Defined in Data.Exists Methods showsPrec :: Int -> Exists f -> ShowS # show :: Exists f -> String # showList :: [Exists f] -> ShowS #
BinaryExists f => Binary (Exists f) Source #
Instance details Defined in Data.Exists Methods put :: Exists f -> Put # get :: Get (Exists f) # putList :: [Exists f] -> Put #
EqForallPoly f => Eq (Exists f) Source #
Instance details Defined in Data.Exists Methods (==) :: Exists f -> Exists f -> Bool # (/=) :: Exists f -> Exists f -> Bool #
OrdForallPoly f => Ord (Exists f) Source #
Instance details Defined in Data.Exists Methods compare :: Exists f -> Exists f -> Ordering # (<) :: Exists f -> Exists f -> Bool # (<=) :: Exists f -> Exists f -> Bool # (>) :: Exists f -> Exists f -> Bool # (>=) :: Exists f -> Exists f -> Bool # max :: Exists f -> Exists f -> Exists f # min :: Exists f -> Exists f -> Exists f #
(EqForallPoly f, HashableForall f) => Hashable (Exists f) Source #
Instance details Defined in Data.Exists Methods hashWithSalt :: Int -> Exists f -> Int # hash :: Exists f -> Int #
PathPieceExists f => PathPiece (Exists f) Source #
Instance details Defined in Data.Exists Methods fromPathPiece :: Text -> Maybe (Exists f) # toPathPiece :: Exists f -> Text #

data Exists2 (f :: k -> j -> Type) Source #

Hide two type parameters.

Constructors

forall a b. Exists2 !(f a b)

Instances

Instances details

ShowForall2 f => Show (Exists2 f) Source #
Instance details Defined in Data.Exists Methods showsPrec :: Int -> Exists2 f -> ShowS # show :: Exists2 f -> String # showList :: [Exists2 f] -> ShowS #
BinaryExists2 f => Binary (Exists2 f) Source #
Instance details Defined in Data.Exists Methods put :: Exists2 f -> Put # get :: Get (Exists2 f) # putList :: [Exists2 f] -> Put #
EqForallPoly2 f => Eq (Exists2 f) Source #
Instance details Defined in Data.Exists Methods (==) :: Exists2 f -> Exists2 f -> Bool # (/=) :: Exists2 f -> Exists2 f -> Bool #

data Exists3 (f :: k -> j -> l -> Type) Source #

Hide three type parameters.

Constructors

forall a b c. Exists3 !(f a b c)

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

A dependent pair in which the first element is a singleton.

Constructors

forall a. Some !(Sing a) !(f a)

Instances

Instances details

(ShowForeach f, ShowSing k) => Show (Some f) Source #
Instance details Defined in Data.Exists Methods showsPrec :: Int -> Some f -> ShowS # show :: Some f -> String # showList :: [Some f] -> ShowS #
(EqForeach f, EqSing k) => Eq (Some f) Source #
Instance details Defined in Data.Exists Methods (==) :: Some f -> Some f -> Bool # (/=) :: Some f -> Some f -> Bool #
(OrdForeach f, OrdSing k) => Ord (Some f) Source #
Instance details Defined in Data.Exists 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 #

data DependentPair (f :: k -> Type) (g :: k -> Type) Source #

A pair in which the type of the second element can only be discovered by looking at the first element. The type instance does not enforce this, but all of its typeclass instances make this assumption.

Constructors

forall a. DependentPair (f a) (g a)

Instances

Instances details

(ShowForall f, ToSing f, ShowForeach g) => Show (DependentPair f g) Source #
Instance details Defined in Data.Exists Methods showsPrec :: Int -> DependentPair f g -> ShowS # show :: DependentPair f g -> String # showList :: [DependentPair f g] -> ShowS #
(EqForallPoly f, ToSing f, EqForeach g) => Eq (DependentPair f g) Source #
Instance details Defined in Data.Exists Methods (==) :: DependentPair f g -> DependentPair f g -> Bool # (/=) :: DependentPair f g -> DependentPair f g -> Bool #
(OrdForallPoly f, ToSing f, OrdForeach g) => Ord (DependentPair f g) Source #
Instance details Defined in Data.Exists Methods compare :: DependentPair f g -> DependentPair f g -> Ordering # (<) :: DependentPair f g -> DependentPair f g -> Bool # (<=) :: DependentPair f g -> DependentPair f g -> Bool # (>) :: DependentPair f g -> DependentPair f g -> Bool # (>=) :: DependentPair f g -> DependentPair f g -> Bool # max :: DependentPair f g -> DependentPair f g -> DependentPair f g # min :: DependentPair f g -> DependentPair f g -> DependentPair f g #

data WitnessedEquality (a :: k) (b :: k) where Source #

Constructors

WitnessedEqualityEqual :: WitnessedEquality a a
WitnessedEqualityUnequal :: WitnessedEquality a b

data WitnessedOrdering (a :: k) (b :: k) where Source #

Constructors

WitnessedOrderingLT :: WitnessedOrdering a b
WitnessedOrderingEQ :: WitnessedOrdering a a
WitnessedOrderingGT :: WitnessedOrdering a b

newtype ApplyForall f a Source #

Constructors

ApplyForall
Fields getApplyForall :: f a

Instances

Instances details

MonoidForall f => MonoidForall (ApplyForall f :: k -> Type) Source #
Instance details Defined in Data.Exists Methods emptyForall :: forall (a :: k0). ApplyForall f a Source #
SemigroupForall f => SemigroupForall (ApplyForall f :: k -> Type) Source #
Instance details Defined in Data.Exists Methods appendForall :: forall (a :: k0). ApplyForall f a -> ApplyForall f a -> ApplyForall f a Source #
MonoidForall f => Monoid (ApplyForall f a) Source #
Instance details Defined in Data.Exists Methods mempty :: ApplyForall f a # mappend :: ApplyForall f a -> ApplyForall f a -> ApplyForall f a # mconcat :: [ApplyForall f a] -> ApplyForall f a #
SemigroupForall f => Semigroup (ApplyForall f a) Source #
Instance details Defined in Data.Exists Methods (<>) :: ApplyForall f a -> ApplyForall f a -> ApplyForall f a # sconcat :: NonEmpty (ApplyForall f a) -> ApplyForall f a # stimes :: Integral b => b -> ApplyForall f a -> ApplyForall f a #
ShowForall f => Show (ApplyForall f a) Source #
Instance details Defined in Data.Exists Methods showsPrec :: Int -> ApplyForall f a -> ShowS # show :: ApplyForall f a -> String # showList :: [ApplyForall f a] -> ShowS #

newtype ApplyForeach f a Source #

This is useful for recovering an instance of a typeclass when we have the pi-quantified variant and a singleton in scope.

Constructors

ApplyForeach
Fields getApplyForeach :: f a

Instances

Instances details

EqForeach f => EqForeach (ApplyForeach f :: k -> Type) Source #
Instance details Defined in Data.Exists Methods eqForeach :: forall (a :: k0). Sing a -> ApplyForeach f a -> ApplyForeach f a -> Bool Source #
MonoidForeach f => MonoidForeach (ApplyForeach f :: k -> Type) Source #
Instance details Defined in Data.Exists Methods emptyForeach :: forall (a :: k0). Sing a -> ApplyForeach f a Source #
OrdForeach f => OrdForeach (ApplyForeach f :: k -> Type) Source #
Instance details Defined in Data.Exists Methods compareForeach :: forall (a :: k0). Sing a -> ApplyForeach f a -> ApplyForeach f a -> Ordering Source #
SemigroupForeach f => SemigroupForeach (ApplyForeach f :: k -> Type) Source #
Instance details Defined in Data.Exists Methods appendForeach :: forall (a :: k0). Sing a -> ApplyForeach f a -> ApplyForeach f a -> ApplyForeach f a Source #
(MonoidForeach f, Reify a) => Monoid (ApplyForeach f a) Source #
Instance details Defined in Data.Exists Methods mempty :: ApplyForeach f a # mappend :: ApplyForeach f a -> ApplyForeach f a -> ApplyForeach f a # mconcat :: [ApplyForeach f a] -> ApplyForeach f a #
(SemigroupForeach f, Reify a) => Semigroup (ApplyForeach f a) Source #
Instance details Defined in Data.Exists Methods (<>) :: ApplyForeach f a -> ApplyForeach f a -> ApplyForeach f a # sconcat :: NonEmpty (ApplyForeach f a) -> ApplyForeach f a # stimes :: Integral b => b -> ApplyForeach f a -> ApplyForeach f a #
(ShowForeach f, Reify a) => Show (ApplyForeach f a) Source #
Instance details Defined in Data.Exists Methods showsPrec :: Int -> ApplyForeach f a -> ShowS # show :: ApplyForeach f a -> String # showList :: [ApplyForeach f a] -> ShowS #
(EqForeach f, Reify a) => Eq (ApplyForeach f a) Source #
Instance details Defined in Data.Exists Methods (==) :: ApplyForeach f a -> ApplyForeach f a -> Bool # (/=) :: ApplyForeach f a -> ApplyForeach f a -> Bool #
(OrdForeach f, Reify a) => Ord (ApplyForeach f a) Source #
Instance details Defined in Data.Exists Methods compare :: ApplyForeach f a -> ApplyForeach f a -> Ordering # (<) :: ApplyForeach f a -> ApplyForeach f a -> Bool # (<=) :: ApplyForeach f a -> ApplyForeach f a -> Bool # (>) :: ApplyForeach f a -> ApplyForeach f a -> Bool # (>=) :: ApplyForeach f a -> ApplyForeach f a -> Bool # max :: ApplyForeach f a -> ApplyForeach f a -> ApplyForeach f a # min :: ApplyForeach f a -> ApplyForeach f a -> ApplyForeach f a #

newtype ApplyLifted f a Source #

Constructors

ApplyLifted
Fields getApplyLifted :: f a

Instances

Instances details

Eq1 f => Eq1 (ApplyLifted f) Source #
Instance details Defined in Data.Exists Methods liftEq :: (a -> b -> Bool) -> ApplyLifted f a -> ApplyLifted f b -> Bool #
Ord1 f => Ord1 (ApplyLifted f) Source #
Instance details Defined in Data.Exists Methods liftCompare :: (a -> b -> Ordering) -> ApplyLifted f a -> ApplyLifted f b -> Ordering #
Monoid1 f => Monoid1 (ApplyLifted f) Source #
Instance details Defined in Data.Exists Methods liftEmpty :: a -> ApplyLifted f a Source #
Semigroup1 f => Semigroup1 (ApplyLifted f) Source #
Instance details Defined in Data.Exists Methods liftAppend :: (a -> a -> a) -> ApplyLifted f a -> ApplyLifted f a -> ApplyLifted f a Source #
(Monoid1 f, Monoid a) => Monoid (ApplyLifted f a) Source #
Instance details Defined in Data.Exists Methods mempty :: ApplyLifted f a # mappend :: ApplyLifted f a -> ApplyLifted f a -> ApplyLifted f a # mconcat :: [ApplyLifted f a] -> ApplyLifted f a #
(Semigroup1 f, Semigroup a) => Semigroup (ApplyLifted f a) Source #
Instance details Defined in Data.Exists Methods (<>) :: ApplyLifted f a -> ApplyLifted f a -> ApplyLifted f a # sconcat :: NonEmpty (ApplyLifted f a) -> ApplyLifted f a # stimes :: Integral b => b -> ApplyLifted f a -> ApplyLifted f a #
(Eq1 f, Eq a) => Eq (ApplyLifted f a) Source #
Instance details Defined in Data.Exists Methods (==) :: ApplyLifted f a -> ApplyLifted f a -> Bool # (/=) :: ApplyLifted f a -> ApplyLifted f a -> Bool #
(Ord1 f, Ord a) => Ord (ApplyLifted f a) Source #
Instance details Defined in Data.Exists Methods compare :: ApplyLifted f a -> ApplyLifted f a -> Ordering # (<) :: ApplyLifted f a -> ApplyLifted f a -> Bool # (<=) :: ApplyLifted f a -> ApplyLifted f a -> Bool # (>) :: ApplyLifted f a -> ApplyLifted f a -> Bool # (>=) :: ApplyLifted f a -> ApplyLifted f a -> Bool # max :: ApplyLifted f a -> ApplyLifted f a -> ApplyLifted f a # min :: ApplyLifted f a -> ApplyLifted f a -> ApplyLifted f a #

Type Classes

class EqForall f where Source #

Methods

eqForall :: f a -> f a -> Bool Source #

Instances

Instances details

EqForall (Proxy :: k -> Type) Source #
Instance details Defined in Data.Exists Methods eqForall :: forall (a :: k0). Proxy a -> Proxy a -> Bool Source #
Eq a => EqForall (Const a :: k -> Type) Source #
Instance details Defined in Data.Exists Methods eqForall :: forall (a0 :: k0). Const a a0 -> Const a a0 -> Bool Source #
EqForall ((:~:) a :: k -> Type) Source #
Instance details Defined in Data.Exists Methods eqForall :: forall (a0 :: k0). (a :~: a0) -> (a :~: a0) -> Bool Source #
(EqForall f, EqForall g) => EqForall (Product f g :: k -> Type) Source #
Instance details Defined in Data.Exists Methods eqForall :: forall (a :: k0). Product f g a -> Product f g a -> Bool Source #
(EqForall f, EqForall g) => EqForall (Sum f g :: k -> Type) Source #
Instance details Defined in Data.Exists Methods eqForall :: forall (a :: k0). Sum f g a -> Sum f g a -> Bool Source #
(Eq1 f, EqForall g) => EqForall (Compose f g :: k -> Type) Source #
Instance details Defined in Data.Exists Methods eqForall :: forall (a :: k0). Compose f g a -> Compose f g a -> Bool Source #
EqForall (SingList :: [k] -> Type) Source #
Instance details Defined in Data.Exists Methods eqForall :: forall (a :: k0). SingList a -> SingList a -> Bool Source #

class EqForall f => EqForallPoly f where Source #

Minimal complete definition

Nothing

Methods

eqForallPoly :: f a -> f b -> WitnessedEquality a b Source #

default eqForallPoly :: TestEquality f => f a -> f b -> WitnessedEquality a b Source #

Instances

Instances details

(EqForallPoly f, EqForallPoly g) => EqForallPoly (Product f g :: k -> Type) Source #
Instance details Defined in Data.Exists Methods eqForallPoly :: forall (a :: k0) (b :: k0). Product f g a -> Product f g b -> WitnessedEquality a b Source #
EqSing k => EqForallPoly (SingList :: [k] -> Type) Source #
Instance details Defined in Data.Exists Methods eqForallPoly :: forall (a :: k0) (b :: k0). SingList a -> SingList b -> WitnessedEquality a b Source #

class EqForeach f where Source #

Variant of EqForall that requires a pi-quantified type.

Methods

eqForeach :: Sing a -> f a -> f a -> Bool Source #

Instances

Instances details

EqForeach f => EqForeach (ApplyForeach f :: k -> Type) Source #
Instance details Defined in Data.Exists Methods eqForeach :: forall (a :: k0). Sing a -> ApplyForeach f a -> ApplyForeach f a -> Bool Source #
(Eq1 f, EqForeach g) => EqForeach (Compose f g :: k -> Type) Source #
Instance details Defined in Data.Exists Methods eqForeach :: forall (a :: k0). Sing a -> Compose f g a -> Compose f g a -> Bool Source #

class EqForall f => OrdForall f where Source #

Methods

compareForall :: f a -> f a -> Ordering Source #

Instances

Instances details

OrdForall (Proxy :: k -> Type) Source #
Instance details Defined in Data.Exists Methods compareForall :: forall (a :: k0). Proxy a -> Proxy a -> Ordering Source #
Ord a => OrdForall (Const a :: k -> Type) Source #
Instance details Defined in Data.Exists Methods compareForall :: forall (a0 :: k0). Const a a0 -> Const a a0 -> Ordering Source #
(OrdForall f, OrdForall g) => OrdForall (Product f g :: k -> Type) Source #
Instance details Defined in Data.Exists Methods compareForall :: forall (a :: k0). Product f g a -> Product f g a -> Ordering Source #
(OrdForall f, OrdForall g) => OrdForall (Sum f g :: k -> Type) Source #
Instance details Defined in Data.Exists Methods compareForall :: forall (a :: k0). Sum f g a -> Sum f g a -> Ordering Source #

class (OrdForall f, EqForallPoly f) => OrdForallPoly f where Source #

Methods

compareForallPoly :: f a -> f b -> WitnessedOrdering a b Source #

Instances

Instances details

(OrdForallPoly f, OrdForallPoly g) => OrdForallPoly (Product f g :: k -> Type) Source #
Instance details Defined in Data.Exists Methods compareForallPoly :: forall (a :: k0) (b :: k0). Product f g a -> Product f g b -> WitnessedOrdering a b Source #

class EqForeach f => OrdForeach f where Source #

Variant of OrdForall that requires a pi-quantified type.

Methods

compareForeach :: Sing a -> f a -> f a -> Ordering Source #

Instances

Instances details

OrdForeach f => OrdForeach (ApplyForeach f :: k -> Type) Source #
Instance details Defined in Data.Exists Methods compareForeach :: forall (a :: k0). Sing a -> ApplyForeach f a -> ApplyForeach f a -> Ordering Source #
(Ord1 f, OrdForeach g) => OrdForeach (Compose f g :: k -> Type) Source #
Instance details Defined in Data.Exists Methods compareForeach :: forall (a :: k0). Sing a -> Compose f g a -> Compose f g a -> Ordering Source #

class ShowForall f where Source #

Methods

showsPrecForall :: Int -> f a -> ShowS Source #

Instances

Instances details

ShowForall (Proxy :: k -> Type) Source #
Instance details Defined in Data.Exists Methods showsPrecForall :: forall (a :: k0). Int -> Proxy a -> ShowS Source #
Show a => ShowForall (Const a :: k -> Type) Source #
Instance details Defined in Data.Exists Methods showsPrecForall :: forall (a0 :: k0). Int -> Const a a0 -> ShowS Source #
(ShowForall f, ShowForall g) => ShowForall (Product f g :: k -> Type) Source #
Instance details Defined in Data.Exists Methods showsPrecForall :: forall (a :: k0). Int -> Product f g a -> ShowS Source #
(Show1 f, ShowForall g) => ShowForall (Compose f g :: k -> Type) Source #
Instance details Defined in Data.Exists Methods showsPrecForall :: forall (a :: k0). Int -> Compose f g a -> ShowS Source #

class ShowForeach f where Source #

Methods

showsPrecForeach :: Sing a -> Int -> f a -> ShowS Source #

Instances

Instances details

(Show1 f, ShowForeach g) => ShowForeach (Compose f g :: k -> Type) Source #
Instance details Defined in Data.Exists Methods showsPrecForeach :: forall (a :: k0). Sing a -> Int -> Compose f g a -> ShowS Source #

class ReadExists f where Source #

Methods

readPrecExists :: ReadPrec (Exists f) Source #

Instances

Instances details

ReadExists (Proxy :: k -> Type) Source #
Instance details Defined in Data.Exists Methods readPrecExists :: ReadPrec (Exists Proxy) Source #

class EnumForall f where Source #

Methods

toEnumForall :: Int -> f a Source #

fromEnumForall :: f a -> Int Source #

class EnumExists f where Source #

Methods

toEnumExists :: Int -> Exists f Source #

fromEnumExists :: Exists f -> Int Source #

class BoundedExists f where Source #

Methods

minBoundExists :: Exists f Source #

maxBoundExists :: Exists f Source #

class SemigroupForall f where Source #

Methods

appendForall :: f a -> f a -> f a Source #

Instances

Instances details

SemigroupForall (Proxy :: k -> Type) Source #
Instance details Defined in Data.Exists Methods appendForall :: forall (a :: k0). Proxy a -> Proxy a -> Proxy a Source #
Semigroup a => SemigroupForall (Const a :: k -> Type) Source #
Instance details Defined in Data.Exists Methods appendForall :: forall (a0 :: k0). Const a a0 -> Const a a0 -> Const a a0 Source #
SemigroupForall f => SemigroupForall (ApplyForall f :: k -> Type) Source #
Instance details Defined in Data.Exists Methods appendForall :: forall (a :: k0). ApplyForall f a -> ApplyForall f a -> ApplyForall f a Source #
(Semigroup1 f, SemigroupForall g) => SemigroupForall (Compose f g :: k -> Type) Source #
Instance details Defined in Data.Exists Methods appendForall :: forall (a :: k0). Compose f g a -> Compose f g a -> Compose f g a Source #

class SemigroupForeach f where Source #

Methods

appendForeach :: Sing a -> f a -> f a -> f a Source #

Instances

Instances details

SemigroupForeach f => SemigroupForeach (ApplyForeach f :: k -> Type) Source #
Instance details Defined in Data.Exists Methods appendForeach :: forall (a :: k0). Sing a -> ApplyForeach f a -> ApplyForeach f a -> ApplyForeach f a Source #
(Semigroup1 f, SemigroupForeach g) => SemigroupForeach (Compose f g :: k -> Type) Source #
Instance details Defined in Data.Exists Methods appendForeach :: forall (a :: k0). Sing a -> Compose f g a -> Compose f g a -> Compose f g a Source #

class SemigroupForall f => MonoidForall f where Source #

Methods

emptyForall :: f a Source #

Instances

Instances details

Monoid a => MonoidForall (Const a :: k -> Type) Source #
Instance details Defined in Data.Exists Methods emptyForall :: forall (a0 :: k0). Const a a0 Source #
MonoidForall f => MonoidForall (ApplyForall f :: k -> Type) Source #
Instance details Defined in Data.Exists Methods emptyForall :: forall (a :: k0). ApplyForall f a Source #

class SemigroupForeach f => MonoidForeach f where Source #

Methods

emptyForeach :: Sing a -> f a Source #

Instances

Instances details

MonoidForeach f => MonoidForeach (ApplyForeach f :: k -> Type) Source #
Instance details Defined in Data.Exists Methods emptyForeach :: forall (a :: k0). Sing a -> ApplyForeach f a Source #

class HashableForall f where Source #

Methods

hashWithSaltForall :: Int -> f a -> Int Source #

Instances

Instances details

Hashable a => HashableForall (Const a :: k -> Type) Source #
Instance details Defined in Data.Exists Methods hashWithSaltForall :: forall (a0 :: k0). Int -> Const a a0 -> Int Source #

class HashableForeach f where Source #

Methods

hashWithSaltForeach :: Sing a -> Int -> f a -> Int Source #

class PathPieceExists f where Source #

Methods

fromPathPieceForall :: Text -> Maybe (Exists f) Source #

toPathPieceForall :: Exists f -> Text Source #

class StorableForeach (f :: k -> Type) where Source #

Methods

peekForeach :: Sing a -> Ptr (f a) -> IO (f a) Source #

pokeForeach :: Sing a -> Ptr (f a) -> f a -> IO () Source #

sizeOfForeach :: forall (a :: k). Proxy f -> Sing a -> Int Source #

class StorableForall (f :: k -> Type) where Source #

This is like StorableForall except that the type constructor must ignore its argument (for purposes of representation).

Methods

peekForall :: Ptr (f a) -> IO (f a) Source #

pokeForall :: Ptr (f a) -> f a -> IO () Source #

sizeOfForall :: Proxy f -> Int Source #

class PrimForall (f :: k -> Type) where Source #

Be careful with this typeclass. It is more unsafe than Prim. With writeByteArray# and readByteArray#, one can implement unsafeCoerce.

Methods

sizeOfForall# :: Proxy# f -> Int# Source #

alignmentForall# :: Proxy# f -> Int# Source #

indexByteArrayForall# :: ByteArray# -> Int# -> f a Source #

readByteArrayForall# :: MutableByteArray# s -> Int# -> State# s -> (# State# s, f a #) Source #

writeByteArrayForall# :: MutableByteArray# s -> Int# -> f a -> State# s -> State# s Source #

setByteArrayForall# :: MutableByteArray# s -> Int# -> Int# -> f a -> State# s -> State# s Source #

indexOffAddrForall# :: Addr# -> Int# -> f a Source #

readOffAddrForall# :: Addr# -> Int# -> State# s -> (# State# s, f a #) Source #

writeOffAddrForall# :: Addr# -> Int# -> f a -> State# s -> State# s Source #

setOffAddrForall# :: Addr# -> Int# -> Int# -> f a -> State# s -> State# s Source #

class BinaryExists (f :: k -> Type) where Source #

Methods

putExists :: Exists f -> Put Source #

getExists :: Get (Exists f) Source #

Instances

Instances details

(SingKind k, Binary k) => BinaryExists (SingList :: [k] -> Type) Source #
Instance details Defined in Data.Exists Methods putExists :: Exists SingList -> Put Source # getExists :: Get (Exists SingList) Source #

class BinaryForeach (f :: k -> Type) where Source #

Methods

putForeach :: Sing a -> f a -> Put Source #

getForeach :: Sing a -> Get (f a) Source #

Instances

Instances details

(Binary1 f, BinaryForeach g) => BinaryForeach (Compose f g :: k -> Type) Source #
Instance details Defined in Data.Exists Methods putForeach :: forall (a :: k0). Sing a -> Compose f g a -> Put Source # getForeach :: forall (a :: k0). Sing a -> Get (Compose f g a) Source #

Higher Rank Classes

class EqForall2 f where Source #

Methods

eqForall2 :: f a b -> f a b -> Bool Source #

Instances

Instances details

EqForall2 ((:~:) :: k -> k -> Type) Source #
Instance details Defined in Data.Exists Methods eqForall2 :: forall (a :: k0) (b :: k1). (a :~: b) -> (a :~: b) -> Bool Source #

class EqForallPoly2 (f :: k -> j -> Type) where Source #

Methods

eqForallPoly2 :: forall (a :: k) (b :: j) (c :: k) (d :: j). f a b -> f c d -> WitnessedEquality '(a, b) '(c, d) Source #

class ShowForall2 f where Source #

Methods

showsPrecForall2 :: Int -> f a b -> ShowS Source #

class ShowForeach2 f where Source #

Methods

showsPrecForeach2 :: Sing a -> Sing b -> Int -> f a b -> ShowS Source #

class BinaryExists2 (f :: k -> j -> Type) where Source #

Methods

putExists2 :: Exists2 f -> Put Source #

getExists2 :: Get (Exists2 f) Source #

More Type Classes

type family Sing = (r :: k -> Type) | r -> k Source #

Instances

Instances details

type Sing Source #
Instance details Defined in Data.Exists type Sing = SingMaybe :: Maybe k -> Type
type Sing Source #
Instance details Defined in Data.Exists type Sing = SingList :: [k] -> Type

data SingList :: forall (k :: Type). [k] -> Type where Source #

Constructors

SingListNil :: SingList '[]
SingListCons :: Sing r -> SingList rs -> SingList (r ': rs)

Instances

Instances details

(SingKind k, Binary k) => BinaryExists (SingList :: [k] -> Type) Source #
Instance details Defined in Data.Exists Methods putExists :: Exists SingList -> Put Source # getExists :: Get (Exists SingList) Source #
EqForall (SingList :: [k] -> Type) Source #
Instance details Defined in Data.Exists Methods eqForall :: forall (a :: k0). SingList a -> SingList a -> Bool Source #
EqSing k => EqForallPoly (SingList :: [k] -> Type) Source #
Instance details Defined in Data.Exists Methods eqForallPoly :: forall (a :: k0) (b :: k0). SingList a -> SingList b -> WitnessedEquality a b Source #
ShowSing k => Show (SingList xs) Source #
Instance details Defined in Data.Exists Methods showsPrec :: Int -> SingList xs -> ShowS # show :: SingList xs -> String # showList :: [SingList xs] -> ShowS #

data SingMaybe :: Maybe k -> Type where Source #

Constructors

SingMaybeJust :: Sing a -> SingMaybe ('Just a)
SingMaybeNothing :: SingMaybe 'Nothing

class Reify a where Source #

Methods

reify :: Sing a Source #

Instances

Instances details

Reify ('Nothing :: Maybe a) Source #
Instance details Defined in Data.Exists Methods reify :: Sing 'Nothing Source #
Reify ('[] :: [k]) Source #
Instance details Defined in Data.Exists Methods reify :: Sing '[] Source #
Reify a2 => Reify ('Just a2 :: Maybe a1) Source #
Instance details Defined in Data.Exists Methods reify :: Sing ('Just a2) Source #
(Reify a2, Reify as) => Reify (a2 ': as :: [a1]) Source #
Instance details Defined in Data.Exists Methods reify :: Sing (a2 ': as) Source #

class Unreify k where Source #

Methods

unreify :: forall (a :: k) b. Sing a -> (Reify a => b) -> b Source #

Instances

Instances details

Unreify k => Unreify [k] Source #
Instance details Defined in Data.Exists Methods unreify :: forall (a :: [k]) b. Sing a -> (Reify a => b) -> b Source #

Sing Type Classes

class EqSing k where Source #

Methods

eqSing :: forall (a :: k) (b :: k). Sing a -> Sing b -> Maybe (a :~: b) Source #

Instances

Instances details

EqSing a => EqSing [a] Source #
Instance details Defined in Data.Exists Methods eqSing :: forall (a0 :: [a]) (b :: [a]). Sing a0 -> Sing b -> Maybe (a0 :~: b) Source #

class EqSing k => OrdSing k where Source #

Methods

compareSing :: forall (a :: k) (b :: k). Sing a -> Sing b -> WitnessedOrdering a b Source #

class ShowSing k where Source #

Methods

showsPrecSing :: forall (a :: k). Int -> Sing a -> ShowS Source #

Instances

Instances details

ShowSing k => ShowSing [k] Source #
Instance details Defined in Data.Exists Methods showsPrecSing :: forall (a :: [k]). Int -> Sing a -> ShowS Source #

class ToSing (f :: k -> Type) where Source #

Methods

toSing :: f a -> Sing a Source #

class SingKind k where Source #

The two functions must form an isomorphism.

Methods

demoteSing :: Sing (a :: k) -> k Source #

promoteSing :: k -> Exists (Sing :: k -> Type) Source #

Instances

Instances details

SingKind k => SingKind [k] Source #
Instance details Defined in Data.Exists Methods demoteSing :: forall (a :: [k]). Sing a -> [k] Source # promoteSing :: [k] -> Exists Sing Source #