packages feed

witness 0.1 → 0.2

raw patch · 10 files changed

+241/−57 lines, 10 filesdep ~base

Dependency ranges changed: base

Files

− Control/Category.hs 
@@ -1,18 +0,0 @@-module Control.Category where-{-	import qualified Prelude;--	-- | ('.') must be associative, and 'id' must be a left and right identity for ('.').-	;-	class Category comp where-	{-		id :: comp a a;-		(.) :: comp b c -> comp a b -> comp a c;-	};--	instance Category (->) where-	{-		id = Prelude.id;-		(.) = (Prelude..);-	};-}
Data/Witness.hs view
@@ -1,21 +1,25 @@ 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.
Data/Witness/EqualType.hs view
@@ -1,7 +1,6 @@ module Data.Witness.EqualType where { 	import Control.Category;-	import Prelude hiding (id,(.));  	-- | witness that type parameters @a@ and @b@ are the same type 	;
Data/Witness/List.hs view
@@ -1,9 +1,10 @@ module Data.Witness.List where {-	import Control.Category;+	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@. @@ -29,8 +30,11 @@  	instance (Representative w) => Representative (ListType w) where 	{-		withRepresentative f NilListType = f NilListType;-		withRepresentative f (ConsListType w lw) = withRepresentative (\w' -> withRepresentative (\lw' -> f (ConsListType w' lw')) lw) w;+		getRepWitness NilListType = MkRepWitness;+		getRepWitness (ConsListType w lw) = case (getRepWitness w,getRepWitness lw) of+		{+			(MkRepWitness,MkRepWitness) -> MkRepWitness;+		}; 	};  	instance (Representative w) => Is (ListType w) () where@@ -54,4 +58,29 @@ 		}; 		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 view
@@ -0,0 +1,53 @@+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 view
@@ -1,19 +1,39 @@ 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'. 		;-		withRepresentative :: forall r. (forall a. (Is rep a) => rep a -> r) -> (forall b. rep b -> r);+		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@@ -34,4 +54,19 @@  	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/Type.hs view
@@ -18,7 +18,7 @@  	instance Representative Type where 	{-		withRepresentative f t = f t;+		getRepWitness Type = MkRepWitness; 	};  	instance Is Type a where
Data/Witness/WitnessDict.hs view
@@ -2,7 +2,6 @@ { 	import Data.Witness.Any; 	import Data.Witness.SimpleWitness;-	import Control.Monad.State; 	import Data.Maybe; 	 	-- | A dictionary that is heterogenous up to its simple witness type @w@.
+ Data/Witness/WitnessFDict.hs view
@@ -0,0 +1,63 @@+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;+}
witness.cabal view
@@ -1,33 +1,53 @@-name:			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-category:		Data-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.+cabal-version: >= 1.6 -	See the paper /Witnesses and Open Witnesses/ (<http://semantic.org/stuff/Open-Witnesses.pdf>).-extensions:-	RankNTypes-	MultiParamTypeClasses-	FlexibleInstances-	FlexibleContexts-	GADTs-	KindSignatures-build-type:		Simple-exposed-modules:-	Control.Category-	Data.Witness-	Data.Witness.WitnessDict-	Data.Witness.Representative-	Data.Witness.List-	Data.Witness.Any-	Data.Witness.Type-	Data.Witness.SimpleWitness-	Data.Witness.EqualType+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: