module Data.OpenWitness.Dynamic where
{
import Data.Kind;
import Data.Witness;
import Data.Type.Heterogeneous;
import Data.OpenWitness.TypeRep;
import Data.OpenWitness.Typeable;
;
type Dynamic = Any TypeRep;
;
toDyn :: forall (a :: *). Typeable a => a -> Dynamic;
toDyn = MkAny typeRep;
fromDyn :: Typeable a => Dynamic -> a -> a;
fromDyn dyn def = case fromDynamic dyn of
{
Just a -> a;
_ -> def;
};
fromDynamic :: forall (a :: *). Typeable a => Dynamic -> Maybe a;
fromDynamic (MkAny uq a) = do
{
Refl <- testEquality uq (typeRep :: TypeRep a);
return a;
};
;
dynApply :: Dynamic -> Dynamic -> Maybe Dynamic;
dynApply (MkAny (ApplyTypeRep (ApplyTypeRep repFn' rx') ry) f) (MkAny rx x) = do
{
ReflH <- testHetEquality repFn' (typeRep :: TypeRep (->));
ReflH <- testHetEquality rx' rx;
return (MkAny ry (f x));
};
dynApply _ _ = Nothing;
dynApp :: Dynamic -> Dynamic -> Dynamic;
dynApp a b = case (dynApply a b) of
{
Just d -> d;
_ -> error "Type error in dynamic application.\nCan't apply function to argument";
};
dynTypeRep :: Dynamic -> AnyWitness (TypeRep :: * -> *);
dynTypeRep (MkAny r _) = MkAnyWitness r;
}