open-witness 0.1.1 → 0.3.1

raw patch · 8 files changed

+459/−382 lines, 8 filesdep +hashabledep +randomdep +template-haskelldep −mtldep ~basedep ~witnessPVP ok

version bump matches the API change (PVP)

Dependencies added: hashable, random, template-haskell, transformers

Dependencies removed: mtl

Dependency ranges changed: base, witness

API changes (from Hackage documentation)

Files

• Data/OpenWitness.hs +123/−78
• Data/OpenWitness/Dynamic.hs +42/−39
• Data/OpenWitness/Exception.hs +41/−32
• Data/OpenWitness/OpenRep.hs +70/−0
• Data/OpenWitness/ST.hs +50/−48
• Data/OpenWitness/Typeable.hs +86/−93
• Data/OpenWitness/Typeable/Rep.hs +0/−62
• open-witness.cabal +47/−30

@@ -1,89 +1,134 @@+{-# OPTIONS -fno-warn-name-shadowing #-} module Data.OpenWitness (-	OpenWitness,-	RealWorld,IOWitness,newIOWitness,-	OW,newOpenWitnessOW,runOW,owToIO,---	unsafeIOWitnessFromInteger,-	unsafeIOWitnessFromString+    OpenWitness,+    RealWorld,IOWitness,newIOWitness,+    OW,newOpenWitnessOW,runOW,owToIO,+--    unsafeIOWitnessFromInteger,+--    unsafeIOWitnessFromString,+    iowitness ) where {-	import Data.Witness;-	import Unsafe.Coerce;-	import System.IO.Unsafe (unsafePerformIO);-	import Control.Concurrent.MVar;-	import Control.Monad.State;-	import Data.HashTable;+    import Prelude;+    import Data.List;+    import System.Random;+    import Language.Haskell.TH;+    import Unsafe.Coerce;+    import System.IO.Unsafe (unsafePerformIO);+    import Control.Concurrent.MVar;+    import Control.Monad.Fix;+    import Control.Monad.Trans.State;+    import Data.Functor.Identity;+    import Data.Traversable;+    import Data.Hashable;+    import Data.Witness; -	unsafeSameType :: EqualType a b;-	unsafeSameType = unsafeCoerce MkEqualType; -	-- | A witness type that can witness to any type.-	-- But values cannot be constructed; they can only be generated in 'IO' and certain other monads.-	;-	newtype OpenWitness s a = MkOpenWitness Integer deriving Eq;-	-	instance SimpleWitness (OpenWitness s) where-	{-		matchWitness (MkOpenWitness ua) (MkOpenWitness ub) = -			if ua == ub then Just unsafeSameType else Nothing;-	};+    unsafeSameType :: a :~: b;+    unsafeSameType = unsafeCoerce Refl; -	-- | The @s@ type for running 'OW' in 'IO'.-	;-	data RealWorld;+    -- | A witness type that can witness to any type.+    -- But values cannot be constructed; they can only be generated in 'IO' and certain other monads.+    ;+    newtype OpenWitness s (a :: k) = MkOpenWitness Integer deriving Eq; -	-- | An 'OpenWitness' for 'IO'.-	;-	type IOWitness = OpenWitness RealWorld;+    instance TestEquality (OpenWitness s) where+    {+        testEquality (MkOpenWitness ua) (MkOpenWitness ub) =+            if ua == ub then Just unsafeSameType else Nothing;+    }; -	ioWitnessSource :: MVar Integer;-	{-# NOINLINE ioWitnessSource #-};-	ioWitnessSource = unsafePerformIO (newMVar 0);+    -- | The @s@ type for running 'OW' in 'IO'.+    ;+    data RealWorld; -	-- | Generate a new 'IOWitness' in 'IO'.-	;-	newIOWitness :: forall a. IO (IOWitness a);-	newIOWitness = do-	{-		val <- takeMVar ioWitnessSource;-		putMVar ioWitnessSource (val + 1);-		return (MkOpenWitness val);-	};-	-	type OWState = Integer;-	-	-- | A runnable monad in which 'OpenWitness' values can be generated.-	-- The @s@ parameter plays the same role as it does in 'ST', preventing 'OpenWitness' values from one run being used in another.-	;-	newtype OW s a = MkOW (State OWState a) deriving (Functor,Monad,MonadFix);-	-	-- | Run an 'OW' computation.-	;-	runOW :: forall a. (forall s. OW s a) -> a;-	runOW uw = (\(MkOW st) -> evalState st 0) uw;-	-	-- | Generate a new 'OpenWitness' in 'OW'.-	;-	newOpenWitnessOW :: forall s a. OW s (OpenWitness s a);-	newOpenWitnessOW = MkOW (State (\val -> (MkOpenWitness val,val+1)));-	-	-- | Run an 'OW' computation in 'IO'.-	;-	owToIO :: OW RealWorld a -> IO a;-	owToIO (MkOW st) = modifyMVar ioWitnessSource (\start -> let-	{-		(a,count) = runState st start;-	} in return (count,a));-	-	-- | In the absence of open witness declarations, an unsafe hack to generate 'IOWitness' values.-	-- This is safe if you use a different integer each time, and if @a@ is a single type.-	;-	unsafeIOWitnessFromInteger :: Integer -> IOWitness a;-	unsafeIOWitnessFromInteger = MkOpenWitness;-	-	-- | In the absence of open witness declarations, an unsafe hack to generate 'IOWitness' values.-	-- This is safe if you use a different string each time (and 'hashString' doesn't collide), and if @a@ is a single type.-	;-	unsafeIOWitnessFromString :: String -> IOWitness a;-	unsafeIOWitnessFromString = unsafeIOWitnessFromInteger . fromIntegral . hashString;+    -- | An 'OpenWitness' for 'IO'.+    ;+    type IOWitness = OpenWitness RealWorld;++    ioWitnessSource :: MVar Integer;+    {-# NOINLINE ioWitnessSource #-};+    ioWitnessSource = unsafePerformIO (newMVar 0);++    -- | Generate a new 'IOWitness' in 'IO'.+    ;+    newIOWitness :: forall a. IO (IOWitness a);+    newIOWitness = do+    {+        val <- takeMVar ioWitnessSource;+        putMVar ioWitnessSource (val + 1);+        return (MkOpenWitness val);+    };++    type OWState = Integer;++    -- | A runnable monad in which 'OpenWitness' values can be generated.+    -- The @s@ parameter plays the same role as it does in 'ST', preventing 'OpenWitness' values from one run being used in another.+    ;+    newtype OW s a = MkOW (State OWState a) deriving (Functor,Applicative,Monad,MonadFix);++    -- | Run an 'OW' computation.+    ;+    runOW :: forall a. (forall s. OW s a) -> a;+    runOW uw = (\(MkOW st) -> evalState st 0) uw;++    -- | Generate a new 'OpenWitness' in 'OW'.+    ;+    newOpenWitnessOW :: forall s a. OW s (OpenWitness s a);+    newOpenWitnessOW = MkOW (StateT (\val -> Identity (MkOpenWitness val,val+1)));++    -- | Run an 'OW' computation in 'IO'.+    ;+    owToIO :: OW RealWorld a -> IO a;+    owToIO (MkOW st) = modifyMVar ioWitnessSource (\start -> let+    {+        (a,count) = runState st start;+    } in return (count,a));++    -- | An unsafe hack to generate 'IOWitness' values.+    -- This is safe if you use a different integer each time, and if @a@ is a single type.+    ;+    unsafeIOWitnessFromInteger :: Integer -> IOWitness a;+    unsafeIOWitnessFromInteger = MkOpenWitness;++    -- | An unsafe hack to generate 'IOWitness' values.+    -- This is safe if you use a different string each time (and 'hashString' doesn't collide), and if @a@ is a single type.+    ;+    unsafeIOWitnessFromString :: String -> IOWitness a;+    unsafeIOWitnessFromString = unsafeIOWitnessFromInteger . fromIntegral . hash;++    -- | Template Haskell function to declare 'IOWitness' values.+    ;+    iowitness :: TypeQ -> Q Exp;+    iowitness qt = do+    {+        t <- qt;+        _ <- forM (freevarsType t) (\v -> reportError ("Type variable "++(show v)++" free in iowitness type"));+        l <- location;+        rnd :: Integer <- runIO randomIO;+        key <- return ((showLoc l) ++ "/" ++ (show rnd));+        keyExpr <- return (LitE (StringL key));+        untypedWitExpr <- [| unsafeIOWitnessFromString $(return keyExpr) |];+        [| $(return untypedWitExpr) :: IOWitness $(return t) |];+    } where+    {+        showLoc :: Loc -> String;+        showLoc l = (loc_filename l) ++ "=" ++ (loc_package l) ++ ":" ++ (loc_module l) ++ (show (loc_start l)) ++ (show (loc_end l));++        unionList :: (Eq a) => [[a]] -> [a];+        unionList [] = [];+        unionList (l:ls) = union l (unionList ls);++        bindingvarTVB :: TyVarBndr -> Name;+        bindingvarTVB (PlainTV n) = n;+        bindingvarTVB (KindedTV n _) = n;++        freevarsType :: Language.Haskell.TH.Type -> [Name];+        freevarsType (ForallT tvbs ps t) =+         (union (freevarsType t) (unionList (fmap freevarsType ps))) \\ (fmap bindingvarTVB tvbs);+        freevarsType (VarT name) = [name];+        freevarsType (AppT t1 t2) = union (freevarsType t1) (freevarsType t2);+        freevarsType (SigT t _) = freevarsType t;+        freevarsType _ = [];+    }; }

@@ -1,53 +1,56 @@ -- | This is an approximate re-implementation of "Data.Dynamic" using open witnesses. module Data.OpenWitness.Dynamic where {-	import Data.Witness;-	import Data.OpenWitness.Typeable;+{-+    import Data.Witness;+    import Data.OpenWitness.OpenRep;+    import Data.OpenWitness.Typeable; -	-- * The @Dynamic@ type-	;+    -- * The @Dynamic@ type+    ; -	type Dynamic = Any Rep;+    type Dynamic = Any OpenRep; -	-- * Converting to and from @Dynamic@-	;+    -- * Converting to and from @Dynamic@+    ; -	toDyn :: Typeable a => a -> Dynamic;-	toDyn = MkAny rep;+    toDyn :: Typeable a => a -> Dynamic;+    toDyn = MkAny rep; -	fromDyn :: Typeable a => Dynamic -> a -> a;-	fromDyn dyn def = case fromDynamic dyn of-	{-		Just a -> a;-		_ -> def;-	};+    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-	{-		MkEqualType <- matchWitness uq (rep :: Rep a);-		return a;-	};+    fromDynamic :: forall a. Typeable a => Dynamic -> Maybe a;+    fromDynamic (MkAny uq a) = do+    {+        MkEqualType <- testEquality uq (rep :: OpenRep a);+        return a;+    }; -	-- * Applying functions of dynamic type-	;+    -- * Applying functions of dynamic type+    ; -	dynApply :: Dynamic -> Dynamic -> Maybe Dynamic;-	dynApply (MkAny (ApplyRep (ApplyRep1 repFn' rx') ry) f) (MkAny rx x) = do-	{-		MkEqualType <- matchRep2 repFn' (rep2 :: Rep2 (->));-		MkEqualType <- matchWitness rx' rx;-		return (MkAny ry (f x));-	};-	dynApply _ _ = Nothing;+    dynApply :: Dynamic -> Dynamic -> Maybe Dynamic;+    dynApply (MkAny (ApplyOpenRep (ApplyOpenRep1 repFn' rx') ry) f) (MkAny rx x) = do+    {+        MkEqualType <- matchOpenRep2 repFn' (rep2 :: OpenRep2 (->));+        MkEqualType <- testEquality 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";-	};+    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 -> TypeRep;-	dynTypeRep (MkAny r _) = MkAnyWitness r;+    dynTypeRep :: Dynamic -> TypeRep;+    dynTypeRep (MkAny r _) = MkAnyWitness r;+-} }

@@ -1,39 +1,48 @@+{-# LANGUAGE DeriveDataTypeable #-}+{-# OPTIONS -fno-warn-unused-matches #-} module Data.OpenWitness.Exception (-	Exn, unsafeExnFromString, throw, catch+    Exn, declexn, throw, catch ) where {-	import Data.OpenWitness;-	import Data.Witness;-	import Data.Maybe;-	import Data.Typeable;-	import Control.Exception (throwDyn,catchDyn);-	import Prelude(IO,String);+    import Data.OpenWitness;+    import Data.Witness;+    import Data.Maybe;+    import Data.Typeable;+    import Language.Haskell.TH;+    import qualified Control.Exception as CE (Exception,throw,catch);+    import Prelude(IO,Show(..)); -	-- | A key to match exceptions. The type variable is the data the exception carries.-	;-	type Exn = IOWitness;+    -- | A key to match exceptions. The type variable is the data the exception carries.+    ;+    newtype Exn (e :: *) = MkExn (IOWitness e); -	newtype ExnException = MkExnException (Any Exn);-	-	-- | In the absence of open witness declarations, an unsafe hack to generate 'Exn' exception keys.-	-- This is safe if you use a different string each time (and 'hashString' doesn't collide), and if @e@ is a single type.-	;-	unsafeExnFromString :: String -> Exn e;-	unsafeExnFromString = unsafeIOWitnessFromString;-	-	instance Typeable ExnException where-	{-		typeOf _ = mkTyConApp (mkTyCon "Data.OpenWitness.Exception.ExnException") [];-	};-	-	throw :: Exn e -> e -> a;-	throw exn e = throwDyn (MkExnException (MkAny exn e));-	-	catch :: IO a -> Exn e -> (e -> IO a) -> IO a;-	catch foo exn catcher = catchDyn foo (\ex@(MkExnException cell) -> case matchAny exn cell of-	{-		Just e -> catcher e;-		_ -> throwDyn ex;-	});+    instance TestEquality Exn where+    {+        testEquality (MkExn a) (MkExn b) = testEquality a b;+    };++    newtype ExnException = MkExnException (Any Exn) deriving Typeable;++    -- | Template Haskell function to declare 'Exn' exception keys.+    ;+    declexn :: TypeQ -> Q Exp;+    declexn te = [| MkExn $(iowitness te) |];++    instance Show ExnException where+    {+        show _ = "ExnException";+    };++    instance CE.Exception ExnException;++    throw :: Exn e -> e -> a;+    throw exn e = CE.throw (MkExnException (MkAny exn e));++    catch :: IO a -> Exn e -> (e -> IO a) -> IO a;+    catch foo exn catcher = CE.catch foo (\ex@(MkExnException cell) -> case matchAny exn cell of+    {+        Just e -> catcher e;+        _ -> CE.throw ex;+    }); }

@@ -0,0 +1,70 @@+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);+    };+-}+}

@@ -1,57 +1,59 @@ -- | This is an approximate re-implementation of "Control.Monad.ST" and "Data.STRef" using open witnesses. module Data.OpenWitness.ST (-	-- * The @ST@ Monad-	ST,runST,fixST,-	-- * Converting @ST@ to @OW@ and @IO@-	stToOW,RealWorld,stToIO,-	-- * STRefs-	STRef,newSTRef,readSTRef,writeSTRef,modifySTRef+    -- * The @ST@ Monad+    ST,runST,fixST,+    -- * Converting @ST@ to @OW@ and @IO@+    stToOW,RealWorld,stToIO,+    -- * STRefs+    STRef,newSTRef,readSTRef,writeSTRef,modifySTRef ) where {-	import Data.OpenWitness;-	import Data.Witness.WitnessDict;-	import Control.Monad.State;-	-	type ST s = StateT (WitnessDict (OpenWitness s)) (OW s);+    import Data.OpenWitness;+    import Data.Witness.WitnessDict;+    import Control.Monad.Trans.State;+    import Control.Monad.Trans.Class;+    import Control.Monad.Fix; -	stToOW :: ST s a -> OW s a;-	stToOW st = evalStateT st emptyWitnessDict;+    type ST s = StateT (WitnessDict (OpenWitness s)) (OW s); -	runST :: (forall s . ST s a) -> a;-	runST st = runOW (stToOW st);-	-	fixST :: (a -> ST s a) -> ST s a;-	fixST = mfix;+    stToOW :: ST s a -> OW s a;+    stToOW st = evalStateT st emptyWitnessDict; -	type STRef = OpenWitness;-	-	newSTRef :: a -> ST s (STRef s a);-	newSTRef a = do-	{-		wit <- lift newOpenWitnessOW;-		dict <- get;-		put (witnessDictAdd wit a dict);-		return wit;-	};-	-	readSTRef :: STRef s a -> ST s a;-	readSTRef key = do-	{-		dict <- get;-		case witnessDictLookup key dict of-		{-			Just a -> return a;-			_ -> fail "ref not found";-		};-	};-	-	writeSTRef :: forall s a. STRef s a -> a -> ST s ();-	writeSTRef key newa = modify (witnessDictReplace key newa);-	-	modifySTRef :: forall s a. STRef s a -> (a -> a) -> ST s ();-	modifySTRef key amap = modify (witnessDictModify key amap);-	-	stToIO :: ST RealWorld a -> IO a;-	stToIO = owToIO . stToOW;+    runST :: (forall s . ST s a) -> a;+    runST st = runOW (stToOW st);++    fixST :: (a -> ST s a) -> ST s a;+    fixST = mfix;++    type STRef = OpenWitness;++    newSTRef :: a -> ST s (STRef s a);+    newSTRef a = do+    {+        wit <- lift newOpenWitnessOW;+        dict <- get;+        put (witnessDictAdd wit a dict);+        return wit;+    };++    readSTRef :: STRef s a -> ST s a;+    readSTRef key = do+    {+        dict <- get;+        case witnessDictLookup key dict of+        {+            Just a -> return a;+            _ -> fail "ref not found";+        };+    };++    writeSTRef :: forall s a. STRef s a -> a -> ST s ();+    writeSTRef key newa = modify (witnessDictReplace key newa);++    modifySTRef :: forall s a. STRef s a -> (a -> a) -> ST s ();+    modifySTRef key amap = modify (witnessDictModify key amap);++    stToIO :: ST RealWorld a -> IO a;+    stToIO = owToIO . stToOW; }

@@ -1,109 +1,102 @@ -- | This is an approximate re-implementation of "Data.Typeable" using open witnesses.-module Data.OpenWitness.Typeable-(-	module Data.OpenWitness.Typeable.Rep,-	module Data.OpenWitness.Typeable-) where+module Data.OpenWitness.Typeable where {-	import Data.OpenWitness.Typeable.Rep;-	import Data.OpenWitness;-	import Data.Witness;-	import Data.Maybe;+{-+    import Data.OpenWitness.OpenRep;+    import Data.OpenWitness;+    import Data.Witness; -	-- | types of kind @*@ with a representation-	;-	class Typeable a where-	{-		rep :: Rep a;-	};+    -- | types of kind @*@ with a representation+    ;+    class Typeable a where+    {+        rep :: OpenRep a;+    }; -	-- | types of kind @* -> *@ with a representation-	;-	class Typeable1 t where-	{-		rep1 :: Rep1 t;-	};+    -- | types of kind @* -> *@ with a representation+    ;+    class Typeable1 t where+    {+        rep1 :: OpenRep1 t;+    }; -	-- | types of kind @* -> * -> *@ with a representation-	;-	class Typeable2 t where-	{-		rep2 :: Rep2 t;-	};+    -- | types of kind @* -> * -> *@ with a representation+    ;+    class Typeable2 t where+    {+        rep2 :: OpenRep2 t;+    }; -	instance (Typeable1 f,Typeable a) => Typeable (f a) where-	{-		rep = ApplyRep rep1 rep;-	};+    instance (Typeable1 f,Typeable a) => Typeable (f a) where+    {+        rep = ApplyOpenRep rep1 rep;+    }; -	instance (Typeable2 f,Typeable a) => Typeable1 (f a) where-	{-		rep1 = ApplyRep1 rep2 rep;-	};+    instance (Typeable2 f,Typeable a) => Typeable1 (f a) where+    {+        rep1 = ApplyOpenRep1 rep2 rep;+    }; -	instance Typeable2 (->) where-	{-		rep2 = SimpleRep2 witFn where-		{-			witFn :: IOWitness (() -> ()); -- <- newIOWitness;-			witFn = unsafeIOWitnessFromString "Data.OpenWitness.Typeable.witFn";-		};-	};+    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 <- matchWitness rep rep;-		return a;-	};+    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 <- matchWitness rep rep;-		return ca;-	};+    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 Rep;+    -- | represents a type of kind @*@+    ;+    type TypeRep = AnyWitness OpenRep; -	typeOf :: forall t. (Typeable t) => t -> TypeRep;-	typeOf _ = MkAnyWitness (rep :: Rep t);-	-	-- | represents a type of kind @* -> *@-	;-	type TypeRep1 = AnyWitness1 Rep1;+    typeOf :: forall t. (Typeable t) => t -> TypeRep;+    typeOf _ = MkAnyWitness (rep :: OpenRep t); -	typeOf1 :: forall t a. (Typeable1 t) => t a -> TypeRep1;-	typeOf1 _ = MkAnyWitness1 (rep1 :: Rep1 t);-	-	-- | represents a type of kind @* -> * -> *@-	;-	type TypeRep2 = AnyWitness2 Rep2;+    -- | represents a type of kind @* -> *@+    ;+    type TypeRep1 = AnyWitness1 OpenRep1; -	typeOf2 :: forall t a b. (Typeable2 t) => t a b -> TypeRep2;-	typeOf2 _ = MkAnyWitness2 (rep2 :: Rep2 t);-	-	-- | given representations of @a@ and @b@, make a representation of @a -> b@-	;-	mkFunTy :: TypeRep -> TypeRep -> TypeRep;-	mkFunTy (MkAnyWitness ta) (MkAnyWitness tb) = MkAnyWitness (ApplyRep (ApplyRep1 (rep2 :: Rep2 (->)) ta) tb);+    typeOf1 :: forall t a. (Typeable1 t) => t a -> TypeRep1;+    typeOf1 _ = MkAnyWitness1 (rep1 :: OpenRep1 t); -	-- | given representations of @a -> b@ and @a@, make a representation of @b@ (otherwise not)-	;-	funResultTy :: TypeRep -> TypeRep -> Maybe TypeRep;-	funResultTy (MkAnyWitness (ApplyRep (ApplyRep1 repFn' ta') tb')) (MkAnyWitness ta) = do-	{-		MkEqualType <- matchRep2 repFn' (rep2 :: Rep2 (->));-		MkEqualType <- matchWitness ta' ta;-		return (MkAnyWitness tb');-	};-	funResultTy _ _ = Nothing;-	-	mkAppTy :: TypeRep1 -> TypeRep -> TypeRep;-	mkAppTy (MkAnyWitness1 tf) (MkAnyWitness ta) = MkAnyWitness (ApplyRep tf ta);-	-	mkAppTy1 :: TypeRep2 -> TypeRep -> TypeRep1;-	mkAppTy1 (MkAnyWitness2 tf) (MkAnyWitness ta) = MkAnyWitness1 (ApplyRep1 tf ta);+    -- | 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);+-} }

