packages feed

open-witness (empty) → 0.1

raw patch · 8 files changed

+413/−0 lines, 8 filesdep +basedep +mtldep +witnesssetup-changed

Dependencies added: base, mtl, witness

Files

+ Data/OpenWitness.hs view
@@ -0,0 +1,89 @@+module Data.OpenWitness+(+	OpenWitness,+	RealWorld,IOWitness,newIOWitness,+	OW,newOpenWitnessOW,runOW,owToIO,+--	unsafeIOWitnessFromInteger,+	unsafeIOWitnessFromString+) where+{+	import Data.Witness;+	import Unsafe.Coerce;+	import System.IO.Unsafe (unsafePerformIO);+	import Control.Concurrent.MVar;+	import Control.Monad.State;+	import Data.HashTable;++	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;+	};++	-- | The @s@ type for running 'OW' in 'IO'.+	;+	data RealWorld;++	-- | 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,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;+}
+ Data/OpenWitness/Dynamic.hs view
@@ -0,0 +1,53 @@+-- | This is an approximate re-implementation of "Data.Dynamic" using open witnesses.+module Data.OpenWitness.Dynamic where+{+	import Data.Witness;+	import Data.OpenWitness.Typeable;++	-- * The @Dynamic@ type+	;++	type Dynamic = Any Rep;++	-- * Converting to and from @Dynamic@+	;++	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;+	};++	fromDynamic :: forall a. Typeable a => Dynamic -> Maybe a;+	fromDynamic (MkAny uq a) = do+	{+		MkEqualType <- matchWitness uq (rep :: Rep a);+		return a;+	};++	-- * 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;++	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;+}
+ Data/OpenWitness/ST.hs view
@@ -0,0 +1,57 @@+-- | 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+) where+{+	import Data.OpenWitness;+	import Data.Witness.WitnessDict;+	import Control.Monad.State;+	+	type ST s = StateT (WitnessDict (OpenWitness s)) (OW s);++	stToOW :: ST s a -> OW s a;+	stToOW st = evalStateT st emptyWitnessDict;++	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;+}
+ Data/OpenWitness/Typeable.hs view
@@ -0,0 +1,109 @@+-- | 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+{+	import Data.OpenWitness.Typeable.Rep;+	import Data.OpenWitness;+	import Data.Witness;+	import Data.Maybe;++	-- | types of kind @*@ with a representation+	;+	class Typeable a where+	{+		rep :: Rep a;+	};++	-- | types of kind @* -> *@ with a representation+	;+	class Typeable1 t where+	{+		rep1 :: Rep1 t;+	};++	-- | types of kind @* -> * -> *@ with a representation+	;+	class Typeable2 t where+	{+		rep2 :: Rep2 t;+	};++	instance (Typeable1 f,Typeable a) => Typeable (f a) where+	{+		rep = ApplyRep rep1 rep;+	};++	instance (Typeable2 f,Typeable a) => Typeable1 (f a) where+	{+		rep1 = ApplyRep1 rep2 rep;+	};++	instance Typeable2 (->) where+	{+		rep2 = SimpleRep2 witFn where+		{+			witFn :: IOWitness (() -> ()); -- <- newIOWitness;+			witFn = unsafeIOWitnessFromString "Data.OpenWitness.Typeable.witFn";+		};+	};++	cast :: forall a b. (Typeable a,Typeable b) => a -> Maybe b;+	cast a = do+	{+		MkEqualType :: EqualType a b <- matchWitness 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;+	};++	-- | represents a type of kind @*@+	;+	type TypeRep = AnyWitness Rep;++	typeOf :: forall t. (Typeable t) => t -> TypeRep;+	typeOf _ = MkAnyWitness (rep :: Rep t);+	+	-- | represents a type of kind @* -> *@+	;+	type TypeRep1 = AnyWitness1 Rep1;++	typeOf1 :: forall t a. (Typeable1 t) => t a -> TypeRep1;+	typeOf1 _ = MkAnyWitness1 (rep1 :: Rep1 t);+	+	-- | represents a type of kind @* -> * -> *@+	;+	type TypeRep2 = AnyWitness2 Rep2;++	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);++	-- | 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);+}
+ Data/OpenWitness/Typeable/Rep.hs view
@@ -0,0 +1,62 @@+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);+	};+}
+ LICENSE view
@@ -0,0 +1,10 @@+open-witness is Copyright (c) Ashley Yakeley, 2007-2008.+All rights reserved.++Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:++- Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.++- Neither name of the copyright holders nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ open-witness.cabal view
@@ -0,0 +1,31 @@+name:			open-witness+version:		0.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+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.++	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+other-modules: