module Data.Witness.Representative where
{
import Data.Witness.Any;
import Data.Witness.SimpleWitness;
class Eq1 p where
{
equals1 :: forall a. p a -> p a -> Bool;
};
data RepWitness rep a where
{
MkRepWitness :: (Is rep a) => RepWitness rep a;
};
isWitnessRepresentative :: RepWitness rep a -> rep a;
isWitnessRepresentative MkRepWitness = representative;
instance (SimpleWitness w) => SimpleWitness (RepWitness w) where
{
matchWitness wa wb = matchWitness (isWitnessRepresentative wa) (isWitnessRepresentative wb);
};
class Eq1 rep => Representative rep where
{
;
getRepWitness :: rep a -> RepWitness rep a;
};
withRepresentative :: forall rep r. (Representative rep) => (forall a. (Is rep a) => rep a -> r) -> (forall b. rep b -> r);
withRepresentative foo rep = case getRepWitness rep of
{
MkRepWitness -> foo rep;
};
;
class Representative rep => Is rep a where
{
;
representative :: rep a;
};
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;
instance Eq1 (RepWitness rep) where
{
equals1 MkRepWitness MkRepWitness = True;
};
instance Representative (RepWitness rep) where
{
getRepWitness MkRepWitness = MkRepWitness;
};
instance (Is rep a) => Is (RepWitness rep) a where
{
representative = MkRepWitness;
};
}