module Data.Type.Witness.General.Representative where
import Data.Type.Witness.General.WitnessValue
import Data.Type.Witness.Specific.Some
import Import
isWitnessRepresentative :: Dict (Is rep a) -> rep a
isWitnessRepresentative :: forall {k} (rep :: k -> Type) (a :: k). Dict (Is rep a) -> rep a
isWitnessRepresentative Dict (Is rep a)
Dict = forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative
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
withSubrepresentative :: forall {k} (p :: k -> Type) (q :: k -> Type) (a :: k) r.
Subrepresentative p q -> p a -> (Is q a => r) -> r
withSubrepresentative Subrepresentative p q
subrep p a
pa Is q a => r
f =
case Subrepresentative p q
subrep p a
pa of
Dict (Is q a)
Dict -> Is q a => r
f
type Representative :: forall k. (k -> Type) -> Constraint
class Representative rep where
getRepWitness :: Subrepresentative rep rep
instance Representative Proxy where
getRepWitness :: Subrepresentative Proxy Proxy
getRepWitness Proxy a
Proxy = forall (a :: Constraint). a => Dict a
Dict
withRepresentative :: Representative rep => rep a -> (Is rep a => r) -> r
withRepresentative :: forall {k} (rep :: k -> Type) (a :: k) r.
Representative rep =>
rep a -> (Is rep a => r) -> r
withRepresentative = forall {k} (p :: k -> Type) (q :: k -> Type) (a :: k) r.
Subrepresentative p q -> p a -> (Is q a => r) -> r
withSubrepresentative forall k (rep :: k -> Type).
Representative rep =>
Subrepresentative rep rep
getRepWitness
type Is :: forall k. (k -> Type) -> k -> Constraint
class Representative rep => Is rep a where
representative :: rep a
instance Is Proxy a where
representative :: Proxy a
representative = forall k (a :: k). Proxy a
Proxy
getRepresentative :: Is rep a => a -> rep a
getRepresentative :: forall (rep :: Type -> Type) a. Is rep a => a -> rep a
getRepresentative a
_ = forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative
rerepresentative :: Is rep a => p a -> rep a
rerepresentative :: forall {k} (rep :: k -> Type) (a :: k) (p :: k -> Type).
Is rep a =>
p a -> rep a
rerepresentative p a
_ = forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative
fromRepWitness :: Dict (Is rep a) -> rep a
fromRepWitness :: forall {k} (rep :: k -> Type) (a :: k). Dict (Is rep a) -> rep a
fromRepWitness Dict (Is rep a)
Dict = forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative
mkSomeOf :: Is rep a => a -> SomeOf rep
mkSomeOf :: forall (rep :: Type -> Type) a. Is rep a => a -> SomeOf rep
mkSomeOf a
a = forall (w :: Type -> Type) a. w a -> a -> SomeOf w
MkSomeOf forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative a
a
mkSomeFor :: Is rep a => f a -> SomeFor f rep
mkSomeFor :: forall {k} (rep :: k -> Type) (a :: k) (f :: k -> Type).
Is rep a =>
f a -> SomeFor f rep
mkSomeFor f a
fa = forall k (f :: k -> Type) (w :: k -> Type) (a :: k).
w a -> f a -> SomeFor f w
MkSomeFor forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative f a
fa
instance Representative ((:~:) (t :: k)) where
getRepWitness :: Subrepresentative ((:~:) t) ((:~:) t)
getRepWitness t :~: a
Refl = forall (a :: Constraint). a => Dict a
Dict
instance Is ((:~:) (t :: k)) (t :: k) where
representative :: t :~: t
representative = forall k (t :: k). t :~: t
Refl
instance Representative (Compose Dict c) where
getRepWitness :: Subrepresentative (Compose Dict c) (Compose Dict c)
getRepWitness (Compose Dict (c a)
Dict) = forall (a :: Constraint). a => Dict a
Dict
instance c t => Is (Compose Dict c) t where
representative :: Compose Dict c t
representative = forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose forall (a :: Constraint). a => Dict a
Dict
typeValue ::
forall k (rep :: k -> Type) (a :: k). (Is rep a, WitnessValue rep)
=> WitnessValueType rep
typeValue :: forall k (rep :: k -> Type) (a :: k).
(Is rep a, WitnessValue rep) =>
WitnessValueType rep
typeValue = forall k (w :: k -> Type) (t :: k).
WitnessValue w =>
w t -> WitnessValueType w
witnessToValue @k @rep (forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative @k @rep @a)
matchIs ::
forall w a b. (TestEquality w, Is w a, Is w b)
=> Maybe (a :~: b)
matchIs :: forall {k} (w :: k -> Type) (a :: k) (b :: k).
(TestEquality w, Is w a, Is w b) =>
Maybe (a :~: b)
matchIs = let
r :: forall t. Is w t
=> w t
r :: forall (t :: k). Is w t => w t
r = forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative
in forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall (t :: k). Is w t => w t
r @a) (forall (t :: k). Is w t => w t
r @b)