@@ -1,62 +0,0 @@-module Data.OpenWitness.Typeable.Rep where-{-	import Data.Witness;-	import Data.OpenWitness;-	import Data.Maybe;--	data Rep2 p where-	{-		SimpleRep2 :: IOWitness (p () ()) -> Rep2 p;---		ApplyRep2 :: TypeRep3 p -> Rep a -> Rep2 (p a);-	};--	matchRep2 :: Rep2 a -> Rep2 b -> Maybe (EqualType (a () ()) (b () ()));-	matchRep2 (SimpleRep2 wa) (SimpleRep2 wb) = matchWitness wa wb;-{--	matchRep2 (ApplyRep1 tfa ta) (ApplyRep1 tfb tb) = do-	{-		MkEqualType <- matchRep2 tfa tfb;-		MkEqualType <- matchWitness ta tb;-		return MkEqualType;-	};-	matchRep2 _ _ = Nothing;--}-	data Rep1 p where-	{-		SimpleRep1 :: IOWitness (p ()) -> Rep1 p;-		ApplyRep1 :: Rep2 p -> Rep a -> Rep1 (p a);-	};--	matchRep1 :: Rep1 a -> Rep1 b -> Maybe (EqualType (a ()) (b ()));-	matchRep1 (SimpleRep1 wa) (SimpleRep1 wb) = matchWitness wa wb;-	matchRep1 (ApplyRep1 tfa ta) (ApplyRep1 tfb tb) = do-	{-		MkEqualType <- matchRep2 tfa tfb;-		MkEqualType <- matchWitness ta tb;-		return MkEqualType;-	};-	matchRep1 _ _ = Nothing;--	data Rep a where-	{-		SimpleRep :: IOWitness a -> Rep a;-		ApplyRep :: Rep1 p -> Rep a -> Rep (p a);-	};--	instance SimpleWitness Rep where-	{-		matchWitness (SimpleRep wa) (SimpleRep wb) = matchWitness wa wb;-		matchWitness (ApplyRep tfa ta) (ApplyRep tfb tb) = do-		{-			MkEqualType <- matchRep1 tfa tfb;-			MkEqualType <- matchWitness ta tb;-			return MkEqualType;-		};-		matchWitness _ _ = Nothing;-	};--	instance Eq1 Rep where-	{-		equals1 r1 r2 = isJust (matchWitness r1 r2);-	};-}

