diff --git a/Control/Category.hs b/Control/Category.hs
new file mode 100644
--- /dev/null
+++ b/Control/Category.hs
@@ -0,0 +1,18 @@
+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..);
+	};
+}
diff --git a/Data/Witness.hs b/Data/Witness.hs
new file mode 100644
--- /dev/null
+++ b/Data/Witness.hs
@@ -0,0 +1,29 @@
+module Data.Witness
+(
+	module Data.Witness.WitnessDict,
+	module Data.Witness.Any,
+	module Data.Witness.Representative,
+	module Data.Witness.Type,
+	module Data.Witness.SimpleWitness,
+	module Data.Witness.EqualType,
+	module Data.Witness.List,
+	module Data.Witness
+) where
+{
+	import Data.Witness.List;
+	import Data.Witness.EqualType;
+	import Data.Witness.SimpleWitness;
+	import Data.Witness.Type;
+	import Data.Witness.Representative;
+	import Data.Witness.Any;
+	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;
+	};
+}
diff --git a/Data/Witness/Any.hs b/Data/Witness/Any.hs
new file mode 100644
--- /dev/null
+++ b/Data/Witness/Any.hs
@@ -0,0 +1,56 @@
+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);
+}
diff --git a/Data/Witness/EqualType.hs b/Data/Witness/EqualType.hs
new file mode 100644
--- /dev/null
+++ b/Data/Witness/EqualType.hs
@@ -0,0 +1,18 @@
+module Data.Witness.EqualType where
+{
+	import Control.Category;
+	import Prelude hiding (id,(.));
+
+	-- | 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;
+	};
+}
diff --git a/Data/Witness/List.hs b/Data/Witness/List.hs
new file mode 100644
--- /dev/null
+++ b/Data/Witness/List.hs
@@ -0,0 +1,57 @@
+module Data.Witness.List where
+{
+	import Control.Category;
+	import Data.Witness.Representative;
+	import Data.Witness.SimpleWitness;
+	import Data.Witness.EqualType;
+	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
+	{
+		withRepresentative f NilListType = f NilListType;
+		withRepresentative f (ConsListType w lw) = withRepresentative (\w' -> withRepresentative (\lw' -> f (ConsListType w' lw')) lw) w;
+	};
+
+	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;
+	};
+}
diff --git a/Data/Witness/Representative.hs b/Data/Witness/Representative.hs
new file mode 100644
--- /dev/null
+++ b/Data/Witness/Representative.hs
@@ -0,0 +1,37 @@
+module Data.Witness.Representative where
+{
+	import Data.Witness.Any;
+
+	class Eq1 p where
+	{
+		equals1 :: forall a. p a -> p a -> Bool;
+	};
+
+	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);
+	};
+
+	-- | 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;
+}
diff --git a/Data/Witness/SimpleWitness.hs b/Data/Witness/SimpleWitness.hs
new file mode 100644
--- /dev/null
+++ b/Data/Witness/SimpleWitness.hs
@@ -0,0 +1,15 @@
+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);
+	};
+}
diff --git a/Data/Witness/Type.hs b/Data/Witness/Type.hs
new file mode 100644
--- /dev/null
+++ b/Data/Witness/Type.hs
@@ -0,0 +1,28 @@
+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
+	{
+		withRepresentative f t = f t;
+	};
+
+	instance Is Type a where
+	{
+		representative = Type;
+	};
+}
diff --git a/Data/Witness/WitnessDict.hs b/Data/Witness/WitnessDict.hs
new file mode 100644
--- /dev/null
+++ b/Data/Witness/WitnessDict.hs
@@ -0,0 +1,64 @@
+module Data.Witness.WitnessDict where
+{
+	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@. 
+	-- 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;
+}
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,10 @@
+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.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/witness.cabal b/witness.cabal
new file mode 100644
--- /dev/null
+++ b/witness.cabal
@@ -0,0 +1,33 @@
+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.
+
+	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