Safe Haskell	None
Language	GHC2021

Data.Type.Witness.General.Representative

Synopsis

isWitnessRepresentative :: forall {k} rep (a :: k). Dict (Is rep a) -> rep a
type Subrepresentative (p :: k -> Type) (q :: k -> Type) = forall (a :: k). p a -> Dict (Is q a)
withSubrepresentative :: forall {k} p (q :: k -> Type) (a :: k) r. Subrepresentative p q -> p a -> (Is q a => r) -> r
class Representative (rep :: k -> Type) where
- getRepWitness :: Subrepresentative rep rep
withRepresentative :: forall {k} rep (a :: k) r. Representative rep => rep a -> (Is rep a => r) -> r
class Representative rep => Is (rep :: k -> Type) (a :: k) where
- representative :: rep a
getRepresentative :: Is rep a => a -> rep a
rerepresentative :: forall {k} rep (a :: k) p. Is rep a => p a -> rep a
fromRepWitness :: forall {k} rep (a :: k). Dict (Is rep a) -> rep a
mkSomeOf :: forall (rep :: Type -> Type) a. Is rep a => a -> SomeOf rep
mkSomeFor :: forall {k} (rep :: k -> Type) (a :: k) f. Is rep a => f a -> SomeFor f rep
typeValue :: forall k (rep :: k -> Type) (a :: k). (Is rep a, WitnessValue rep) => WitnessValueType rep
matchIs :: forall {k} (w :: k -> Type) (a :: k) (b :: k). (TestEquality w, Is w a, Is w b) => Maybe (a :~: b)

Documentation

isWitnessRepresentative :: forall {k} rep (a :: k). Dict (Is rep a) -> rep a Source #

type Subrepresentative (p :: k -> Type) (q :: k -> Type) = forall (a :: k). p a -> Dict (Is q a) Source #

withSubrepresentative :: forall {k} p (q :: k -> Type) (a :: k) r. Subrepresentative p q -> p a -> (Is q a => r) -> r Source #

class Representative (rep :: k -> Type) where Source #

Methods

getRepWitness :: Subrepresentative rep rep Source #

Every value is an instance of Is.

Instances

Instances details

Representative NaturalType Source #
Instance details Defined in Data.Type.Witness.Specific.Natural Methods getRepWitness :: Subrepresentative NaturalType NaturalType Source #
Representative PeanoNatType Source #
Instance details Defined in Data.Type.Witness.Specific.PeanoNat Methods getRepWitness :: Subrepresentative PeanoNatType PeanoNatType Source #
Representative SymbolType Source #
Instance details Defined in Data.Type.Witness.Specific.Symbol Methods getRepWitness :: Subrepresentative SymbolType SymbolType Source #
Representative w => Representative (ListProductType w :: Type -> Type) Source #
Instance details Defined in Data.Type.Witness.Specific.List.Product Methods getRepWitness :: Subrepresentative (ListProductType w) (ListProductType w) Source #
Representative w => Representative (ListSumType w :: Type -> Type) Source #
Instance details Defined in Data.Type.Witness.Specific.List.Sum Methods getRepWitness :: Subrepresentative (ListSumType w) (ListSumType w) Source #
Representative (Proxy :: k -> Type) Source #
Instance details Defined in Data.Type.Witness.General.Representative Methods getRepWitness :: Subrepresentative (Proxy :: k -> Type) (Proxy :: k -> Type) Source #
Representative (EmptyType :: k -> Type) Source #
Instance details Defined in Data.Type.Witness.Specific.Empty Methods getRepWitness :: Subrepresentative (EmptyType :: k -> Type) (EmptyType :: k -> Type) Source #
Representative ((:~:) t :: k -> Type) Source #
Instance details Defined in Data.Type.Witness.General.Representative Methods getRepWitness :: Subrepresentative ((:~:) t) ((:~:) t) Source #
(Representative w1, Representative w2) => Representative (PairType w1 w2 :: k -> Type) Source #
Instance details Defined in Data.Type.Witness.Specific.Pair Methods getRepWitness :: Subrepresentative (PairType w1 w2) (PairType w1 w2) Source #
Representative (Compose Dict c :: k -> Type) Source #
Instance details Defined in Data.Type.Witness.General.Representative Methods getRepWitness :: Subrepresentative (Compose Dict c) (Compose Dict c) Source #
Representative w => Representative (ListType w :: [k] -> Type) Source #
Instance details Defined in Data.Type.Witness.Specific.List.List Methods getRepWitness :: Subrepresentative (ListType w) (ListType w) Source #

