Safe Haskell	None
Language	GHC2021

Data.Type.Witness.Specific.Some

Synopsis

data SomeFor (f :: k -> Type) (w :: k -> Type) = MkSomeFor (w a) (f a)
mapSome :: forall k (g :: k -> Type) w1 w2. (forall (t :: k). w1 t -> w2 t) -> SomeFor g w1 -> SomeFor g w2
matchSomeFor :: forall {k} w (a :: k) f. TestEquality w => w a -> SomeFor f w -> Maybe (f a)
type SomeOf = SomeFor Identity
pattern MkSomeOf :: () => w a -> a -> SomeOf w
matchSomeOf :: TestEquality w => w a -> SomeOf w -> Maybe a
type Some = SomeFor (Const () :: k -> Type)
pattern MkSome :: forall {k} w (a :: k). () => w a -> Some w
matchSome :: forall k w (a :: k). TestEquality w => w a -> Some w -> Bool
withSomeAllConstraint :: AllConstraint c w => Some w -> (forall (a :: k). c (w a) => w a -> r) -> r
someForToSome :: forall {k} (f :: k -> Type) (w :: k -> Type). SomeFor f w -> Some w

Documentation

data SomeFor (f :: k -> Type) (w :: k -> Type) Source #

Any value with a witness to a parameter of its type.

Constructors

MkSomeFor (w a) (f a)

Instances

Instances details

(TestEquality w, WitnessConstraint Eq w) => Eq (SomeOf w) Source #
Instance details Defined in Data.Type.Witness.Specific.Some Methods (==) :: SomeOf w -> SomeOf w -> Bool # (/=) :: SomeOf w -> SomeOf w -> Bool #
AllConstraint Show w => Show (Some w) Source #
Instance details Defined in Data.Type.Witness.Specific.Some Methods showsPrec :: Int -> Some w -> ShowS # show :: Some w -> String # showList :: [Some w] -> ShowS #
(TestEquality w, FiniteWitness w) => Countable (Some w) Source #
Instance details Defined in Data.Type.Witness.General.Finite Methods countPrevious :: Some w -> Maybe (Some w) # countMaybeNext :: Maybe (Some w) -> Maybe (Some w) #
(TestEquality w, FiniteWitness w) => Finite (Some w) Source #
Instance details Defined in Data.Type.Witness.General.Finite Methods allValues :: [Some w] # assemble :: forall b f. Applicative f => (Some w -> f b) -> f (Some w -> b) #
(TestEquality w, FiniteWitness w) => Searchable (Some w) Source #
Instance details Defined in Data.Type.Witness.General.Finite Methods search :: (Some w -> Maybe b) -> Maybe b #
TestEquality w => Eq (Some w) Source #
Instance details Defined in Data.Type.Witness.Specific.Some Methods (==) :: Some w -> Some w -> Bool # (/=) :: Some w -> Some w -> Bool #
TestOrder w => Ord (Some w) Source #
Instance details Defined in Data.Type.Witness.Specific.Some Methods compare :: Some w -> Some w -> Ordering # (<) :: Some w -> Some w -> Bool # (<=) :: Some w -> Some w -> Bool # (>) :: Some w -> Some w -> Bool # (>=) :: Some w -> Some w -> Bool # max :: Some w -> Some w -> Some w # min :: Some w -> Some w -> Some w #

mapSome :: forall k (g :: k -> Type) w1 w2. (forall (t :: k). w1 t -> w2 t) -> SomeFor g w1 -> SomeFor g w2 Source #

matchSomeFor :: forall {k} w (a :: k) f. TestEquality w => w a -> SomeFor f w -> Maybe (f a) Source #

type SomeOf = SomeFor Identity Source #

pattern MkSomeOf :: () => w a -> a -> SomeOf w Source #

matchSomeOf :: TestEquality w => w a -> SomeOf w -> Maybe a Source #

type Some = SomeFor (Const () :: k -> Type) Source #

pattern MkSome :: forall {k} w (a :: k). () => w a -> Some w Source #

matchSome :: forall k w (a :: k). TestEquality w => w a -> Some w -> Bool Source #

withSomeAllConstraint :: AllConstraint c w => Some w -> (forall (a :: k). c (w a) => w a -> r) -> r Source #

someForToSome :: forall {k} (f :: k -> Type) (w :: k -> Type). SomeFor f w -> Some w Source #