witness 0.3.0.1 → 0.4

raw patch · 8 files changed

+73/−46 lines, 8 filesdep +semigroupoidsdep −categories

Dependencies added: semigroupoids

Dependencies removed: categories

Files

• src/Control/Category/Tensor.hs +23/−0
• src/Data/Nat.hs +19/−0
• src/Data/Witness/List.hs +2/−20
• src/Data/Witness/ListElement.hs +7/−6
• src/Data/Witness/Nat.hs +15/−16
• src/Data/Witness/WitnessDict.hs +1/−1
• src/Data/Witness/WitnessFDict.hs +1/−1
• witness.cabal +5/−2

@@ -0,0 +1,23 @@+module Control.Category.Tensor where+{+    import Data.Semigroupoid.Dual;++    -- 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);+    };+}

@@ -0,0 +1,19 @@+module Data.Nat where+{+    data Nat = Zero | Succ Nat;++    addNat :: Nat -> Nat -> Nat;+    addNat Zero b = b;+    addNat (Succ a) b = Succ $ addNat a b;++    -- | subtractFromNat a b = b - a+    ;+    subtractFromNat :: Nat -> Nat -> Maybe Nat;+    subtractFromNat Zero b = Just b;+    subtractFromNat (Succ a) (Succ b) = subtractFromNat a b;+    subtractFromNat (Succ _) Zero = Nothing;++    multiplyNat :: Nat -> Nat -> Nat;+    multiplyNat Zero _ = Zero;+    multiplyNat (Succ a) b = addNat (multiplyNat a b) b;+}

@@ -1,13 +1,14 @@+{-# OPTIONS -fno-warn-overlapping-patterns #-} 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;+    import Control.Category.Tensor;      -- | a witness type for HList-style lists.     -- The @w@ parameter is the witness type of the elements.@@ -199,25 +200,6 @@                 }             };         };-    };--    -- 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;

@@ -1,15 +1,16 @@ module Data.Witness.ListElement where {+    import Data.Nat;     import Data.Witness.Nat; -    class HasListElement (n :: NatKind) (list :: *) where+    class HasListElement (n :: Nat) (list :: *) where     {         type ListElement n list :: *;-        getListElement :: Nat n -> list -> ListElement n list;-        putListElement :: Nat n -> ListElement n list -> list -> list;+        getListElement :: NatType n -> list -> ListElement n list;+        putListElement :: NatType n -> ListElement n list -> list -> list;     }; -    modifyListElement :: (HasListElement n t) => Nat n -> (ListElement n t -> ListElement n t) -> t -> t;+    modifyListElement :: (HasListElement n t) => NatType 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@@ -22,7 +23,7 @@     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);+        getListElement (SuccType n) (_,r) = getListElement n r;+        putListElement (SuccType n) a (f,r) = (f,putListElement n a r);     }; }

@@ -4,20 +4,19 @@     import Data.Maybe;     import Data.Type.Equality;     import Data.Constraint(Dict(..));+    import Data.Nat;     import Data.Witness.Representative; -    data NatKind = Zero | Succ NatKind;--    data Nat (t :: NatKind) where+    data NatType (t :: Nat) where     {-        ZeroNat :: Nat 'Zero;-        SuccNat :: Nat t -> Nat ('Succ t);+        ZeroType :: NatType 'Zero;+        SuccType :: NatType t -> NatType ('Succ t);     }; -    instance TestEquality Nat where+    instance TestEquality NatType where     {-        testEquality ZeroNat ZeroNat = return Refl;-        testEquality (SuccNat a) (SuccNat b) = do+        testEquality ZeroType ZeroType = return Refl;+        testEquality (SuccType a) (SuccType b) = do         {             Refl <- testEquality a b;             return Refl;@@ -25,27 +24,27 @@         testEquality _ _ = Nothing;     }; -    instance Eq1 Nat where+    instance Eq1 NatType where     {         equals1 a b = isJust (testEquality a b);     }; -    instance Representative Nat where+    instance Representative NatType where     {-        getRepWitness ZeroNat = Dict;-        getRepWitness (SuccNat n) = case getRepWitness n of+        getRepWitness ZeroType = Dict;+        getRepWitness (SuccType n) = case getRepWitness n of         {             Dict -> Dict;         };     }; -    instance Is Nat 'Zero where+    instance Is NatType 'Zero where     {-        representative = ZeroNat;+        representative = ZeroType;     }; -    instance (Is Nat n) => Is Nat ('Succ n) where+    instance (Is NatType n) => Is NatType ('Succ n) where     {-        representative = SuccNat representative;+        representative = SuccType representative;     }; }

@@ -58,6 +58,6 @@      -- | Create a dictionary from a list of witness\/value pairs     ;-    witnessDictFromList :: (TestEquality w) => [Any w] -> WitnessDict w;+    witnessDictFromList :: [Any w] -> WitnessDict w;     witnessDictFromList = MkWitnessDict; }

@@ -58,6 +58,6 @@      -- | Create a dictionary from a list of witness\/value pairs     ;-    witnessFDictFromList :: (TestEquality w) => [AnyF w f] -> WitnessFDict w f;+    witnessFDictFromList :: [AnyF w f] -> WitnessFDict w f;     witnessFDictFromList = MkWitnessFDict; }

@@ -1,6 +1,6 @@ cabal-version:  >=1.14 name:           witness-version:        0.3.0.1+version:        0.4 x-follows-version-policy: license:        BSD3 license-file:   LICENSE@@ -35,12 +35,15 @@         DataKinds         ScopedTypeVariables         PatternGuards+        PatternSynonyms     build-depends:         base >= 4.7 && < 5,         transformers,-        categories,+        semigroupoids,         constraints     exposed-modules:+        Data.Nat+        Control.Category.Tensor         Data.Witness.Any         Data.Witness.WitnessDict         Data.Witness.WitnessFDict