Typeable.hs

-- | This is an approximate re-implementation of "Data.Typeable" using open witnesses.
module Data.OpenWitness.Typeable where
{
{-
    import Data.OpenWitness.OpenRep;
    import Data.OpenWitness;
    import Data.Witness;

    -- | types of kind @*@ with a representation
    ;
    class Typeable a where
    {
        rep :: OpenRep a;
    };

    -- | types of kind @* -> *@ with a representation
    ;
    class Typeable1 t where
    {
        rep1 :: OpenRep1 t;
    };

    -- | types of kind @* -> * -> *@ with a representation
    ;
    class Typeable2 t where
    {
        rep2 :: OpenRep2 t;
    };

    instance (Typeable1 f,Typeable a) => Typeable (f a) where
    {
        rep = ApplyOpenRep rep1 rep;
    };

    instance (Typeable2 f,Typeable a) => Typeable1 (f a) where
    {
        rep1 = ApplyOpenRep1 rep2 rep;
    };

    instance Typeable2 (->) where
    {
        rep2 = SimpleOpenRep2 $(iowitness [t|T2 (->)|]);
    };

    cast :: forall a b. (Typeable a,Typeable b) => a -> Maybe b;
    cast a = do
    {
        MkEqualType :: EqualType a b <- testEquality rep rep;
        return a;
    };

    gcast :: forall a b c. (Typeable a,Typeable b) => c a -> Maybe (c b);
    gcast ca = do
    {
        MkEqualType :: EqualType a b <- testEquality rep rep;
        return ca;
    };

    -- | represents a type of kind @*@
    ;
    type TypeRep = AnyWitness OpenRep;

    typeOf :: forall t. (Typeable t) => t -> TypeRep;
    typeOf _ = MkAnyWitness (rep :: OpenRep t);

    -- | represents a type of kind @* -> *@
    ;
    type TypeRep1 = AnyWitness1 OpenRep1;

    typeOf1 :: forall t a. (Typeable1 t) => t a -> TypeRep1;
    typeOf1 _ = MkAnyWitness1 (rep1 :: OpenRep1 t);

    -- | represents a type of kind @* -> * -> *@
    ;
    type TypeRep2 = AnyWitness2 OpenRep2;

    typeOf2 :: forall t a b. (Typeable2 t) => t a b -> TypeRep2;
    typeOf2 _ = MkAnyWitness2 (rep2 :: OpenRep2 t);

    -- | given representations of @a@ and @b@, make a representation of @a -> b@
    ;
    mkFunTy :: TypeRep -> TypeRep -> TypeRep;
    mkFunTy (MkAnyWitness ta) (MkAnyWitness tb) = MkAnyWitness (ApplyOpenRep (ApplyOpenRep1 (rep2 :: OpenRep2 (->)) ta) tb);

    -- | given representations of @a -> b@ and @a@, make a representation of @b@ (otherwise not)
    ;
    funResultTy :: TypeRep -> TypeRep -> Maybe TypeRep;
    funResultTy (MkAnyWitness (ApplyOpenRep (ApplyOpenRep1 repFn' ta') tb')) (MkAnyWitness ta) = do
    {
        MkEqualType <- matchOpenRep2 repFn' (rep2 :: OpenRep2 (->));
        MkEqualType <- testEquality ta' ta;
        return (MkAnyWitness tb');
    };
    funResultTy _ _ = Nothing;

    mkAppTy :: TypeRep1 -> TypeRep -> TypeRep;
    mkAppTy (MkAnyWitness1 tf) (MkAnyWitness ta) = MkAnyWitness (ApplyOpenRep tf ta);

    mkAppTy1 :: TypeRep2 -> TypeRep -> TypeRep1;
    mkAppTy1 (MkAnyWitness2 tf) (MkAnyWitness ta) = MkAnyWitness1 (ApplyOpenRep1 tf ta);
-}
}