open-witness-0.3.1: Data/OpenWitness/OpenRep.hs

module Data.OpenWitness.OpenRep where
{
--    import Data.Witness;
--    import Data.OpenWitness;
--    import Data.Maybe;
{-
        data T2 (a :: * -> * -> *);

    data OpenRep2 p where
    {
        SimpleOpenRep2 :: IOWitness (T2 p) -> OpenRep2 p;
--        ApplyOpenRep2 :: OpenRep3 p -> OpenRep a -> OpenRep2 (p a);
    };

    matchOpenRep2 :: OpenRep2 a -> OpenRep2 b -> Maybe (EqualType (T2 a) (T2 b));
    matchOpenRep2 (SimpleOpenRep2 wa) (SimpleOpenRep2 wb) = testEquality wa wb;
{-
    matchOpenRep2 (ApplyOpenRep1 tfa ta) (ApplyOpenRep1 tfb tb) = do
    {
        MkEqualType <- matchOpenRep2 tfa tfb;
        MkEqualType <- testEquality ta tb;
        return MkEqualType;
    };
    matchOpenRep2 _ _ = Nothing;
-}

        data T1 (a :: * -> *);

    data OpenRep1 p where
    {
        SimpleOpenRep1 :: IOWitness (T1 p) -> OpenRep1 p;
        ApplyOpenRep1 :: OpenRep2 p -> OpenRep a -> OpenRep1 (p a);
    };

    matchOpenRep1 :: OpenRep1 a -> OpenRep1 b -> Maybe (EqualType (T1 a) (T1 b));
    matchOpenRep1 (SimpleOpenRep1 wa) (SimpleOpenRep1 wb) = testEquality wa wb;
    matchOpenRep1 (ApplyOpenRep1 tfa ta) (ApplyOpenRep1 tfb tb) = do
    {
        MkEqualType <- matchOpenRep2 tfa tfb;
        MkEqualType <- testEquality ta tb;
        return MkEqualType;
    };
    matchOpenRep1 _ _ = Nothing;
-}

{-
    data OpenRep :: k -> * where
    {
        SimpleOpenRep :: IOWitness a -> OpenRep a;
        ApplyOpenRep :: OpenRep p -> OpenRep a -> OpenRep (p a);
    };

    instance TestEquality OpenRep where
    {
        testEquality (SimpleOpenRep wa) (SimpleOpenRep wb) = testEquality wa wb;
        testEquality (ApplyOpenRep tfa ta) (ApplyOpenRep tfb tb) = do
        {
            MkEqualType <- testEquality tfa tfb;
            MkEqualType <- testEquality ta tb;
            return MkEqualType;
        };
        testEquality _ _ = Nothing;
    };

    instance Eq1 OpenRep where
    {
        equals1 r1 r2 = isJust (testEquality r1 r2);
    };
-}
}