diff --git a/Control/Category.hs b/Control/Category.hs deleted file mode 100644 --- a/Control/Category.hs +++ /dev/null @@ -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..); - }; -} diff --git a/Data/Witness.hs b/Data/Witness.hs --- a/Data/Witness.hs +++ b/Data/Witness.hs @@ -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. diff --git a/Data/Witness/EqualType.hs b/Data/Witness/EqualType.hs --- a/Data/Witness/EqualType.hs +++ b/Data/Witness/EqualType.hs @@ -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 ; diff --git a/Data/Witness/List.hs b/Data/Witness/List.hs --- a/Data/Witness/List.hs +++ b/Data/Witness/List.hs @@ -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); + }; } diff --git a/Data/Witness/Nat.hs b/Data/Witness/Nat.hs new file mode 100644 --- /dev/null +++ b/Data/Witness/Nat.hs @@ -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; + }; +} diff --git a/Data/Witness/Representative.hs b/Data/Witness/Representative.hs --- a/Data/Witness/Representative.hs +++ b/Data/Witness/Representative.hs @@ -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; + }; } diff --git a/Data/Witness/Type.hs b/Data/Witness/Type.hs --- a/Data/Witness/Type.hs +++ b/Data/Witness/Type.hs @@ -18,7 +18,7 @@ instance Representative Type where { - withRepresentative f t = f t; + getRepWitness Type = MkRepWitness; }; instance Is Type a where diff --git a/Data/Witness/WitnessDict.hs b/Data/Witness/WitnessDict.hs --- a/Data/Witness/WitnessDict.hs +++ b/Data/Witness/WitnessDict.hs @@ -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@. diff --git a/Data/Witness/WitnessFDict.hs b/Data/Witness/WitnessFDict.hs new file mode 100644 --- /dev/null +++ b/Data/Witness/WitnessFDict.hs @@ -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; +} diff --git a/witness.cabal b/witness.cabal --- a/witness.cabal +++ b/witness.cabal @@ -1,33 +1,53 @@ -name: witness -version: 0.1 -license: BSD3 -license-file: LICENSE -author: Ashley Yakeley -maintainer: Ashley Yakeley -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/ (). -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 +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/ (). +category: Data +author: Ashley Yakeley +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: