Data.Type.Witness.General.Representative

Documentation

isWitnessRepresentative :: Dict (Is rep a) -> rep a

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

withSubrepresentative :: Subrepresentative p q -> p a -> (Is q a => r) -> r

class Representative rep where

Methods

getRepWitness :: Subrepresentative rep rep

Every value is an instance of Is.

Instances

Representative NaturalType

Defined in Data.Type.Witness.Specific.Natural

Methods

getRepWitness :: Subrepresentative NaturalType NaturalType

Representative PeanoNatType

Defined in Data.Type.Witness.Specific.PeanoNat

Methods

getRepWitness :: Subrepresentative PeanoNatType PeanoNatType

Representative SymbolType

Defined in Data.Type.Witness.Specific.Symbol

Methods

getRepWitness :: Subrepresentative SymbolType SymbolType

Representative w => Representative (ListProductType w :: Type -> Type)

Defined in Data.Type.Witness.Specific.List.Product

Methods

getRepWitness :: Subrepresentative (ListProductType w) (ListProductType w)

Representative w => Representative (ListSumType w :: Type -> Type)

Defined in Data.Type.Witness.Specific.List.Sum

Methods

getRepWitness :: Subrepresentative (ListSumType w) (ListSumType w)

Representative (Proxy :: k -> Type)

Defined in Data.Type.Witness.General.Representative

Methods

getRepWitness :: Subrepresentative Proxy Proxy

Representative (EmptyType :: k -> Type)

Defined in Data.Type.Witness.Specific.Empty

Methods

getRepWitness :: Subrepresentative EmptyType EmptyType

Representative ((:~:) t :: k -> Type)

Defined in Data.Type.Witness.General.Representative

Methods

getRepWitness :: Subrepresentative ((:~:) t) ((:~:) t)

(Representative w1, Representative w2) => Representative (PairType w1 w2 :: k -> Type)

Defined in Data.Type.Witness.Specific.Pair

Methods

getRepWitness :: Subrepresentative (PairType w1 w2) (PairType w1 w2)

Representative (Compose Dict c :: k -> Type)

Defined in Data.Type.Witness.General.Representative

Methods

getRepWitness :: Subrepresentative (Compose Dict c) (Compose Dict c)

Representative w => Representative (ListType w :: [k] -> Type)

Defined in Data.Type.Witness.Specific.List.List

Methods

getRepWitness :: Subrepresentative (ListType w) (ListType w)

withRepresentative :: Representative rep => rep a -> (Is rep a => r) -> r

class Representative rep => Is rep a where

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

Methods

representative :: rep a

The representative value for type a.

Instances

KnownNat bn => Is NaturalType (bn :: Nat)

Defined in Data.Type.Witness.Specific.Natural

Methods

representative :: NaturalType bn

Is PeanoNatType 'Zero

Defined in Data.Type.Witness.Specific.PeanoNat

Methods

representative :: PeanoNatType 'Zero

KnownSymbol symbol => Is SymbolType (symbol :: Symbol)

Defined in Data.Type.Witness.Specific.Symbol

Methods

representative :: SymbolType symbol

Is PeanoNatType n => Is PeanoNatType ('Succ n :: PeanoNat)

Defined in Data.Type.Witness.Specific.PeanoNat

Methods

representative :: PeanoNatType ('Succ n)

Representative w => Is (ListProductType w :: Type -> Type) ()

Defined in Data.Type.Witness.Specific.List.Product

Methods

representative :: ListProductType w ()

Representative w => Is (ListSumType w :: Type -> Type) Void

Defined in Data.Type.Witness.Specific.List.Sum

Methods

representative :: ListSumType w Void

Is (Proxy :: k -> Type) (a :: k)

Defined in Data.Type.Witness.General.Representative

Methods

representative :: Proxy a

(Is w a, Is (ListProductType w) ar) => Is (ListProductType w :: Type -> Type) ((a, ar) :: Type)

Defined in Data.Type.Witness.Specific.List.Product

Methods

representative :: ListProductType w (a, ar)

(Is w a, Is (ListSumType w) ar) => Is (ListSumType w :: Type -> Type) (Either a ar :: Type)

Defined in Data.Type.Witness.Specific.List.Sum

Methods

representative :: ListSumType w (Either a ar)

Is ((:~:) t :: k -> Type) (t :: k)

Defined in Data.Type.Witness.General.Representative

Methods

representative :: t :~: t

(Is w1 t, Is w2 t) => Is (PairType w1 w2 :: k -> Type) (t :: k)

Defined in Data.Type.Witness.Specific.Pair

Methods

representative :: PairType w1 w2 t

c t => Is (Compose Dict c :: k -> Type) (t :: k)

Defined in Data.Type.Witness.General.Representative

Methods

representative :: Compose Dict c t

Representative w => Is (ListType w :: [k] -> Type) ('[] :: [k])

Defined in Data.Type.Witness.Specific.List.List

Methods

representative :: ListType w '[]

(Is w a2, Is (ListType w) lt) => Is (ListType w :: [a1] -> Type) (a2 ': lt :: [a1])

Defined in Data.Type.Witness.Specific.List.List

Methods

representative :: ListType w (a2 ': lt)

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

rerepresentative :: Is rep a => p a -> rep a

fromRepWitness :: Dict (Is rep a) -> rep a

mkSomeOf :: Is rep a => a -> SomeOf rep

mkSomeFor :: 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 w a b. (TestEquality w, Is w a, Is w b) => Maybe (a :~: b)

See whether two represented and witnessed types are the same.