withRepresentative :: forall {k} rep (a :: k) r. Representative rep => rep a -> (Is rep a => r) -> r Source #

class Representative rep => Is (rep :: k -> Type) (a :: k) where Source #

If two representatives have the same type, then they have the same value.

Methods

representative :: rep a Source #

The representative value for type a.

Instances

Instances details

KnownNat bn => Is NaturalType (bn :: Nat) Source #
Instance details Defined in Data.Type.Witness.Specific.Natural Methods representative :: NaturalType bn Source #
Is PeanoNatType 'Zero Source #
Instance details Defined in Data.Type.Witness.Specific.PeanoNat Methods representative :: PeanoNatType 'Zero Source #
KnownSymbol symbol => Is SymbolType (symbol :: Symbol) Source #
Instance details Defined in Data.Type.Witness.Specific.Symbol Methods representative :: SymbolType symbol Source #
Is PeanoNatType n => Is PeanoNatType ('Succ n :: PeanoNat) Source #
Instance details Defined in Data.Type.Witness.Specific.PeanoNat Methods representative :: PeanoNatType ('Succ n) Source #
Representative w => Is (ListProductType w :: Type -> Type) () Source #
Instance details Defined in Data.Type.Witness.Specific.List.Product Methods representative :: ListProductType w () Source #
Representative w => Is (ListSumType w :: Type -> Type) Void Source #
Instance details Defined in Data.Type.Witness.Specific.List.Sum Methods representative :: ListSumType w Void Source #
Is (Proxy :: k -> Type) (a :: k) Source #
Instance details Defined in Data.Type.Witness.General.Representative Methods representative :: Proxy a Source #
(Is w a, Is (ListProductType w) ar) => Is (ListProductType w :: Type -> Type) ((a, ar) :: Type) Source #
Instance details Defined in Data.Type.Witness.Specific.List.Product Methods representative :: ListProductType w (a, ar) Source #
(Is w a, Is (ListSumType w) ar) => Is (ListSumType w :: Type -> Type) (Either a ar :: Type) Source #
Instance details Defined in Data.Type.Witness.Specific.List.Sum Methods representative :: ListSumType w (Either a ar) Source #
Is ((:~:) t :: k -> Type) (t :: k) Source #
Instance details Defined in Data.Type.Witness.General.Representative Methods representative :: t :~: t Source #
(Is w1 t, Is w2 t) => Is (PairType w1 w2 :: k -> Type) (t :: k) Source #
Instance details Defined in Data.Type.Witness.Specific.Pair Methods representative :: PairType w1 w2 t Source #
c t => Is (Compose Dict c :: k -> Type) (t :: k) Source #
Instance details Defined in Data.Type.Witness.General.Representative Methods representative :: Compose Dict c t Source #
Representative w => Is (ListType w :: [k] -> Type) ('[] :: [k]) Source #
Instance details Defined in Data.Type.Witness.Specific.List.List Methods representative :: ListType w ('[] :: [k]) Source #
(Is w a2, Is (ListType w) lt) => Is (ListType w :: [a1] -> Type) (a2 ': lt :: [a1]) Source #
Instance details Defined in Data.Type.Witness.Specific.List.List Methods representative :: ListType w (a2 ': lt) Source #

getRepresentative :: Is rep a => a -> rep a Source #

rerepresentative :: forall {k} rep (a :: k) p. Is rep a => p a -> rep a Source #

fromRepWitness :: forall {k} rep (a :: k). Dict (Is rep a) -> rep a Source #

mkSomeOf :: forall (rep :: Type -> Type) a. Is rep a => a -> SomeOf rep Source #

mkSomeFor :: forall {k} (rep :: k -> Type) (a :: k) f. Is rep a => f a -> SomeFor f rep Source #

typeValue :: forall k (rep :: k -> Type) (a :: k). (Is rep a, WitnessValue rep) => WitnessValueType rep Source #

matchIs :: forall {k} (w :: k -> Type) (a :: k) (b :: k). (TestEquality w, Is w a, Is w b) => Maybe (a :~: b) Source #

See whether two represented and witnessed types are the same.