@@ -1,32 +1,49 @@-name:			open-witness-version:		0.1.1-license:		BSD3-license-file:	LICENSE-author:			Ashley Yakeley <ashley@semantic.org>-maintainer:		Ashley Yakeley <ashley@semantic.org>-build-depends:	base>=2.0, mtl>=1.1, witness==0.1-category:		Data-synopsis:		open witnesses+cabal-version:  >=1.14+name:           open-witness+version:        0.3.1+x-follows-version-policy:+license:        BSD3+license-file:   LICENSE+copyright:      Ashley Yakeley <ashley@semantic.org>+author:         Ashley Yakeley <ashley@semantic.org>+maintainer:     Ashley Yakeley <ashley@semantic.org>+homepage:       https://github.com/AshleyYakeley/open-witness+bug-reports:    https://github.com/AshleyYakeley/open-witness/issues+synopsis:       open witnesses description:-	Open witnesses are witnesses that can witness to any type. However, they cannot be constructed, they can only be generated in the IO monad.+    Open witnesses are witnesses that can witness to any type. However, they cannot be constructed, they can only be generated in the IO monad.+    See the paper /Witnesses and Open Witnesses/ (<http://semantic.org/stuff/Open-Witnesses.pdf>).+category:       Data+build-type:     Simple -	See the paper /Witnesses and Open Witnesses/ (<http://semantic.org/stuff/Open-Witnesses.pdf>).-build-type:		Simple-extensions:-	RankNTypes-	EmptyDataDecls-	GeneralizedNewtypeDeriving-	ScopedTypeVariables-	GADTs-	PatternSignatures-	FlexibleContexts-	FlexibleInstances-	MultiParamTypeClasses-exposed-modules:-	Data.OpenWitness-	Data.OpenWitness.ST-	Data.OpenWitness.Typeable-	Data.OpenWitness.Typeable.Rep-	Data.OpenWitness.Dynamic-	Data.OpenWitness.Exception-other-modules:+library+    hs-source-dirs: .+    default-language: Haskell2010+    default-extensions:+        MultiParamTypeClasses+        RankNTypes+        FlexibleContexts+        TypeOperators+        FlexibleInstances+        EmptyDataDecls+        KindSignatures+        TemplateHaskell+        GeneralizedNewtypeDeriving+        GADTs+        PolyKinds+        ScopedTypeVariables+    build-depends:+        base >= 4.8 && < 5,+        random,+        template-haskell,+        transformers,+        hashable,+        witness >= 0.3+    exposed-modules:+        Data.OpenWitness+        Data.OpenWitness.Dynamic+        Data.OpenWitness.Exception+        Data.OpenWitness.OpenRep+        Data.OpenWitness.ST+        Data.OpenWitness.Typeable+    ghc-options: -Wall