module Data.Witness.Representative where
{
import Data.Witness.Any;
import Data.Constraint;
import Data.Proxy;
class Eq1 (p :: k -> *) where
{
equals1 :: forall a. p a -> p a -> Bool;
};
instance Eq1 Proxy where
{
equals1 Proxy Proxy = True;
};
isWitnessRepresentative :: Dict (Is rep a) -> rep a;
isWitnessRepresentative Dict = representative;
class Eq1 rep => Representative (rep :: k -> *) where
{
;
getRepWitness :: forall (a :: k). rep a -> Dict (Is rep a);
};
instance Representative Proxy where
{
getRepWitness Proxy = Dict;
};
withRepresentative :: forall (rep :: k -> *) r. (Representative rep) =>
(forall (a :: k). (Is rep a) => rep a -> r) -> (forall (b :: k). rep b -> r);
withRepresentative foo rep = case getRepWitness rep of
{
Dict -> foo rep;
};
;
class Representative rep => Is (rep :: k -> *) (a :: k) where
{
;
representative :: rep a;
};
instance Is Proxy a where
{
representative = Proxy;
};
getRepresentative :: (Is rep a) => a -> rep a;
getRepresentative _ = representative;
rerepresentative :: (Is rep a) => p a -> rep a;
rerepresentative _ = representative;
mkAny :: (Is rep a) => a -> Any rep;
mkAny a = MkAny representative a;
mkAnyF :: (Is rep a) => f a -> AnyF rep f;
mkAnyF fa = MkAnyF representative fa;
}