packages feed

witness 0.2 → 0.3

raw patch · 19 files changed

+750/−538 lines, 19 filesdep +categoriesdep +constraintsdep +transformersdep −mtl

Dependencies added: categories, constraints, transformers

Dependencies removed: mtl

Files

− Data/Witness.hs 
@@ -1,33 +0,0 @@-module Data.Witness-(-	module Data.Witness.WitnessDict,-	module Data.Witness.WitnessFDict,-	module Data.Witness.Any,-	module Data.Witness.Representative,-	module Data.Witness.Type,-	module Data.Witness.SimpleWitness,-	module Data.Witness.EqualType,-	module Data.Witness.Nat,-	module Data.Witness.List,-	module Data.Witness-) where-{-	import Data.Witness.List;-	import Data.Witness.Nat;-	import Data.Witness.EqualType;-	import Data.Witness.SimpleWitness;-	import Data.Witness.Type;-	import Data.Witness.Representative;-	import Data.Witness.Any;-	import Data.Witness.WitnessFDict;-	import Data.Witness.WitnessDict;--	-- | See whether two represented and witnessed types are the same.-	;-	matchIs :: (SimpleWitness w,Is w a,Is w b) => Type (w ()) -> Maybe (EqualType a b);-	matchIs t = matchWitness (foo t) (foo t) where-	{-		foo :: (Is w a) => Type (w ()) -> w a;-		foo _ = representative;-	};-}
− Data/Witness/Any.hs 
@@ -1,56 +0,0 @@-module Data.Witness.Any where-{-	import Data.Witness.SimpleWitness;-	import Data.Witness.EqualType;-	import Data.Maybe;--	-- | Any value with a witness to it.-	;-	data Any w = forall a. MkAny (w a) a;-	-	matchAny :: (SimpleWitness w) => w a -> Any w -> Maybe a;-	matchAny wit (MkAny cwit ca) = do-	{-		MkEqualType <- matchWitness cwit wit;-		return ca;-	};--	-- | Any value with a witness to a parameter of its type.-	;-	data AnyF w f = forall a. MkAnyF (w a) (f a);-	-	matchAnyF :: (SimpleWitness w) => w a -> AnyF w f -> Maybe (f a);-	matchAnyF wit (MkAnyF cwit cfa) = do-	{-		MkEqualType <- matchWitness cwit wit;-		return cfa;-	};--	-- | Any value with a witness to a parameter of its type of kind @* -> *@.-	;-	data AnyF1 w f = forall (a :: * -> *). MkAnyF1 (w a) (f a);--	-- | Any value with a witness to a parameter of its type of kind @* -> * -> *@.-	;-	data AnyF2 w f = forall (a :: * -> * -> *). MkAnyF2 (w a) (f a);--	-- | Any witness.-	;-	data AnyWitness w = forall a. MkAnyWitness (w a);-	-	matchAnyWitness :: (SimpleWitness w) => w a -> AnyWitness w -> Bool;-	matchAnyWitness wit (MkAnyWitness cwit) = isJust (matchWitness cwit wit);--	instance (SimpleWitness w) => Eq (AnyWitness w) where-	{-		(==) (MkAnyWitness wa) = matchAnyWitness wa;-	};--	-- | Any witness of a type of kind @* -> *@.-	;-	data AnyWitness1 w = forall (a :: * -> *). MkAnyWitness1 (w a);--	-- | Any witness of a type of kind @* -> * -> *@.-	;-	data AnyWitness2 w = forall (a :: * -> * -> *). MkAnyWitness2 (w a);-}
− Data/Witness/EqualType.hs 
@@ -1,17 +0,0 @@-module Data.Witness.EqualType where-{-	import Control.Category;--	-- | witness that type parameters @a@ and @b@ are the same type-	;-	data EqualType a b where-	{-		MkEqualType :: EqualType t t;-	};--	instance Category EqualType where-	{-		id = MkEqualType;-		MkEqualType . MkEqualType = MkEqualType;-	};-}
− Data/Witness/List.hs 
@@ -1,86 +0,0 @@-module Data.Witness.List where-{-	import Data.Witness.Nat;-	import Data.Witness.Representative;-	import Data.Witness.SimpleWitness;-	import Data.Witness.EqualType;-	import Control.Category;-	import Prelude hiding (id,(.));--	-- | a witness type for HList-style lists. Here we use @()@ and @(,)@ for @HNil@ and @HCons@. -	-- The @w@ parameter is the witness type of the elements.-	;-	data ListType w a where-	{-		NilListType :: ListType w ();-		ConsListType :: w a -> ListType w b -> ListType w (a,b);-	};--	instance Eq1 w => Eq1 (ListType w) where-	{-		equals1 NilListType NilListType = True;-		equals1 (ConsListType pe pl) (ConsListType qe ql) = (equals1 pe qe) && (equals1 pl ql);-		equals1 _ _ = False;-	};--	instance Eq1 w => Eq (ListType w a) where-	{-		(==) = equals1;-	};--	instance (Representative w) => Representative (ListType w) where-	{-		getRepWitness NilListType = MkRepWitness;-		getRepWitness (ConsListType w lw) = case (getRepWitness w,getRepWitness lw) of-		{-			(MkRepWitness,MkRepWitness) -> MkRepWitness;-		};-	};--	instance (Representative w) => Is (ListType w) () where-	{-		representative = NilListType;-	};--	instance (Is w a,Is (ListType w) b) => Is (ListType w) (a,b) where-	{-		representative = ConsListType representative representative;-	};--	instance (SimpleWitness w) => SimpleWitness (ListType w) where-	{-		matchWitness NilListType NilListType = Just id;-		matchWitness (ConsListType wpa wpb) (ConsListType wqa wqb) = do-		{-			MkEqualType <- matchWitness wpa wqa;-			MkEqualType <- matchWitness wpb wqb;-			return MkEqualType;-		};-		matchWitness _ _ = Nothing;-	};---    class HasListElement n list where-    {-        type ListElement n list :: *;-        getListElement :: Nat n -> list -> ListElement n list;-        putListElement :: Nat n -> ListElement n list -> list -> list;-    };--    modifyListElement :: (HasListElement n t) => Nat n -> (ListElement n t -> ListElement n t) -> t -> t;-    modifyListElement n aa t = putListElement n (aa (getListElement n t)) t;--    instance HasListElement Zero (a,r) where-    {-        type ListElement Zero (a,r) = a;-        getListElement _ (a,_) = a;-        putListElement _ a (_,r) = (a,r);-    };--    instance (HasListElement n r) => HasListElement (Succ n) (a,r) where-    {-        type ListElement (Succ n) (a,r) = ListElement n r;-        getListElement (SuccNat n) (_,r) = getListElement n r;-        putListElement (SuccNat n) a (f,r) = (f,putListElement n a r);-    };-}
− Data/Witness/Nat.hs 
@@ -1,53 +0,0 @@-module Data.Witness.Nat where-{-	import Data.Witness.Representative;-	import Data.Witness.SimpleWitness;-	import Data.Witness.EqualType;-	import Data.Maybe;-	import Prelude hiding (id,(.));--    data Zero;-    -    data Succ n;-    -    data Nat t where-    {-        ZeroNat :: Nat Zero;-        SuccNat :: Nat t -> Nat (Succ t);-    };--    instance SimpleWitness Nat where-    {-        matchWitness ZeroNat ZeroNat = return MkEqualType;-        matchWitness (SuccNat a) (SuccNat b) = do-        {-            MkEqualType <- matchWitness a b;-            return MkEqualType;-        };-        matchWitness _ _ = Nothing;-    };--    instance Eq1 Nat where-    {-        equals1 a b = isJust (matchWitness a b);-    };--    instance Representative Nat where-    {-        getRepWitness ZeroNat = MkRepWitness;-        getRepWitness (SuccNat n) = case getRepWitness n of-        {-            MkRepWitness -> MkRepWitness;-        };-    };--    instance Is Nat Zero where-    {-        representative = ZeroNat;-    };--    instance (Is Nat n) => Is Nat (Succ n) where-    {-        representative = SuccNat representative;-    };-}
− Data/Witness/Representative.hs 
@@ -1,72 +0,0 @@-module Data.Witness.Representative where-{-	import Data.Witness.Any;-	import Data.Witness.SimpleWitness;--	class Eq1 p where-	{-		equals1 :: forall a. p a -> p a -> Bool;-	};--	data RepWitness rep a where-	{-		MkRepWitness :: (Is rep a) => RepWitness rep a;-	};--	isWitnessRepresentative :: RepWitness rep a -> rep a;-	isWitnessRepresentative MkRepWitness = representative;--	instance (SimpleWitness w) => SimpleWitness (RepWitness w) where-	{-		matchWitness wa wb = matchWitness (isWitnessRepresentative wa) (isWitnessRepresentative wb);-	};--	class Eq1 rep => Representative rep where-	{-		-- | Every value is an instance of 'Is'.-		;-		getRepWitness :: rep a -> RepWitness rep a;-	};--	withRepresentative :: forall rep r. (Representative rep) => (forall a. (Is rep a) => rep a -> r) -> (forall b. rep b -> r);-	withRepresentative foo rep = case getRepWitness rep of-	{-		MkRepWitness -> foo rep;-	};--	-- | If two representatives have the same type, then they have the same value.-	;-	class Representative rep => Is rep a where-	{-		-- | The representative value for type @a@.-		;-		representative :: rep a;-	};--	getRepresentative :: (Is rep a) => a -> rep a;-	getRepresentative _ = representative;--	rerepresentative :: (Is rep a) => p a -> rep a;-	rerepresentative _ = representative;--	mkAny :: (Is rep a) => a -> Any rep;-	mkAny a = MkAny representative a;--	mkAnyF :: (Is rep a) => f a -> AnyF rep f;-	mkAnyF fa = MkAnyF representative fa;--	instance Eq1 (RepWitness rep) where-	{-		equals1 MkRepWitness MkRepWitness = True;-	};--	instance Representative (RepWitness rep) where-	{-		getRepWitness MkRepWitness = MkRepWitness;-	};--	instance (Is rep a) => Is (RepWitness rep) a where-	{-		representative = MkRepWitness;-	};-}
− Data/Witness/SimpleWitness.hs 
@@ -1,15 +0,0 @@-module Data.Witness.SimpleWitness where-{-	import Data.Witness.EqualType;--	-- | @w@ is a simple witness type if each value witnesses to a single type. Thus if two values are the same, then they have the same type.-	;-	class SimpleWitness w where-	{-		-- | If the two values are the same, then @a@ and @b@ are the same type.-		---		-- As an equivalence relation, 'matchWitness' must be reflexive, commutative, and transitive.-		;-		matchWitness :: w a -> w b -> Maybe (EqualType a b);-	};-}
− Data/Witness/Type.hs 
@@ -1,28 +0,0 @@-module Data.Witness.Type where-{-	import Data.Witness.Representative;--	-- | The simplest 'Representative', with one value that represents all types.-	;-	data Type a = Type;--	instance Eq1 Type where-	{-		equals1 Type Type = True;-	};--	instance Eq (Type a) where-	{-		(==) = equals1;-	};--	instance Representative Type where-	{-		getRepWitness Type = MkRepWitness;-	};--	instance Is Type a where-	{-		representative = Type;-	};-}
− Data/Witness/WitnessDict.hs 
@@ -1,63 +0,0 @@-module Data.Witness.WitnessDict where-{-	import Data.Witness.Any;-	import Data.Witness.SimpleWitness;-	import Data.Maybe;-	-	-- | A dictionary that is heterogenous up to its simple witness type @w@. -	-- Witnesses are the keys of the dictionary, and the values they witness are the values of the dictionary.-	;-	newtype WitnessDict w = MkWitnessDict [Any w];-	-	-- | An empty dictionary.-	;-	emptyWitnessDict :: WitnessDict w;-	emptyWitnessDict = MkWitnessDict[];-	-	-- | Look up the first value in the dictionary that matches the given witness.-	;-	witnessDictLookup :: (SimpleWitness w) => w a -> WitnessDict w -> Maybe a;-	witnessDictLookup wit (MkWitnessDict cells) = listToMaybe (mapMaybe (matchAny wit) cells);-	-	-- | Modify the first value in the dictionary that matches a particular witness.-	;-	witnessDictModify :: (SimpleWitness w) => w a -> (a -> a) -> WitnessDict w -> WitnessDict w;-	witnessDictModify wit amap (MkWitnessDict cells) = MkWitnessDict -		(replaceFirst ((fmap ((MkAny wit) . amap)) . (matchAny wit)) cells) where-	{-		replaceFirst :: (a -> Maybe a) -> [a] -> [a];-		replaceFirst ama (a:aa) = case ama a of-		{-			Just newa -> (newa:aa);-			_ -> a : (replaceFirst ama aa);-		};-		replaceFirst _ _ = [];-	};--	-- | Replace the first value in the dictionary that matches the witness-	;-	witnessDictReplace :: (SimpleWitness w) => w a -> a -> WitnessDict w -> WitnessDict w;-	witnessDictReplace wit newa = witnessDictModify wit (const newa);-	-	-- | Add a witness and value as the first entry in the dictionary.-	;-	witnessDictAdd :: w a -> a -> WitnessDict w -> WitnessDict w;-	witnessDictAdd wit a (MkWitnessDict cells) = MkWitnessDict ((MkAny wit a):cells);-	-	-- | Remove the first entry in the dictionary that matches the given witness.-	;-	witnessDictRemove :: (SimpleWitness w) => w a -> WitnessDict w -> WitnessDict w;-	witnessDictRemove wit (MkWitnessDict cells) = MkWitnessDict -		(removeFirst (\(MkAny cwit _) -> isJust (matchWitness wit cwit)) cells) where-	{-		removeFirst :: (a -> Bool) -> [a] -> [a];-		removeFirst p (a:as) | p a = as;-		removeFirst p (a:as) = a : (removeFirst p as);-		removeFirst _ _ = [];-	};-	-	-- | Create a dictionary from a list of witness\/value pairs-	;-	witnessDictFromList :: (SimpleWitness w) => [Any w] -> WitnessDict w;-	witnessDictFromList = MkWitnessDict;-}
− Data/Witness/WitnessFDict.hs 
@@ -1,63 +0,0 @@-module Data.Witness.WitnessFDict where-{-	import Data.Witness.Any;-	import Data.Witness.SimpleWitness;-	import Data.Maybe;-	-	-- | A dictionary that is heterogenous up to its simple witness type @w@. -	-- Witnesses are the keys of the dictionary, and the values they witness are the values of the dictionary.-	;-	newtype WitnessFDict w f = MkWitnessFDict [AnyF w f];-	-	-- | An empty dictionary.-	;-	emptyWitnessFDict :: WitnessFDict w f;-	emptyWitnessFDict = MkWitnessFDict [];-	-	-- | Look up the first value in the dictionary that matches the given witness.-	;-	witnessFDictLookup :: (SimpleWitness w) => w a -> WitnessFDict w f -> Maybe (f a);-	witnessFDictLookup wit (MkWitnessFDict cells) = listToMaybe (mapMaybe (matchAnyF wit) cells);-	-	-- | Modify the first value in the dictionary that matches a particular witness.-	;-	witnessFDictModify :: (SimpleWitness w) => w a -> (f a -> f a) -> WitnessFDict w f -> WitnessFDict w f;-	witnessFDictModify wit amap (MkWitnessFDict cells) = MkWitnessFDict -		(replaceFirst ((fmap ((MkAnyF wit) . amap)) . (matchAnyF wit)) cells) where-	{-		replaceFirst :: (a -> Maybe a) -> [a] -> [a];-		replaceFirst ama (a:aa) = case ama a of-		{-			Just newa -> (newa:aa);-			_ -> a : (replaceFirst ama aa);-		};-		replaceFirst _ _ = [];-	};--	-- | Replace the first value in the dictionary that matches the witness-	;-	witnessFDictReplace :: (SimpleWitness w) => w a -> f a -> WitnessFDict w f -> WitnessFDict w f;-	witnessFDictReplace wit newfa = witnessFDictModify wit (const newfa);-	-	-- | Add a witness and value as the first entry in the dictionary.-	;-	witnessFDictAdd :: w a -> f a -> WitnessFDict w f -> WitnessFDict w f;-	witnessFDictAdd wit fa (MkWitnessFDict cells) = MkWitnessFDict ((MkAnyF wit fa):cells);-	-	-- | Remove the first entry in the dictionary that matches the given witness.-	;-	witnessFDictRemove :: (SimpleWitness w) => w a -> WitnessFDict w f -> WitnessFDict w f;-	witnessFDictRemove wit (MkWitnessFDict cells) = MkWitnessFDict -		(removeFirst (\(MkAnyF cwit _) -> isJust (matchWitness wit cwit)) cells) where-	{-		removeFirst :: (a -> Bool) -> [a] -> [a];-		removeFirst p (a:as) | p a = as;-		removeFirst p (a:as) = a : (removeFirst p as);-		removeFirst _ _ = [];-	};-	-	-- | Create a dictionary from a list of witness\/value pairs-	;-	witnessFDictFromList :: (SimpleWitness w) => [AnyF w f] -> WitnessFDict w f;-	witnessFDictFromList = MkWitnessFDict;-}
+ src/Data/Witness.hs view
@@ -0,0 +1,33 @@+module Data.Witness+(+    module Data.Proxy,+    module Data.Type.Equality,+    module Data.Witness.Any,+    module Data.Witness.WitnessDict,+    module Data.Witness.WitnessFDict,+    module Data.Witness.Nat,+    module Data.Witness.ListElement,+    module Data.Witness.List,+    module Data.Witness.Representative,+    module Data.Witness+) where+{+    import Data.Proxy;+    import Data.Type.Equality;+    import Data.Witness.Any;+    import Data.Witness.WitnessDict;+    import Data.Witness.WitnessFDict;+    import Data.Witness.Nat;+    import Data.Witness.ListElement;+    import Data.Witness.List;+    import Data.Witness.Representative;++    -- | See whether two represented and witnessed types are the same.+    ;+    matchIs :: forall w a b. (TestEquality w,Is w a,Is w b) => Proxy w -> Maybe (a :~: b);+    matchIs _ = testEquality r r where+    {+        r :: forall t. (Is w t) => w t;+        r = representative;+    };+}
+ src/Data/Witness/Any.hs view
@@ -0,0 +1,39 @@+module Data.Witness.Any where+{+    import Data.Maybe;+    import Data.Type.Equality;++    -- | Any value with a witness to it.+    ;+    data Any (w :: * -> *) = forall (a :: *). MkAny (w a) a;++    matchAny :: (TestEquality w) => w a -> Any w -> Maybe a;+    matchAny wit (MkAny cwit ca) = do+    {+        Refl <- testEquality cwit wit;+        return ca;+    };++    -- | Any value with a witness to a parameter of its type.+    ;+    data AnyF (w :: k -> *) (f :: k -> *) = forall (a :: k). MkAnyF (w a) (f a);++    matchAnyF :: (TestEquality w) => w a -> AnyF w f -> Maybe (f a);+    matchAnyF wit (MkAnyF cwit cfa) = do+    {+        Refl <- testEquality cwit wit;+        return cfa;+    };++    -- | Any witness.+    ;+    data AnyWitness (w :: k -> *) = forall (a :: k). MkAnyWitness (w a);++    matchAnyWitness :: (TestEquality w) => w a -> AnyWitness w -> Bool;+    matchAnyWitness wit (MkAnyWitness cwit) = isJust (testEquality cwit wit);++    instance (TestEquality w) => Eq (AnyWitness w) where+    {+        (==) (MkAnyWitness wa) = matchAnyWitness wa;+    };+}
+ src/Data/Witness/List.hs view
@@ -0,0 +1,358 @@+module Data.Witness.List where+{+    import Prelude hiding (id,(.));+    import Data.Witness.Representative;+    import Data.Type.Equality;+    import Control.Category.Dual;+    import Data.Constraint(Dict(..));+    import Control.Applicative;+    import Control.Category;+    import Data.Functor.Identity as Import;++    -- | a witness type for HList-style lists.+    -- The @w@ parameter is the witness type of the elements.+    ;+    data ListType (w :: * -> *) (lt :: *) where+    {+        NilListType :: ListType w ();+        ConsListType :: w a -> ListType w lt -> ListType w (a,lt);+    };++    instance Eq1 w => Eq1 (ListType w) where+    {+        equals1 NilListType NilListType = True;+        equals1 (ConsListType pe pl) (ConsListType qe ql) = (equals1 pe qe) && (equals1 pl ql);+        equals1 _ _ = False;+    };++    instance Eq1 w => Eq (ListType w a) where+    {+        (==) = equals1;+    };++    instance (Representative w) => Representative (ListType w) where+    {+        getRepWitness NilListType = Dict;+        getRepWitness (ConsListType w lw) = case (getRepWitness w,getRepWitness lw) of+        {+            (Dict,Dict) -> Dict;+        };+    };++    instance (Representative w) => Is (ListType w) () where+    {+        representative = NilListType;+    };++    instance (Is w a,Is (ListType w) lt) => Is (ListType w) (a,lt) where+    {+        representative = ConsListType representative representative;+    };++    instance (TestEquality w) => TestEquality (ListType w) where+    {+        testEquality NilListType NilListType = Just Refl;+        testEquality (ConsListType wpa wpb) (ConsListType wqa wqb) = do+        {+            Refl <- testEquality wpa wqa;+            Refl <- testEquality wpb wqb;+            return Refl;+        };+        testEquality _ _ = Nothing;+    };++    listFill :: ListType w t -> (forall a. w a -> a) -> t;+    listFill NilListType _f = ();+    listFill (ConsListType wa wr) f = (f wa,listFill wr f);++    listMap :: ListType w t -> (forall a. w a -> a -> a) -> t -> t;+    listMap NilListType _f () = ();+    listMap (ConsListType wa wr) f (a,rest) = (f wa a,listMap wr f rest);++    listLift2 :: ListType w t -> (forall a. w a -> a -> a -> a) -> t -> t -> t;+    listLift2 NilListType _f () () = ();+    listLift2 (ConsListType wa wr) f (a,resta) (b,restb) = (f wa a b,listLift2 wr f resta restb);++    listTypeToList :: (forall a. w a -> r) -> ListType w t -> [r];+    listTypeToList _wr NilListType = [];+    listTypeToList wr (ConsListType wa rest) = (wr wa):(listTypeToList wr rest);++    listTypeMap :: (forall a. w1 a -> w2 a) -> ListType w1 t -> ListType w2 t;+    listTypeMap _ww NilListType = NilListType;+    listTypeMap ww (ConsListType wa rest) = ConsListType (ww wa) (listTypeMap ww rest);++    listIdentity :: ListType Identity lt -> lt;+    listIdentity NilListType = ();+    listIdentity (ConsListType (Identity a) rest) = (a,listIdentity rest);++    listSequence ::  (Applicative f) => ListType f lt -> f lt;+    listSequence NilListType = pure ();+    listSequence (ConsListType fa rest) = liftA2 (,) fa (listSequence rest);++    data AppendList w la lb = forall lr. MkAppendList+    {+        listAppendWitness :: ListType w lr,+        listAppend :: la -> lb -> lr,+        listSplit :: lr -> (la,lb)+    };++    appendList :: ListType w la -> ListType w lb -> AppendList w la lb;+    appendList NilListType wlb = MkAppendList+    {+        listAppendWitness = wlb,+        listAppend = \() lb -> lb,+        listSplit = \lb -> ((),lb)+    };+    appendList (ConsListType wa wla) wlb = case appendList wla wlb of+    {+        MkAppendList wit join split -> MkAppendList+        {+            listAppendWitness = ConsListType wa wit,+            listAppend = \(a,la) lb -> (a,join la lb),+            listSplit = \(a,lab) -> case split lab of+            {+                (la,lb) -> ((a,la),lb);+            }+        };+    };++    data AddItemList w a l = forall lr. MkAddItemList+    {+        listAddItemWitness :: ListType w lr,+        listAddItem :: a -> l -> lr,+        listSplitItem :: lr -> (a,l)+    };++    addListItem :: w a -> ListType w l -> AddItemList w a l;+    addListItem wa wl = MkAddItemList+    {+        listAddItemWitness = ConsListType wa wl,+        listAddItem = (,),+        listSplitItem = id+    };++    data MergeItemList w a l = forall lr. MkMergeItemList+    {+        listMergeItemWitness :: ListType w lr,+        listMergeItem :: (Maybe a -> a) -> l -> lr,+        listUnmergeItem :: lr -> (a,l)+    };++    mergeListItem :: (TestEquality w) => ListType w l -> w a -> MergeItemList w a l;+    mergeListItem NilListType wa = MkMergeItemList+    {+        listMergeItemWitness = ConsListType wa NilListType,+        listMergeItem = \maa () -> (maa Nothing,()),+        listUnmergeItem = id+    };+    mergeListItem wl@(ConsListType wa' _) wa | Just Refl <- testEquality wa wa' = MkMergeItemList+    {+        listMergeItemWitness = wl,+        listMergeItem = \maa (a,l) -> (maa (Just a),l),+        listUnmergeItem = \(a,l) -> (a,(a,l))+    };+    mergeListItem (ConsListType wa' wl) wa = case mergeListItem wl wa of+    {+        MkMergeItemList wit merge unmerge -> MkMergeItemList+        {+            listMergeItemWitness = ConsListType wa' wit,+            listMergeItem = \maa (a',l) -> (a',merge maa l),+            listUnmergeItem = \(a',l') -> case unmerge l' of+            {+                (a,l) -> (a,(a',l));+            }+        };+    };++    data MergeList w la lb = forall lr. MkMergeList+    {+        listMergeWitness :: ListType w lr,+        listMerge :: (forall t. w t -> t -> t -> t) -> la -> lb -> lr,+        listUnmerge :: lr -> (la,lb)+    };++    mergeList :: (TestEquality w) => ListType w la -> ListType w lb -> MergeList w la lb;+    mergeList wla NilListType = MkMergeList+    {+        listMergeWitness = wla,+        listMerge = \_ la () -> la,+        listUnmerge = \la -> (la,())+    };+    mergeList wla (ConsListType wb wlb) = case mergeListItem wla wb of+    {+        MkMergeItemList wla' mergeItem unmergeItem -> case mergeList wla' wlb of+        {+            MkMergeList wlr merge unmerge -> MkMergeList+            {+                listMergeWitness = wlr,+                listMerge = \f la (b,lb) -> merge f (mergeItem (\mb' -> case mb' of+                {+                    Just b' -> f wb b' b;+                    Nothing -> b;+                }) la) lb,+                listUnmerge = \lr -> case unmerge lr of+                {+                    (la',lb) -> case unmergeItem la' of+                    {+                        (b,la) -> (la,(b,lb));+                    };+                }+            };+        };+    };++    -- could use data-lens:Control.Category.Product(Tensor)+    class Tensor cc where+    {+        tensorUnit :: cc () ();+        tensorPair :: cc a1 b1 -> cc a2 b2 -> cc (a1,a2) (b1,b2);+    };++    instance Tensor (->) where+    {+        tensorUnit = id;+        tensorPair ab1 ab2 (a1,a2) = (ab1 a1,ab2 a2);+    };++    instance (Tensor cc) => Tensor (Dual cc) where+    {+        tensorUnit = Dual tensorUnit;+        tensorPair (Dual ab1) (Dual ab2) = Dual (tensorPair ab1 ab2);+    };++    type MapWitness cc w1 w2 = forall r v1. w1 v1 -> (forall v2. w2 v2 -> (cc v1 v2) -> r) -> r;++    sameMapWitness :: (forall v. w v -> cc v v) -> MapWitness cc w w;+    sameMapWitness wc w wcr = wcr w (wc w);++    data MapList cc w2 l = forall lr. MkMapList+    {+        listMapWitness :: ListType w2 lr,+        listMapW :: cc l lr+    };++    mapList :: (Tensor cc) => MapWitness cc w1 w2 -> ListType w1 l -> MapList cc w2 l;+    mapList _ NilListType = MkMapList+    {+        listMapWitness = NilListType,+        listMapW = tensorUnit+    };+    mapList mapwit (ConsListType w rest) = case mapList mapwit rest of+    {+        MkMapList wit listMapW' -> mapwit w (\w' vmap -> MkMapList+        {+            listMapWitness = ConsListType w' wit,+            listMapW = tensorPair vmap listMapW'+        });+    };++    data RemoveFromList w a l = forall lr. MkRemoveFromList+    {+        listRemoveWitness :: ListType w lr,+        listInsert :: a -> lr -> l,+        listRemove :: l -> lr+    };++    removeAllMatching :: (TestEquality w) => w a -> ListType w l -> RemoveFromList w a l;+    removeAllMatching _ NilListType = MkRemoveFromList+    {+        listRemoveWitness = NilListType,+        listInsert = \_ -> id,+        listRemove = id+    };+    removeAllMatching wa (ConsListType wb rest) = case removeAllMatching wa rest of+    {+        MkRemoveFromList wit ins rm -> case testEquality wa wb of+        {+            Just Refl -> MkRemoveFromList+            {+                listRemoveWitness = wit,+                listInsert = \a l2 -> (a,ins a l2),+                listRemove = \(_,l1) -> rm l1+            };+            Nothing -> MkRemoveFromList+            {+                listRemoveWitness = ConsListType wb wit,+                listInsert = \a (b,l2) -> (b,ins a l2),+                listRemove = \(b,l1) -> (b,rm l1)+            };+        };+    };++    data RemoveManyFromList wit lx l = forall lr. MkRemoveManyFromList+    {+        listRemoveManyWitness :: ListType wit lr,+        listInsertMany :: lx -> lr -> l,+        listRemoveMany :: l -> lr+    };++    removeAllMatchingMany :: (TestEquality wit) => ListType wit lx -> ListType wit l -> RemoveManyFromList wit lx l;+    removeAllMatchingMany NilListType wl = MkRemoveManyFromList+    {+        listRemoveManyWitness = wl,+        listInsertMany = \_ lr -> lr,+        listRemoveMany = \l -> l+    };+    removeAllMatchingMany (ConsListType wa wlx) wl = case removeAllMatching wa wl of+    {+        MkRemoveFromList wl' ins rm -> case removeAllMatchingMany wlx wl' of+        {+            MkRemoveManyFromList wl'' insM remM -> MkRemoveManyFromList+            {+                listRemoveManyWitness = wl'',+                listInsertMany = \(a,lx) lr -> ins a (insM lx lr),+                listRemoveMany = remM . rm+            };+        };+    };++    newtype EitherWitness (w1 :: k -> *) (w2 :: k -> *) (a :: k) = MkEitherWitness (Either (w1 a) (w2 a));++    instance (TestEquality w1,TestEquality w2) => TestEquality (EitherWitness w1 w2) where+    {+        testEquality (MkEitherWitness (Left wa)) (MkEitherWitness (Left wb)) = testEquality wa wb;+        testEquality (MkEitherWitness (Right wa)) (MkEitherWitness (Right wb)) = testEquality wa wb;+        testEquality _ _ = Nothing;+    };++    data PartitionList wit1 wit2 l = forall l1 l2. MkPartitionList+    {+        listPartitionWitness1 :: ListType wit1 l1,+        listPartitionWitness2 :: ListType wit2 l2,+        listFromPartition :: l1 -> l2 -> l,+        listToPartition1 :: l -> l1,+        listToPartition2 :: l -> l2+    };++    partitionList :: ListType (EitherWitness w1 w2) l -> PartitionList w1 w2 l;+    partitionList NilListType = MkPartitionList+    {+        listPartitionWitness1 = NilListType,+        listPartitionWitness2 = NilListType,+        listFromPartition = \() () -> (),+        listToPartition1 = \() -> (),+        listToPartition2 = \() -> ()+    };+    partitionList (ConsListType (MkEitherWitness (Left w1a)) rest) = case partitionList rest of+    {+        MkPartitionList pw1 pw2 fp tp1 tp2 -> MkPartitionList+        {+            listPartitionWitness1 = ConsListType w1a pw1,+            listPartitionWitness2 = pw2,+            listFromPartition = \(a,l1) l2 -> (a,fp l1 l2),+            listToPartition1 = \(a,l) -> (a,tp1 l),+            listToPartition2 = \(_,l) -> tp2 l+        };+    };+    partitionList (ConsListType (MkEitherWitness (Right w2a)) rest) = case partitionList rest of+    {+        MkPartitionList pw1 pw2 fp tp1 tp2 -> MkPartitionList+        {+            listPartitionWitness1 = pw1,+            listPartitionWitness2 = ConsListType w2a pw2,+            listFromPartition = \l1 (a,l2) -> (a,fp l1 l2),+            listToPartition1 = \(_,l) -> tp1 l,+            listToPartition2 = \(a,l) -> (a,tp2 l)+        };+    };+}
+ src/Data/Witness/ListElement.hs view
@@ -0,0 +1,28 @@+module Data.Witness.ListElement where+{+    import Data.Witness.Nat;++    class HasListElement (n :: NatKind) (list :: *) where+    {+        type ListElement n list :: *;+        getListElement :: Nat n -> list -> ListElement n list;+        putListElement :: Nat n -> ListElement n list -> list -> list;+    };++    modifyListElement :: (HasListElement n t) => Nat n -> (ListElement n t -> ListElement n t) -> t -> t;+    modifyListElement n aa t = putListElement n (aa (getListElement n t)) t;++    instance HasListElement Zero (a,r) where+    {+        type ListElement Zero (a,r) = a;+        getListElement _ (a,_) = a;+        putListElement _ a (_,r) = (a,r);+    };++    instance (HasListElement n r) => HasListElement (Succ n) (a,r) where+    {+        type ListElement (Succ n) (a,r) = ListElement n r;+        getListElement (SuccNat n) (_,r) = getListElement n r;+        putListElement (SuccNat n) a (f,r) = (f,putListElement n a r);+    };+}
+ src/Data/Witness/Nat.hs view
@@ -0,0 +1,51 @@+module Data.Witness.Nat where+{+    import Prelude hiding (id,(.));+    import Data.Maybe;+    import Data.Type.Equality;+    import Data.Constraint(Dict(..));+    import Data.Witness.Representative;++    data NatKind = Zero | Succ NatKind;++    data Nat (t :: NatKind) where+    {+        ZeroNat :: Nat Zero;+        SuccNat :: Nat t -> Nat (Succ t);+    };++    instance TestEquality Nat where+    {+        testEquality ZeroNat ZeroNat = return Refl;+        testEquality (SuccNat a) (SuccNat b) = do+        {+            Refl <- testEquality a b;+            return Refl;+        };+        testEquality _ _ = Nothing;+    };++    instance Eq1 Nat where+    {+        equals1 a b = isJust (testEquality a b);+    };++    instance Representative Nat where+    {+        getRepWitness ZeroNat = Dict;+        getRepWitness (SuccNat n) = case getRepWitness n of+        {+            Dict -> Dict;+        };+    };++    instance Is Nat Zero where+    {+        representative = ZeroNat;+    };++    instance (Is Nat n) => Is Nat (Succ n) where+    {+        representative = SuccNat representative;+    };+}
+ src/Data/Witness/Representative.hs view
@@ -0,0 +1,64 @@+module Data.Witness.Representative where+{+    import Data.Witness.Any;+    import Data.Constraint;+    import Data.Proxy;++    class Eq1 (p :: k -> *) where+    {+        equals1 :: forall a. p a -> p a -> Bool;+    };++    instance Eq1 Proxy where+    {+        equals1 Proxy Proxy = True;+    };++    isWitnessRepresentative :: Dict (Is rep a) -> rep a;+    isWitnessRepresentative Dict = representative;++    class Eq1 rep => Representative (rep :: k -> *) where+    {+        -- | Every value is an instance of 'Is'.+        ;+        getRepWitness :: forall (a :: k). rep a -> Dict (Is rep a);+    };++    instance Representative Proxy where+    {+        getRepWitness Proxy = Dict;+    };++    withRepresentative :: forall (rep :: k -> *) r. (Representative rep) =>+      (forall (a :: k). (Is rep a) => rep a -> r) -> (forall (b :: k). rep b -> r);+    withRepresentative foo rep = case getRepWitness rep of+    {+        Dict -> foo rep;+    };++    -- | If two representatives have the same type, then they have the same value.+    ;+    class Representative rep => Is (rep :: k -> *) (a :: k) where+    {+        -- | The representative value for type @a@.+        ;+        representative :: rep a;+    };++    instance Is Proxy a where+    {+        representative = Proxy;+    };++    getRepresentative :: (Is rep a) => a -> rep a;+    getRepresentative _ = representative;++    rerepresentative :: (Is rep a) => p a -> rep a;+    rerepresentative _ = representative;++    mkAny :: (Is rep a) => a -> Any rep;+    mkAny a = MkAny representative a;++    mkAnyF :: (Is rep a) => f a -> AnyF rep f;+    mkAnyF fa = MkAnyF representative fa;+}
+ src/Data/Witness/WitnessDict.hs view
@@ -0,0 +1,63 @@+module Data.Witness.WitnessDict where+{+    import Data.Maybe;+    import Data.Type.Equality;+    import Data.Witness.Any;++    -- | A dictionary that is heterogenous up to its simple witness type @w@.+    -- Witnesses are the keys of the dictionary, and the values they witness are the values of the dictionary.+    ;+    newtype WitnessDict (w :: * -> *) = MkWitnessDict [Any w];++    -- | An empty dictionary.+    ;+    emptyWitnessDict :: WitnessDict w;+    emptyWitnessDict = MkWitnessDict[];++    -- | Look up the first value in the dictionary that matches the given witness.+    ;+    witnessDictLookup :: (TestEquality w) => w a -> WitnessDict w -> Maybe a;+    witnessDictLookup wit (MkWitnessDict cells) = listToMaybe (mapMaybe (matchAny wit) cells);++    -- | Modify the first value in the dictionary that matches a particular witness.+    ;+    witnessDictModify :: (TestEquality w) => w a -> (a -> a) -> WitnessDict w -> WitnessDict w;+    witnessDictModify wit amap (MkWitnessDict cells) = MkWitnessDict+        (replaceFirst ((fmap ((MkAny wit) . amap)) . (matchAny wit)) cells) where+    {+        replaceFirst :: (a -> Maybe a) -> [a] -> [a];+        replaceFirst ama (a:aa) = case ama a of+        {+            Just newa -> (newa:aa);+            _ -> a : (replaceFirst ama aa);+        };+        replaceFirst _ _ = [];+    };++    -- | Replace the first value in the dictionary that matches the witness+    ;+    witnessDictReplace :: (TestEquality w) => w a -> a -> WitnessDict w -> WitnessDict w;+    witnessDictReplace wit newa = witnessDictModify wit (const newa);++    -- | Add a witness and value as the first entry in the dictionary.+    ;+    witnessDictAdd :: w a -> a -> WitnessDict w -> WitnessDict w;+    witnessDictAdd wit a (MkWitnessDict cells) = MkWitnessDict ((MkAny wit a):cells);++    -- | Remove the first entry in the dictionary that matches the given witness.+    ;+    witnessDictRemove :: (TestEquality w) => w a -> WitnessDict w -> WitnessDict w;+    witnessDictRemove wit (MkWitnessDict cells) = MkWitnessDict+        (removeFirst (\(MkAny cwit _) -> isJust (testEquality wit cwit)) cells) where+    {+        removeFirst :: (a -> Bool) -> [a] -> [a];+        removeFirst p (a:as) | p a = as;+        removeFirst p (a:as) = a : (removeFirst p as);+        removeFirst _ _ = [];+    };++    -- | Create a dictionary from a list of witness\/value pairs+    ;+    witnessDictFromList :: (TestEquality w) => [Any w] -> WitnessDict w;+    witnessDictFromList = MkWitnessDict;+}
+ src/Data/Witness/WitnessFDict.hs view
@@ -0,0 +1,63 @@+module Data.Witness.WitnessFDict where+{+    import Data.Maybe;+    import Data.Type.Equality;+    import Data.Witness.Any;++    -- | A dictionary that is heterogenous up to its simple witness type @w@.+    -- Witnesses are the keys of the dictionary, and the values they witness are the values of the dictionary.+    ;+    newtype WitnessFDict (w :: k -> *) (f :: k -> *) = MkWitnessFDict [AnyF w f];++    -- | An empty dictionary.+    ;+    emptyWitnessFDict :: WitnessFDict w f;+    emptyWitnessFDict = MkWitnessFDict [];++    -- | Look up the first value in the dictionary that matches the given witness.+    ;+    witnessFDictLookup :: (TestEquality w) => w a -> WitnessFDict w f -> Maybe (f a);+    witnessFDictLookup wit (MkWitnessFDict cells) = listToMaybe (mapMaybe (matchAnyF wit) cells);++    -- | Modify the first value in the dictionary that matches a particular witness.+    ;+    witnessFDictModify :: (TestEquality w) => w a -> (f a -> f a) -> WitnessFDict w f -> WitnessFDict w f;+    witnessFDictModify wit amap (MkWitnessFDict cells) = MkWitnessFDict+        (replaceFirst ((fmap ((MkAnyF wit) . amap)) . (matchAnyF wit)) cells) where+    {+        replaceFirst :: (a -> Maybe a) -> [a] -> [a];+        replaceFirst ama (a:aa) = case ama a of+        {+            Just newa -> (newa:aa);+            _ -> a : (replaceFirst ama aa);+        };+        replaceFirst _ _ = [];+    };++    -- | Replace the first value in the dictionary that matches the witness+    ;+    witnessFDictReplace :: (TestEquality w) => w a -> f a -> WitnessFDict w f -> WitnessFDict w f;+    witnessFDictReplace wit newfa = witnessFDictModify wit (const newfa);++    -- | Add a witness and value as the first entry in the dictionary.+    ;+    witnessFDictAdd :: w a -> f a -> WitnessFDict w f -> WitnessFDict w f;+    witnessFDictAdd wit fa (MkWitnessFDict cells) = MkWitnessFDict ((MkAnyF wit fa):cells);++    -- | Remove the first entry in the dictionary that matches the given witness.+    ;+    witnessFDictRemove :: (TestEquality w) => w a -> WitnessFDict w f -> WitnessFDict w f;+    witnessFDictRemove wit (MkWitnessFDict cells) = MkWitnessFDict+        (removeFirst (\(MkAnyF cwit _) -> isJust (testEquality wit cwit)) cells) where+    {+        removeFirst :: (a -> Bool) -> [a] -> [a];+        removeFirst p (a:as) | p a = as;+        removeFirst p (a:as) = a : (removeFirst p as);+        removeFirst _ _ = [];+    };++    -- | Create a dictionary from a list of witness\/value pairs+    ;+    witnessFDictFromList :: (TestEquality w) => [AnyF w f] -> WitnessFDict w f;+    witnessFDictFromList = MkWitnessFDict;+}
witness.cabal view
@@ -1,53 +1,52 @@-cabal-version: >= 1.6+cabal-version:  >=1.14+name:           witness+version:        0.3+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/witness+bug-reports:    https://github.com/AshleyYakeley/witness/issues+synopsis:       values that witness types+description:+    A witness is a value that /witnesses/ some sort of constraint on some list of type variables.+    This library provides support for simple witnesses, that constrain a type variable to a single type, and equality witnesses, that constrain two type variables to be the same type.+    It also provides classes for representatives, which are values that represent types.+    See the paper /Witnesses and Open Witnesses/ (<http://semantic.org/stuff/Open-Witnesses.pdf>).+category:       Data+build-type:     Simple -name: witness-version: 0.2-build-type: Simple-license: BSD3-license-file: LICENSE-copyright:-maintainer: Ashley Yakeley <ashley@semantic.org>-build-depends: base == 4.*, mtl >=1.1-stability:-homepage:-package-url:-bug-reports:-synopsis: values that witness types-description: A witness is a value that /witnesses/ some sort of constraint on some list of type variables.-             This library provides support for simple witnesses, that constrain a type variable to a single type, and equality witnesses, that constrain two type variables to be the same type. It also provides classes for representatives, which are values that represent types.-             See the paper /Witnesses and Open Witnesses/ (<http://semantic.org/stuff/Open-Witnesses.pdf>).-category: Data-author: Ashley Yakeley <ashley@semantic.org>-tested-with:-data-files:-data-dir: ""-extra-source-files:-extra-tmp-files:-exposed-modules: Data.Witness Data.Witness.SimpleWitness-                 Data.Witness.Type Data.Witness.List Data.Witness.WitnessDict-                 Data.Witness.WitnessFDict Data.Witness.Any Data.Witness.Nat-                 Data.Witness.Representative Data.Witness.EqualType-exposed: True-buildable: True-build-tools:-cpp-options:-cc-options:-ld-options:-pkgconfig-depends:-frameworks:-c-sources:-extensions: MultiParamTypeClasses RankNTypes FlexibleContexts-            FlexibleInstances EmptyDataDecls KindSignatures TypeFamilies GADTs-extra-libraries:-extra-lib-dirs:-includes:-install-includes:-include-dirs:-hs-source-dirs: .-other-modules:-ghc-prof-options:-ghc-shared-options:-ghc-options: -Wall-hugs-options:-nhc98-options:-jhc-options:+library+    hs-source-dirs: src+    default-language: Haskell98+    default-extensions:+        MultiParamTypeClasses+        RankNTypes+        FlexibleContexts+        TypeOperators+        FlexibleInstances+        EmptyDataDecls+        KindSignatures+        TypeFamilies+        GADTs+        PolyKinds+        DataKinds+        ScopedTypeVariables+        PatternGuards+    build-depends:+        base == 4.*,+        transformers >=0.3,+        categories == 1.0.*,+        constraints >= 0.3+    exposed-modules:+        Data.Witness.Any+        Data.Witness.WitnessDict+        Data.Witness.WitnessFDict+        Data.Witness.Nat+        Data.Witness.ListElement+        Data.Witness.List+        Data.Witness.Representative+        Data.Witness+    ghc-options: -Wall