packages feed

witness 0.4 → 0.5

raw patch · 29 files changed

+1387/−696 lines, 29 filesdep +countabledep ~basesetup-changed

Dependencies added: countable

Dependency ranges changed: base

Files

Setup.hs view
@@ -1,2 +1,3 @@ import Distribution.Simple+ main = defaultMain
src/Control/Category/Tensor.hs view
@@ -1,23 +1,17 @@ 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);-    };+import Data.Semigroupoid.Dual+import Prelude -    instance Tensor (->) where-    {-        tensorUnit = id;-        tensorPair ab1 ab2 (a1,a2) = (ab1 a1,ab2 a2);-    };+-- 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 cc) => Tensor (Dual cc) where-    {-        tensorUnit = Dual tensorUnit;-        tensorPair (Dual ab1) (Dual ab2) = Dual (tensorPair ab1 ab2);-    };-}+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)
src/Data/Nat.hs view
@@ -1,19 +1,21 @@ 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;+import Prelude -    -- | 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;+data Nat+    = Zero+    | Succ Nat -    multiplyNat :: Nat -> Nat -> Nat;-    multiplyNat Zero _ = Zero;-    multiplyNat (Succ a) b = addNat (multiplyNat a b) b;-}+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
+ src/Data/Type/Apply.hs view
@@ -0,0 +1,14 @@+module Data.Type.Apply where++import Control.Category+import Data.Kind+import Data.Type.Equality++applyRefl ::+       forall k1 k2 (fa :: k1 -> k2) (fb :: k1 -> k2) (a :: k1) (b :: k1). fa :~: fb -> a :~: b -> (fa a) :~: (fb b)+applyRefl Refl Refl = Refl++reflId ::+       forall k (cat :: k -> k -> Type) (a :: k) (b :: k). Category cat+    => a :~: b -> cat a b+reflId Refl = id
+ src/Data/Type/Heterogeneous.hs view
@@ -0,0 +1,15 @@+module Data.Type.Heterogeneous where++import Data.Kind+import Data.Type.Equality+import Prelude++withHRefl :: forall ka (a :: ka) kb (b :: kb) (r :: Type). a :~~: b -> ((a ~~ b) => r) -> r+withHRefl HRefl r = r++-- | somewhat awkwardly named+homoHetEq :: forall (k :: Type) (a :: k) (b :: k). a :~~: b -> a :~: b+homoHetEq HRefl = Refl++class TestHetEquality (w :: forall k. k -> Type) where+    testHetEquality :: forall (ka :: Type) (a :: ka) (kb :: Type) (b :: kb). w a -> w b -> Maybe (a :~~: b)
+ src/Data/Type/With.hs view
@@ -0,0 +1,18 @@+module Data.Type.With where++import Control.Category+import Data.Kind+import Data.Type.Equality++withRefl :: forall k (a :: k) (b :: k) (r :: Type). a :~: b -> (a ~ b => r) -> r+withRefl Refl r = r++reflCat ::+       forall k (cat :: k -> k -> Type) (a :: k) (b :: k). Category cat+    => a :~: b -> cat a b+reflCat Refl = id++reflWitCat ::+       forall kq (cat :: kq -> kq -> Type) kp (w :: kp -> kq) (a :: kp) (b :: kp). Category cat+    => a :~: b -> cat (w a) (w b)+reflWitCat Refl = id
src/Data/Witness.hs view
@@ -1,33 +1,44 @@ 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;+    ( module I+    , module Data.Witness+    ) where -    -- | 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;-    };-}+import Data.Nat as I+import Data.Proxy as I+import Data.Type.Apply as I+import Data.Type.Equality as I+import Data.Type.Heterogeneous as I+import Data.Type.With as I+import Data.Witness.All as I+import Data.Witness.Any as I+import Data.Witness.ApplyStack as I+import Data.Witness.BigNat as I+import Data.Witness.Concat as I+import Data.Witness.Cons as I+import Data.Witness.Constraint as I+import Data.Witness.Either as I+import Data.Witness.Finite as I+import Data.Witness.HList as I+import Data.Witness.Kind as I+import Data.Witness.List as I+import Data.Witness.ListElement as I+import Data.Witness.Nat as I+import Data.Witness.Representative as I+import Data.Witness.Single as I+import Data.Witness.Submap as I+import Data.Witness.Symbol as I+import Data.Witness.WitnessDict as I+import Data.Witness.WitnessFDict as I+import Data.Witness.WitnessValue as I+import Prelude++-- | 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/All.hs view
@@ -0,0 +1,39 @@+module Data.Witness.All where++import Data.Functor.Identity+import Data.Kind+import Data.Type.Equality+import Data.Witness.Any+import Prelude++newtype AllF (w :: k -> Type) (f :: k -> Type) = MkAllF+    { getAllF :: forall (t :: k). w t -> f t+    }++newtype AllValue (w :: Type -> Type) = MkAllValue+    { getAllValue :: forall t. w t -> t+    }++setAllValue :: TestEquality wit => wit a -> a -> AllValue wit -> AllValue wit+setAllValue wa a (MkAllValue wtt) =+    MkAllValue $ \wa' ->+        case testEquality wa wa' of+            Just Refl -> a+            Nothing -> wtt wa'++allFToAllValue :: AllF w Identity -> AllValue w+allFToAllValue (MkAllF wtit) = MkAllValue $ \wt -> runIdentity $ wtit wt++allValueToAllF :: AllValue w -> AllF w Identity+allValueToAllF (MkAllValue wtt) = MkAllF $ \wt -> Identity $ wtt wt++type family UnAllValue (aw :: Type) :: Type -> Type where+    UnAllValue (AllValue w) = w++splitWitnessList :: TestEquality w => [AnyValue w] -> AllF w []+splitWitnessList [] = MkAllF $ \_ -> []+splitWitnessList ((MkAnyValue wt t):rr) =+    MkAllF $ \wt' ->+        case testEquality wt wt' of+            Just Refl -> t : (getAllF (splitWitnessList rr) wt')+            Nothing -> getAllF (splitWitnessList rr) wt'
src/Data/Witness/Any.hs view
@@ -1,39 +1,52 @@ 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;+import Data.Functor.Const+import Data.Functor.Identity+import Data.Kind+import Data.Maybe+import Data.Type.Equality+import Data.Witness.Constraint+import Prelude -    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 -> Type) (f :: k -> Type) =+    forall (a :: k). MkAnyF (w a)+                            (f a) -    -- | 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 -    matchAnyF :: (TestEquality w) => w a -> AnyF w f -> Maybe (f a);-    matchAnyF wit (MkAnyF cwit cfa) = do-    {-        Refl <- testEquality cwit wit;-        return cfa;-    };+type AnyValue w = AnyF w Identity -    -- | Any witness.-    ;-    data AnyWitness (w :: k -> *) = forall (a :: k). MkAnyWitness (w a);+pattern MkAnyValue :: w a -> a -> AnyValue w -    matchAnyWitness :: (TestEquality w) => w a -> AnyWitness w -> Bool;-    matchAnyWitness wit (MkAnyWitness cwit) = isJust (testEquality cwit wit);+pattern MkAnyValue wa a = MkAnyF wa (Identity a) -    instance (TestEquality w) => Eq (AnyWitness w) where-    {-        (==) (MkAnyWitness wa) = matchAnyWitness wa;-    };-}+{-# COMPLETE MkAnyValue #-}++matchAnyValue :: TestEquality w => w a -> AnyValue w -> Maybe a+matchAnyValue wit av = do+    Identity a <- matchAnyF wit av+    return a++type AnyW w = AnyF w (Const ())++pattern MkAnyW :: w a -> AnyW w++pattern MkAnyW wa = MkAnyF wa (Const ())++{-# COMPLETE MkAnyW #-}++matchAnyW :: TestEquality w => w a -> AnyW w -> Bool+matchAnyW wit aw = isJust $ matchAnyF wit aw++instance TestEquality w => Eq (AnyW w) where+    (==) (MkAnyW wa) = matchAnyW wa++mapAnyW :: (forall t. w1 t -> w2 t) -> AnyW w1 -> AnyW w2+mapAnyW f (MkAnyW wt) = MkAnyW $ f wt++instance AllWitnessConstraint Show w => Show (AnyW w) where+    show (MkAnyW wa) = showAllWitness wa
+ src/Data/Witness/ApplyStack.hs view
@@ -0,0 +1,25 @@+module Data.Witness.ApplyStack where++import Data.Type.Equality+import Data.Witness.Concat+import Data.Witness.List+import Data.Witness.Representative+import Prelude hiding ((.), id)++type family ApplyStack (f :: [k -> k]) (a :: k) :: k where+    ApplyStack '[] a = a+    ApplyStack (t ': tt) a = t (ApplyStack tt a)++witApplyConcatRefl ::+       forall k (f1 :: [k -> k]) (f2 :: [k -> k]) (a :: k) w.+       ListType w f1+    -> (ApplyStack (Concat f1 f2) a) :~: (ApplyStack f1 (ApplyStack f2 a))+witApplyConcatRefl NilListType = Refl+witApplyConcatRefl (ConsListType _ lt) =+    case witApplyConcatRefl @k @_ @f2 @a lt of+        Refl -> Refl++applyConcatRefl ::+       forall k (f1 :: [k -> k]) (f2 :: [k -> k]) (a :: k) w. Is (ListType w) f1+    => (ApplyStack (Concat f1 f2) a) :~: (ApplyStack f1 (ApplyStack f2 a))+applyConcatRefl = witApplyConcatRefl @k @f1 @f2 @a $ representative @_ @(ListType w) @f1
+ src/Data/Witness/BigNat.hs view
@@ -0,0 +1,48 @@+module Data.Witness.BigNat+    ( module Data.Witness.BigNat+    , KnownNat+    ) where++import Data.Constraint+import Data.Proxy+import Data.Type.Equality+import Data.Witness.Constraint+import Data.Witness.Representative+import Data.Witness.WitnessValue+import GHC.TypeLits+import Numeric.Natural+import Prelude++type BigNat = Nat++data BigNatType (bn :: BigNat) where+    MkBigNatType :: KnownNat bn => BigNatType bn++instance WitnessValue BigNatType where+    type WitnessValueType BigNatType = Natural+    witnessToValue :: forall t. BigNatType t -> Natural+    witnessToValue MkBigNatType = fromInteger $ natVal (Proxy :: Proxy t)+    valueToWitness i cont =+        case someNatVal $ toInteger i of+            Just (SomeNat p) -> let+                psw :: forall (t :: BigNat). KnownNat t+                    => Proxy t+                    -> BigNatType t+                psw _ = MkBigNatType+                in cont $ psw p+            Nothing -> error "negative Natural"++instance TestEquality BigNatType where+    testEquality (MkBigNatType :: BigNatType a) (MkBigNatType :: BigNatType b) = sameNat (Proxy @a) (Proxy @b)++instance Representative BigNatType where+    getRepWitness MkBigNatType = Dict++instance KnownNat bn => Is BigNatType bn where+    representative = MkBigNatType++instance Show (BigNatType bn) where+    show = show . witnessToValue++instance AllWitnessConstraint Show BigNatType where+    allWitnessConstraint = Dict
+ src/Data/Witness/Concat.hs view
@@ -0,0 +1,34 @@+module Data.Witness.Concat where++import Data.Constraint (Dict(..))+import Data.Type.Equality+import Data.Witness.List+import Data.Witness.Representative+import Prelude hiding ((.), id)++type family Concat (a :: [k]) (b :: [k]) :: [k] where+    Concat '[] bb = bb+    Concat (a ': aa) bb = a ': (Concat aa bb)++concatEmptyRefl :: ListType w a -> Concat a '[] :~: a+concatEmptyRefl NilListType = Refl+concatEmptyRefl (ConsListType _ la) =+    case concatEmptyRefl la of+        Refl -> Refl++concatIsDict ::+       forall w aa bb. (Representative w, Is (ListType w) aa, Is (ListType w) bb)+    => Dict (Is (ListType w) (Concat aa bb))+concatIsDict = let+    build :: forall aa'. ListType w aa' -> Dict (Is (ListType w) (Concat aa' bb))+    build NilListType = Dict+    build (ConsListType wa la) =+        case build la of+            Dict ->+                case getRepWitness wa of+                    Dict -> Dict+    in build $ representative @_ @(ListType w) @aa++concatListType :: ListType w a -> ListType w b -> ListType w (Concat a b)+concatListType NilListType lb = lb+concatListType (ConsListType wa la) lb = ConsListType wa $ concatListType la lb
+ src/Data/Witness/Cons.hs view
@@ -0,0 +1,98 @@+module Data.Witness.Cons where++import Data.Constraint+import Data.Countable+import Data.Empty+import Data.Kind+import Data.Proxy+import Data.Searchable+import Data.Type.Equality+import Data.Witness.All+import Data.Witness.Constraint+import Data.Witness.Finite+import Data.Witness.List+import Data.Witness.ListElement+import Data.Witness.Representative+import Prelude++newtype EmptyType t =+    MkEmptyType None+    deriving (Eq, Countable, Searchable, Empty)++instance Finite (EmptyType t) where+    allValues = []+    assemble _ = pure never++instance TestEquality EmptyType where+    testEquality = never++instance Representative EmptyType where+    getRepWitness = never++instance FiniteWitness EmptyType where+    assembleWitnessF _ = pure emptyAllF++instance WitnessConstraint c EmptyType where+    witnessConstraint = never++emptyAll :: AllValue EmptyType+emptyAll = MkAllValue never++emptyAllF :: AllF EmptyType f+emptyAllF = MkAllF never++data ConsType a r t where+    FirstType :: ConsType t r t+    RestType :: r t -> ConsType a r t++instance TestEquality r => TestEquality (ConsType a r) where+    testEquality FirstType FirstType = return Refl+    testEquality (RestType r1) (RestType r2) = do+        Refl <- testEquality r1 r2+        return Refl+    testEquality _ _ = Nothing++instance FiniteWitness r => FiniteWitness (ConsType a r) where+    assembleWitnessF getsel =+        (\f (MkAllF r) ->+             MkAllF $ \wt ->+                 case wt of+                     FirstType -> f+                     RestType rt -> r rt) <$>+        getsel FirstType <*>+        assembleWitnessF (getsel . RestType)++instance (c a, WitnessConstraint c r) => WitnessConstraint c (ConsType a r) where+    witnessConstraint FirstType = Dict+    witnessConstraint (RestType rt) =+        case witnessConstraint @_ @c rt of+            Dict -> Dict++consAll :: a -> AllValue r -> AllValue (ConsType a r)+consAll a (MkAllValue tup) =+    MkAllValue $ \esel ->+        case esel of+            FirstType -> a+            RestType sel -> tup sel++class Is (ListType Proxy) (FiniteConsWitness sel) => IsFiniteConsWitness (sel :: k -> Type) where+    type FiniteConsWitness sel :: [k]+    toLTW :: forall t. sel t -> ListElementType (FiniteConsWitness sel) t+    fromLTW :: forall t. ListElementType (FiniteConsWitness sel) t -> sel t++instance Is (ListType Proxy) edits => IsFiniteConsWitness (ListElementType edits) where+    type FiniteConsWitness (ListElementType edits) = edits+    toLTW = id+    fromLTW = id++instance IsFiniteConsWitness EmptyType where+    type FiniteConsWitness EmptyType = '[]+    toLTW wit = never wit+    fromLTW lt = never lt++instance IsFiniteConsWitness lt => IsFiniteConsWitness (ConsType a lt) where+    type FiniteConsWitness (ConsType a lt) = a : (FiniteConsWitness lt)+    toLTW FirstType = FirstElementType+    toLTW (RestType sel) = RestElementType $ toLTW sel+    fromLTW FirstElementType = FirstType+    fromLTW (RestElementType lt) = RestType $ fromLTW lt
+ src/Data/Witness/Constraint.hs view
@@ -0,0 +1,23 @@+module Data.Witness.Constraint where++import Data.Constraint+import Data.Kind+import Data.Type.Equality+import Prelude++class AllWitnessConstraint (c :: kw -> Constraint) (w :: kt -> kw) where+    allWitnessConstraint :: forall (t :: kt). Dict (c (w t))++instance AllWitnessConstraint Show ((:~:) t) where+    allWitnessConstraint = Dict++showAllWitness ::+       forall w t. AllWitnessConstraint Show w+    => w t+    -> String+showAllWitness wt =+    case allWitnessConstraint @_ @_ @Show @w @t of+        Dict -> show wt++class WitnessConstraint (c :: k -> Constraint) (w :: k -> Type) where+    witnessConstraint :: forall (t :: k). w t -> Dict (c t)
+ src/Data/Witness/Either.hs view
@@ -0,0 +1,66 @@+module Data.Witness.Either where++import Data.Constraint+import Data.Kind+import Data.Type.Equality+import Data.Witness.All+import Data.Witness.Constraint+import Data.Witness.Finite+import Prelude++data EitherType (colsel1 :: k -> Type) (colsel2 :: k -> Type) (t :: k)+    = LeftType (colsel1 t)+    | RightType (colsel2 t)++instance (TestEquality colsel1, TestEquality colsel2) => TestEquality (EitherType colsel1 colsel2) where+    testEquality (LeftType s1) (LeftType s2) = do+        Refl <- testEquality s1 s2+        return Refl+    testEquality (RightType s1) (RightType s2) = do+        Refl <- testEquality s1 s2+        return Refl+    testEquality _ _ = Nothing++instance (FiniteWitness p, FiniteWitness q) => FiniteWitness (EitherType p q) where+    assembleWitnessF getsel =+        (\(MkAllF p) (MkAllF q) ->+             MkAllF $ \wt ->+                 case wt of+                     LeftType rt -> p rt+                     RightType rt -> q rt) <$>+        assembleWitnessF (getsel . LeftType) <*>+        assembleWitnessF (getsel . RightType)++instance (WitnessConstraint c p, WitnessConstraint c q) => WitnessConstraint c (EitherType p q) where+    witnessConstraint (LeftType rt) =+        case witnessConstraint @_ @c rt of+            Dict -> Dict+    witnessConstraint (RightType rt) =+        case witnessConstraint @_ @c rt of+            Dict -> Dict++instance (Show (p t), Show (q t)) => Show (EitherType p q t) where+    show (LeftType rt) = show rt+    show (RightType rt) = show rt++instance (AllWitnessConstraint Show p, AllWitnessConstraint Show q) => AllWitnessConstraint Show (EitherType p q) where+    allWitnessConstraint :: forall t. Dict (Show (EitherType p q t))+    allWitnessConstraint =+        case allWitnessConstraint @_ @_ @Show @p @t of+            Dict ->+                case allWitnessConstraint @_ @_ @Show @q @t of+                    Dict -> Dict++eitherAll :: AllValue sel1 -> AllValue sel2 -> AllValue (EitherType sel1 sel2)+eitherAll (MkAllValue tup1) (MkAllValue tup2) =+    MkAllValue $ \esel ->+        case esel of+            LeftType sel -> tup1 sel+            RightType sel -> tup2 sel++eitherAllF :: AllF sel1 f -> AllF sel2 f -> AllF (EitherType sel1 sel2) f+eitherAllF (MkAllF tup1) (MkAllF tup2) =+    MkAllF $ \esel ->+        case esel of+            LeftType sel -> tup1 sel+            RightType sel -> tup2 sel
+ src/Data/Witness/Finite.hs view
@@ -0,0 +1,51 @@+{-# OPTIONS -fno-warn-orphans #-}++module Data.Witness.Finite where++import Data.Constraint+import Data.Countable+import Data.Functor.Const+import Data.Functor.Identity+import Data.Kind+import Data.List (intercalate)+import Data.Searchable+import Data.Type.Equality+import Data.Witness.All+import Data.Witness.Any+import Data.Witness.Constraint+import Prelude++class FiniteWitness (w :: k -> Type) where+    assembleWitnessF :: Applicative m => (forall t. w t -> m (f t)) -> m (AllF w f)++instance (TestEquality w, FiniteWitness w) => Countable (AnyW w) where+    countPrevious = finiteCountPrevious+    countMaybeNext = finiteCountMaybeNext++instance (TestEquality w, FiniteWitness w) => Searchable (AnyW w) where+    search = finiteSearch++instance (TestEquality w, FiniteWitness w) => Finite (AnyW w) where+    assemble ::+           forall b f. Applicative f+        => (AnyW w -> f b)+        -> f (AnyW w -> b)+    assemble afb =+        fmap (\(MkAllF wtcb) (MkAnyW wt) -> getConst $ wtcb wt) $ assembleWitnessF $ \wt -> fmap Const $ afb $ MkAnyW wt+    allValues = getConst $ assembleWitnessF $ \wt -> Const [MkAnyW wt]++allWitnesses :: FiniteWitness w => [AnyW w]+allWitnesses = getConst $ assembleWitnessF $ \wt -> Const [MkAnyW wt]++instance (FiniteWitness w, AllWitnessConstraint Show w, WitnessConstraint Show w) => Show (AllValue w) where+    show (MkAllValue wtt) = let+        showItem :: AnyW w -> String+        showItem (MkAnyW wt) =+            showAllWitness wt +++            " -> " +++            case witnessConstraint @_ @Show wt of+                Dict -> show (wtt wt)+        in "{" ++ intercalate "," (fmap showItem allWitnesses) ++ "}"++assembleWitness :: (FiniteWitness w, Applicative m) => (forall t. w t -> m t) -> m (AllValue w)+assembleWitness wtmt = fmap allFToAllValue $ assembleWitnessF $ \wt -> fmap Identity $ wtmt wt
+ src/Data/Witness/HList.hs view
@@ -0,0 +1,267 @@+module Data.Witness.HList where++import Control.Applicative+import Control.Category+import Control.Category.Tensor+import Data.Constraint (Dict(..))+import Data.Functor.Identity as Import+import Data.Kind+import Data.Type.Equality+import Data.Witness.Either+import Data.Witness.List+import Data.Witness.ListElement+import Prelude hiding ((.), id)+import Unsafe.Coerce++type family HList (w :: [Type]) = (r :: Type) | r -> w where+    HList '[] = ()+    HList (t : tt) = (t, HList tt)++-- workaround for https://gitlab.haskell.org/ghc/ghc/issues/10833+injectiveHList ::+       forall (a :: [Type]) (b :: [Type]). HList a ~ HList b+    => a :~: b+injectiveHList = unsafeCoerce Refl++hListEq :: (forall a. w a -> Dict (Eq a)) -> ListType w t -> Dict (Eq (HList t))+hListEq _ NilListType = Dict+hListEq f (ConsListType t tt) =+    case (f t, hListEq f tt) of+        (Dict, Dict) -> Dict++hListShow :: (forall a. w a -> Dict (Show a)) -> ListType w t -> Dict (Show (HList t))+hListShow _ NilListType = Dict+hListShow f (ConsListType t tt) =+    case (f t, hListShow f tt) of+        (Dict, Dict) -> Dict++data HListWit (wit :: Type -> Type) (t :: Type) where+    MkHListWit :: forall (wit :: Type -> Type) (lt :: [Type]). ListType wit lt -> HListWit wit (HList lt)++listFill :: ListType w t -> (forall a. w a -> a) -> HList t+listFill NilListType _f = ()+listFill (ConsListType wa wr) f = (f wa, listFill wr f)++listMap :: ListType w t -> (forall a. w a -> a -> a) -> HList t -> HList 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) -> HList t -> HList t -> HList t+listLift2 NilListType _f () () = ()+listLift2 (ConsListType wa wr) f (a, resta) (b, restb) = (f wa a b, listLift2 wr f resta restb)++listIdentity :: ListType Identity lt -> HList lt+listIdentity NilListType = ()+listIdentity (ConsListType (Identity a) rest) = (a, listIdentity rest)++listSequence :: (Applicative f) => ListType f lt -> f (HList lt)+listSequence NilListType = pure ()+listSequence (ConsListType fa rest) = liftA2 (,) fa (listSequence rest)++getListElement :: ListElementType list t -> HList list -> t+getListElement FirstElementType = fst -- using fst and snd for irrefutable matching+getListElement (RestElementType lw) = getListElement lw . snd++putListElement :: ListElementType list t -> t -> HList list -> HList list+putListElement FirstElementType t (_, r) = (t, r)+putListElement (RestElementType lw) t (a, r) = (a, putListElement lw t r)++modifyListElement :: ListElementType list t -> (t -> t) -> HList list -> HList list+modifyListElement n aa t = putListElement n (aa (getListElement n t)) t++data AppendList w la lb = forall lr. MkAppendList+    { listAppendWitness :: ListType w lr+    , listAppend :: HList la -> HList lb -> HList lr+    , listSplit :: HList lr -> (HList la, HList 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 -> HList l -> HList lr+    , listSplitItem :: HList lr -> (a, HList 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) -> HList l -> HList lr+    , listUnmergeItem :: HList lr -> (a, HList 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) -> HList la -> HList lb -> HList lr+    , listUnmerge :: HList lr -> (HList la, HList 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))+                        }++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 (HList l) (HList 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 -> HList lr -> HList l+    , listRemove :: HList l -> HList 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 :: HList lx -> HList lr -> HList l+    , listRemoveMany :: HList l -> HList 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+                        }++data PartitionList wit1 wit2 l = forall l1 l2. MkPartitionList+    { listPartitionWitness1 :: ListType wit1 l1+    , listPartitionWitness2 :: ListType wit2 l2+    , listFromPartition :: HList l1 -> HList l2 -> HList l+    , listToPartition1 :: HList l -> HList l1+    , listToPartition2 :: HList l -> HList l2+    }++partitionList :: ListType (EitherType w1 w2) l -> PartitionList w1 w2 l+partitionList NilListType =+    MkPartitionList+        { listPartitionWitness1 = NilListType+        , listPartitionWitness2 = NilListType+        , listFromPartition = \() () -> ()+        , listToPartition1 = \() -> ()+        , listToPartition2 = \() -> ()+        }+partitionList (ConsListType (LeftType 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 (RightType 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/Kind.hs view
@@ -0,0 +1,80 @@+module Data.Witness.Kind where++import Data.Constraint+import Data.Kind+import Data.Witness.Constraint+import Data.Witness.Representative+import GHC.TypeLits+import Prelude++type family KindWitness k :: k -> Type++type InKind (a :: k) = Is (KindWitness k) a++inKind ::+       forall k (a :: k). InKind a+    => KindWitness k a+inKind = representative++-- NoWitness+data NoWitness (t :: k) =+    MkNoWitness++instance Representative NoWitness where+    getRepWitness MkNoWitness = Dict++instance Is NoWitness a where+    representative = MkNoWitness++-- Type+type instance KindWitness Type = NoWitness++-- Constraint+type instance KindWitness Constraint = NoWitness++-- Nat+type instance KindWitness Nat = NoWitness++-- kp -> kq+data FunctionKindWitness (wp :: kp -> Type) (wq :: kq -> Type) (t :: kp -> kq) where+    MkFunctionKindWitness+        :: forall kp kq (wp :: kp -> Type) (wq :: kq -> Type) (t :: kp -> kq).+           (forall (p :: kp). Is wp p => Is wq (t p))+        => FunctionKindWitness wp wq t++applyFunctionKindWitness ::+       forall kp kq (wp :: kp -> Type) (wq :: kq -> Type) (t :: kp -> kq) (p :: kp) (proxy :: kp -> Type). Is wp p+    => FunctionKindWitness wp wq t+    -> proxy p+    -> Dict (Is wq (t p))+applyFunctionKindWitness MkFunctionKindWitness _ = Dict++type instance KindWitness (kp -> kq) =+     FunctionKindWitness (KindWitness kp) (KindWitness kq)++instance forall kp kq (wp :: kp -> Type) (wq :: kq -> Type). Representative (FunctionKindWitness wp wq) {- Representative wq => -}+                                                                                                                                   where+    getRepWitness MkFunctionKindWitness = Dict++instance (forall p. Is wp p => Is wq (f p)) =>+             Is (FunctionKindWitness (wp :: kp -> Type) (wq :: kq -> Type)) (f :: kp -> kq) where+    representative = MkFunctionKindWitness++-- (kp,kq)+data PairWitness (wp :: kp -> Type) (wq :: kq -> Type) (t :: (kp, kq)) where+    MkPairWitness :: (Is wp p, Is wq q) => PairWitness wp wq '( p, q)++instance (Representative wp, Representative wq) => Representative (PairWitness wp wq) where+    getRepWitness MkPairWitness = Dict++instance (Is wp p, Is wq q) => Is (PairWitness wp wq) '( p, q) where+    representative = MkPairWitness++type instance KindWitness (kp, kq) =+     PairWitness (KindWitness kp) (KindWitness kq)++data AnyInKind (wit :: k -> Type) =+    forall (t :: k). InKind t => MkAnyInKind (wit t)++instance AllWitnessConstraint Show w => Show (AnyInKind w) where+    show (MkAnyInKind wa) = showAllWitness wa
src/Data/Witness/List.hs view
@@ -1,340 +1,73 @@-{-# OPTIONS -fno-warn-overlapping-patterns #-} module Data.Witness.List where-{-    import Prelude hiding (id,(.));-    import Data.Witness.Representative;-    import Data.Type.Equality;-    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.-    ;-    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)-    };+import Data.Constraint (Dict(..))+import Data.Functor.Identity+import Data.Kind+import Data.List (intercalate)+import Data.Nat+import Data.Type.Equality+import Data.Witness.Any+import Data.Witness.Representative+import Prelude hiding ((.), id) -    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));-                    };-                }-            };-        };-    };+-- | a witness type for lists of types+-- The @w@ parameter is the witness type of the elements.+data ListType (w :: k -> Type) (lt :: [k]) where+    NilListType :: ListType w '[]+    ConsListType :: w a -> ListType w lt -> ListType w (a : lt) -    type MapWitness cc w1 w2 = forall r v1. w1 v1 -> (forall v2. w2 v2 -> (cc v1 v2) -> r) -> r;+instance Representative w => Representative (ListType w) where+    getRepWitness NilListType = Dict+    getRepWitness (ConsListType w lw) =+        case (getRepWitness w, getRepWitness lw) of+            (Dict, Dict) -> Dict -    sameMapWitness :: (forall v. w v -> cc v v) -> MapWitness cc w w;-    sameMapWitness wc w wcr = wcr w (wc w);+instance Representative w => Is (ListType w) '[] where+    representative = NilListType -    data MapList cc w2 l = forall lr. MkMapList-    {-        listMapWitness :: ListType w2 lr,-        listMapW :: cc l lr-    };+instance (Is w a, Is (ListType w) lt) => Is (ListType w) (a : lt) where+    representative = ConsListType representative representative -    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'-        });-    };+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 -    data RemoveFromList w a l = forall lr. MkRemoveFromList-    {-        listRemoveWitness :: ListType w lr,-        listInsert :: a -> lr -> l,-        listRemove :: l -> lr-    };+instance (forall a. Show (w a)) => Show (ListType w lt) where+    show s = "[" <> intercalate "," (showAll s) <> "]"+      where+        showAll :: forall t. ListType w t -> [String]+        showAll NilListType = []+        showAll (ConsListType t1 tr) = show t1 : showAll tr -    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)-            };-        };-    };+assembleListType :: [AnyW w] -> AnyW (ListType w)+assembleListType [] = MkAnyW NilListType+assembleListType ((MkAnyW wa):ww) =+    case assembleListType ww of+        MkAnyW wwa -> MkAnyW $ ConsListType wa wwa -    data RemoveManyFromList wit lx l = forall lr. MkRemoveManyFromList-    {-        listRemoveManyWitness :: ListType wit lr,-        listInsertMany :: lx -> lr -> l,-        listRemoveMany :: l -> lr-    };+mapMListType :: Applicative m => (forall t'. wita t' -> m (witb t')) -> ListType wita t -> m (ListType witb t)+mapMListType _ff NilListType = pure NilListType+mapMListType ff (ConsListType t tt) = ConsListType <$> ff t <*> mapMListType ff tt -    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-            };-        };-    };+mapListType :: (forall t'. wita t' -> witb t') -> ListType wita t -> ListType witb t+mapListType ff l = runIdentity $ mapMListType (\wt -> Identity $ ff wt) l -    newtype EitherWitness (w1 :: k -> *) (w2 :: k -> *) (a :: k) = MkEitherWitness (Either (w1 a) (w2 a));+type family ListElement (n :: Nat) (list :: [k]) :: k where+    ListElement 'Zero (a : aa) = a+    ListElement ('Succ n) (a : aa) = ListElement n aa -    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;-    };+listTypeLength :: ListType w lt -> Int+listTypeLength NilListType = 0+listTypeLength (ConsListType _ lt) = succ $ listTypeLength lt -    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-    };+listTypeToList :: (forall a. w a -> r) -> ListType w t -> [r]+listTypeToList _wr NilListType = []+listTypeToList wr (ConsListType wa rest) = (wr wa) : (listTypeToList wr rest) -    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)-        };-    };-}+listTypeFor_ :: Applicative m => ListType w t -> (forall a. w a -> m ()) -> m ()+listTypeFor_ NilListType _ = pure ()+listTypeFor_ (ConsListType t tt) f = f t *> listTypeFor_ tt f
src/Data/Witness/ListElement.hs view
@@ -1,29 +1,49 @@ module Data.Witness.ListElement where-{-    import Data.Nat;-    import Data.Witness.Nat; -    class HasListElement (n :: Nat) (list :: *) where-    {-        type ListElement n list :: *;-        getListElement :: NatType n -> list -> ListElement n list;-        putListElement :: NatType n -> ListElement n list -> list -> list;-    };+import Data.Countable+import Data.Empty+import Data.Kind+import Data.Maybe+import Data.Searchable+import Data.Type.Equality+import Data.Witness.List+import Prelude -    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;+data ListElementType (kk :: [k]) (t :: k) where+    FirstElementType :: ListElementType (t : tt) t+    RestElementType :: ListElementType aa t -> ListElementType (a : aa) t -    instance HasListElement 'Zero (a,r) where-    {-        type ListElement 'Zero (a,r) = a;-        getListElement _ (a,_) = a;-        putListElement _ a (_,r) = (a,r);-    };+instance TestEquality (ListElementType tt) where+    testEquality FirstElementType FirstElementType = Just Refl+    testEquality (RestElementType lt1) (RestElementType lt2) = do+        Refl <- testEquality lt1 lt2+        return Refl+    testEquality _ _ = Nothing -    instance (HasListElement n r) => HasListElement ('Succ n) (a,r) where-    {-        type ListElement ('Succ n) (a,r) = ListElement n r;-        getListElement (SuccType n) (_,r) = getListElement n r;-        putListElement (SuccType n) a (f,r) = (f,putListElement n a r);-    };-}+instance Searchable (ListElementType '[] t) where+    search = finiteSearch++instance Eq (ListElementType tt t) where+    lt1 == lt2 = isJust $ testEquality lt1 lt2++instance Countable (ListElementType '[] t) where+    countPrevious = finiteCountPrevious+    countMaybeNext = finiteCountMaybeNext++instance Finite (ListElementType '[] t) where+    allValues = []++instance Empty (ListElementType '[] t) where+    never lt = case lt of {}++lookUpListElement ::+       forall k (w :: k -> Type) (t :: k) (lt :: [k]). TestEquality w+    => w t+    -> ListType w lt+    -> Maybe (ListElementType lt t)+lookUpListElement _ NilListType = Nothing+lookUpListElement wt (ConsListType wt' _)+    | Just Refl <- testEquality wt wt' = Just FirstElementType+lookUpListElement wt (ConsListType _ lt) = do+    et <- lookUpListElement wt lt+    return $ RestElementType et
src/Data/Witness/Nat.hs view
@@ -1,50 +1,81 @@ module Data.Witness.Nat where-{-    import Prelude hiding (id,(.));-    import Data.Maybe;-    import Data.Type.Equality;-    import Data.Constraint(Dict(..));-    import Data.Nat;-    import Data.Witness.Representative; -    data NatType (t :: Nat) where-    {-        ZeroType :: NatType 'Zero;-        SuccType :: NatType t -> NatType ('Succ t);-    };+import Data.Constraint (Dict(..))+import Data.Maybe+import Data.Nat+import Data.Type.Equality+import Data.Witness.Representative+import Prelude hiding ((.), id) -    instance TestEquality NatType where-    {-        testEquality ZeroType ZeroType = return Refl;-        testEquality (SuccType a) (SuccType b) = do-        {-            Refl <- testEquality a b;-            return Refl;-        };-        testEquality _ _ = Nothing;-    };+data NatType (t :: Nat) where+    ZeroType :: NatType 'Zero+    SuccType :: NatType t -> NatType ('Succ t) -    instance Eq1 NatType where-    {-        equals1 a b = isJust (testEquality a b);-    };+instance TestEquality NatType where+    testEquality ZeroType ZeroType = return Refl+    testEquality (SuccType a) (SuccType b) = do+        Refl <- testEquality a b+        return Refl+    testEquality _ _ = Nothing -    instance Representative NatType where-    {-        getRepWitness ZeroType = Dict;-        getRepWitness (SuccType n) = case getRepWitness n of-        {-            Dict -> Dict;-        };-    };+instance Representative NatType where+    getRepWitness ZeroType = Dict+    getRepWitness (SuccType n) =+        case getRepWitness n of+            Dict -> Dict -    instance Is NatType 'Zero where-    {-        representative = ZeroType;-    };+instance Is NatType 'Zero where+    representative = ZeroType -    instance (Is NatType n) => Is NatType ('Succ n) where-    {-        representative = SuccType representative;-    };-}+instance (Is NatType n) => Is NatType ('Succ n) where+    representative = SuccType representative++data GreaterEqual (a :: Nat) (b :: Nat) where+    ZeroGreaterEqual :: GreaterEqual a 'Zero+    SuccGreaterEqual :: GreaterEqual a b -> GreaterEqual ('Succ a) ('Succ b)++sameGreaterEqualWit :: NatType a -> GreaterEqual a a+sameGreaterEqualWit ZeroType = ZeroGreaterEqual+sameGreaterEqualWit (SuccType a) = SuccGreaterEqual $ sameGreaterEqualWit a++diff1GreaterEqualWit :: GreaterEqual a b -> GreaterEqual ('Succ a) b+diff1GreaterEqualWit ZeroGreaterEqual = ZeroGreaterEqual+diff1GreaterEqualWit (SuccGreaterEqual ge) = SuccGreaterEqual $ diff1GreaterEqualWit ge++natGreaterEqual :: NatType a -> NatType b -> Maybe (GreaterEqual a b)+natGreaterEqual _ ZeroType = return ZeroGreaterEqual+natGreaterEqual ZeroType _ = Nothing+natGreaterEqual (SuccType a) (SuccType b) = do+    al <- natGreaterEqual a b+    return $ SuccGreaterEqual al++type family Add (a :: Nat) (b :: Nat) :: Nat where+    Add 'Zero b = b+    Add ('Succ a) b = 'Succ (Add a b)++addWit :: NatType a -> NatType b -> NatType (Add a b)+addWit ZeroType b = b+addWit (SuccType a) b = SuccType $ addWit a b++addZeroWit :: NatType a -> Add a 'Zero :~: a+addZeroWit ZeroType = Refl+addZeroWit (SuccType a) =+    case addZeroWit a of+        Refl -> Refl++succAddWit' :: forall a b. NatType a -> 'Succ (Add a b) :~: Add a ('Succ b)+succAddWit' ZeroType = Refl+succAddWit' (SuccType a) =+    case succAddWit' @_ @b a of+        Refl -> Refl++succAddWit :: forall a b. NatType a -> NatType b -> 'Succ (Add a b) :~: Add a ('Succ b)+succAddWit a _ = succAddWit' @a @b a++addGreaterEqualWit :: NatType a -> NatType b -> GreaterEqual (Add a b) a+addGreaterEqualWit a ZeroType =+    case addZeroWit a of+        Refl -> sameGreaterEqualWit a+addGreaterEqualWit a (SuccType b) =+    case succAddWit a b of+        Refl -> diff1GreaterEqualWit $ addGreaterEqualWit a b
src/Data/Witness/Representative.hs view
@@ -1,64 +1,60 @@ 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;-    };+import Data.Constraint+import Data.Functor.Compose+import Data.Kind+import Data.Proxy+import Data.Type.Equality+import Data.Witness.Any -    instance Eq1 Proxy where-    {-        equals1 Proxy Proxy = True;-    };+isWitnessRepresentative :: Dict (Is rep a) -> rep a+isWitnessRepresentative Dict = representative -    isWitnessRepresentative :: Dict (Is rep a) -> rep a;-    isWitnessRepresentative Dict = representative;+type Subrepresentative (p :: k -> Type) (q :: k -> Type) = forall (a :: k). p a -> Dict (Is q a) -    class Eq1 rep => Representative (rep :: k -> *) where-    {-        -- | Every value is an instance of 'Is'.-        ;-        getRepWitness :: forall (a :: k). rep a -> Dict (Is rep a);-    };+withSubrepresentative :: Subrepresentative p q -> p a -> (Is q a => r) -> r+withSubrepresentative subrep pa f =+    case subrep pa of+        Dict -> f -    instance Representative Proxy where-    {-        getRepWitness Proxy = Dict;-    };+class Representative (rep :: k -> Type) where+    -- | Every value is an instance of 'Is'.+    getRepWitness :: Subrepresentative rep rep -    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;-    };+instance Representative Proxy where+    getRepWitness Proxy = Dict -    -- | 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;-    };+withRepresentative :: Representative rep => rep a -> (Is rep a => r) -> r+withRepresentative = withSubrepresentative getRepWitness -    instance Is Proxy a where-    {-        representative = Proxy;-    };+-- | If two representatives have the same type, then they have the same value.+class Representative rep => Is (rep :: k -> Type) (a :: k) where+    -- | The representative value for type @a@.+    representative :: rep a -    getRepresentative :: (Is rep a) => a -> rep a;-    getRepresentative _ = representative;+instance Is Proxy a where+    representative = Proxy -    rerepresentative :: (Is rep a) => p a -> rep a;-    rerepresentative _ = representative;+getRepresentative :: Is rep a => a -> rep a+getRepresentative _ = representative -    mkAny :: (Is rep a) => a -> Any rep;-    mkAny a = MkAny representative a;+rerepresentative :: Is rep a => p a -> rep a+rerepresentative _ = representative -    mkAnyF :: (Is rep a) => f a -> AnyF rep f;-    mkAnyF fa = MkAnyF representative fa;-}+mkAny :: Is rep a => a -> AnyValue rep+mkAny a = MkAnyValue representative a++mkAnyF :: Is rep a => f a -> AnyF rep f+mkAnyF fa = MkAnyF representative fa++instance Representative ((:~:) (t :: k)) where+    getRepWitness Refl = Dict++instance Is ((:~:) (t :: k)) (t :: k) where+    representative = Refl++instance Representative (Compose Dict c) where+    getRepWitness (Compose Dict) = Dict++instance c t => Is (Compose Dict c) t where+    representative = Compose Dict
+ src/Data/Witness/Single.hs view
@@ -0,0 +1,24 @@+{-# OPTIONS -fno-warn-orphans #-}++module Data.Witness.Single where++import Data.Constraint+import Data.Type.Equality+import Data.Witness.All+import Data.Witness.Constraint+import Data.Witness.Finite+import Prelude++type SingleType = (:~:)++instance FiniteWitness (SingleType t) where+    assembleWitnessF getsel = fmap (\ft -> MkAllF $ \Refl -> ft) $ getsel Refl++instance c t => WitnessConstraint c (SingleType t) where+    witnessConstraint Refl = Dict++singleAll :: t -> AllValue (SingleType t)+singleAll t = MkAllValue $ \Refl -> t++getSingleAll :: AllValue (SingleType t) -> t+getSingleAll (MkAllValue f) = f Refl
+ src/Data/Witness/Submap.hs view
@@ -0,0 +1,29 @@+module Data.Witness.Submap where++import Data.Kind+import Data.Witness.All+import Data.Witness.Any+import Data.Witness.Either+import Data.Witness.Finite+import Prelude++data SubmapWitness (w :: k -> Type) (f :: k -> Type) = MkSubmapWitness+    { subWitnessDomain :: [AnyW w]+    , subWitnessMap :: forall (t :: k). w t -> f t+    }++subWitnessCodomain :: SubmapWitness w f -> [AnyW f]+subWitnessCodomain schema = fmap (\(MkAnyW st) -> MkAnyW $ subWitnessMap schema st) $ subWitnessDomain schema++mapSubmapWitness :: (forall t. f1 t -> f2 t) -> SubmapWitness w f1 -> SubmapWitness w f2+mapSubmapWitness ff (MkSubmapWitness ai i) = MkSubmapWitness ai $ \s -> ff $ i s++eitherSubmapWitness ::+       SubmapWitness sel1 itemSchema -> SubmapWitness sel2 itemSchema -> SubmapWitness (EitherType sel1 sel2) itemSchema+eitherSubmapWitness (MkSubmapWitness a1 i1) (MkSubmapWitness a2 i2) =+    MkSubmapWitness+        ((fmap (mapAnyW LeftType) a1) ++ (fmap (mapAnyW RightType) a2))+        (getAllF $ eitherAllF (MkAllF i1) (MkAllF i2))++finiteSubmapWitness :: FiniteWitness w => (forall t. w t -> f t) -> SubmapWitness w f+finiteSubmapWitness wf = MkSubmapWitness allWitnesses wf
+ src/Data/Witness/Symbol.hs view
@@ -0,0 +1,45 @@+module Data.Witness.Symbol+    ( module Data.Witness.Symbol+    , Symbol+    , KnownSymbol+    ) where++import Data.Constraint+import Data.Proxy+import Data.Type.Equality+import Data.Witness.Constraint+import Data.Witness.Representative+import Data.Witness.WitnessValue+import GHC.TypeLits+import Prelude++data SymbolType (symbol :: Symbol) where+    MkSymbolType :: KnownSymbol symbol => SymbolType symbol++instance WitnessValue SymbolType where+    type WitnessValueType SymbolType = String+    witnessToValue :: forall t. SymbolType t -> String+    witnessToValue MkSymbolType = symbolVal (Proxy :: Proxy t)+    valueToWitness s cont =+        case someSymbolVal s of+            SomeSymbol p -> let+                psw :: forall (t :: Symbol). KnownSymbol t+                    => Proxy t+                    -> SymbolType t+                psw _ = MkSymbolType+                in cont $ psw p++instance TestEquality SymbolType where+    testEquality (MkSymbolType :: SymbolType a) (MkSymbolType :: SymbolType b) = sameSymbol (Proxy @a) (Proxy @b)++instance Representative SymbolType where+    getRepWitness MkSymbolType = Dict++instance KnownSymbol symbol => Is SymbolType symbol where+    representative = MkSymbolType++instance Show (SymbolType symbol) where+    show = witnessToValue++instance AllWitnessConstraint Show SymbolType where+    allWitnessConstraint = Dict
src/Data/Witness/WitnessDict.hs view
@@ -1,63 +1,55 @@ 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];+import Data.Kind+import Data.Maybe+import Data.Type.Equality+import Data.Witness.Any+import Prelude -    -- | An empty dictionary.-    ;-    emptyWitnessDict :: WitnessDict w;-    emptyWitnessDict = MkWitnessDict[];+-- | 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 :: Type -> Type) =+    MkWitnessDict [AnyValue w] -    -- | 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);+-- | An empty dictionary.+emptyWitnessDict :: WitnessDict w+emptyWitnessDict = MkWitnessDict [] -    -- | 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 _ _ = [];-    };+-- | 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 (matchAnyValue wit) cells) -    -- | 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);+-- | 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 ((MkAnyValue wit) . amap)) . (matchAnyValue 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 _ _ = [] -    -- | 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);+-- | 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) -    -- | 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 _ _ = [];-    };+-- | 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 ((MkAnyValue wit a) : cells) -    -- | Create a dictionary from a list of witness\/value pairs-    ;-    witnessDictFromList :: [Any w] -> WitnessDict w;-    witnessDictFromList = MkWitnessDict;-}+-- | 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 (\(MkAnyValue 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 :: [AnyValue w] -> WitnessDict w+witnessDictFromList = MkWitnessDict
src/Data/Witness/WitnessFDict.hs view
@@ -1,63 +1,55 @@ 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];+import Data.Kind+import Data.Maybe+import Data.Type.Equality+import Data.Witness.Any+import Prelude -    -- | An empty dictionary.-    ;-    emptyWitnessFDict :: WitnessFDict w f;-    emptyWitnessFDict = MkWitnessFDict [];+-- | 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 -> Type) (f :: k -> Type) =+    MkWitnessFDict [AnyF w f] -    -- | 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);+-- | An empty dictionary.+emptyWitnessFDict :: WitnessFDict w f+emptyWitnessFDict = MkWitnessFDict [] -    -- | 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 _ _ = [];-    };+-- | 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) -    -- | 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);+-- | 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 _ _ = [] -    -- | 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);+-- | 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) -    -- | 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 _ _ = [];-    };+-- | 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) -    -- | Create a dictionary from a list of witness\/value pairs-    ;-    witnessFDictFromList :: [AnyF w f] -> WitnessFDict w f;-    witnessFDictFromList = MkWitnessFDict;-}+-- | 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 :: [AnyF w f] -> WitnessFDict w f+witnessFDictFromList = MkWitnessFDict
+ src/Data/Witness/WitnessValue.hs view
@@ -0,0 +1,21 @@+module Data.Witness.WitnessValue where++import Data.Kind+import Data.Witness.Any++class WitnessValue (w :: k -> Type) where+    type WitnessValueType w :: Type+    witnessToValue :: forall (t :: k). w t -> WitnessValueType w+    valueToWitness :: forall r. WitnessValueType w -> (forall (t :: k). w t -> r) -> r++anyToValue ::+       forall k (w :: k -> Type). WitnessValue w+    => AnyW w+    -> WitnessValueType w+anyToValue (MkAnyW wt) = witnessToValue wt++valueToAny ::+       forall k (w :: k -> Type). WitnessValue w+    => WitnessValueType w+    -> AnyW w+valueToAny v = valueToWitness v MkAnyW
witness.cabal view
@@ -1,55 +1,64 @@-cabal-version:  >=1.14+cabal-version: 1.12++-- This file has been generated from package.yaml by hpack version 0.33.0.+--+-- see: https://github.com/sol/hpack+--+-- hash: 05878bc4862c4de5349ab302faa8396dafc84f16a102fdd267c48f3aae1e6319+ name:           witness-version:        0.4-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+version:        0.5 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>).+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+homepage:       https://github.com/AshleyYakeley/witness+bug-reports:    https://github.com/AshleyYakeley/witness/issues+author:         Ashley Yakeley+maintainer:     <ashley@semantic.org>+copyright:      (c) 2017-2019 Ashley Yakeley+license:        BSD3+license-file:   LICENSE build-type:     Simple  library-    hs-source-dirs: src-    default-language: Haskell98-    default-extensions:-        MultiParamTypeClasses-        RankNTypes-        FlexibleContexts-        TypeOperators-        FlexibleInstances-        EmptyDataDecls-        KindSignatures-        TypeFamilies-        GADTs-        PolyKinds-        DataKinds-        ScopedTypeVariables-        PatternGuards-        PatternSynonyms-    build-depends:-        base >= 4.7 && < 5,-        transformers,-        semigroupoids,-        constraints-    exposed-modules:-        Data.Nat-        Control.Category.Tensor-        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+  hs-source-dirs:+      src+  default-extensions: AllowAmbiguousTypes Arrows ConstraintKinds DataKinds DefaultSignatures EmptyCase EmptyDataDecls ExistentialQuantification FlexibleContexts FlexibleInstances ForeignFunctionInterface FunctionalDependencies GADTs GeneralizedNewtypeDeriving ImplicitParams NoImplicitPrelude InstanceSigs KindSignatures LambdaCase MultiParamTypeClasses OverloadedLabels OverloadedStrings PartialTypeSignatures PatternGuards PatternSynonyms PolyKinds QuantifiedConstraints RankNTypes RecordWildCards RecursiveDo ScopedTypeVariables StandaloneDeriving NoStarIsType TemplateHaskell TypeApplications TypeFamilies TypeFamilyDependencies TypeInType TypeOperators TypeSynonymInstances UndecidableInstances UndecidableSuperClasses ViewPatterns+  ghc-options: -Wall -Wincomplete-uni-patterns -Wincomplete-record-updates -Wcompat -Wnoncanonical-monad-instances+  build-depends:+      base >=4.14 && <5+    , constraints+    , countable+    , semigroupoids+    , transformers+  exposed-modules:+      Data.Type.With+      Data.Type.Apply+      Data.Type.Heterogeneous+      Data.Nat+      Control.Category.Tensor+      Data.Witness.Kind+      Data.Witness.Any+      Data.Witness.All+      Data.Witness.Constraint+      Data.Witness.WitnessValue+      Data.Witness.Symbol+      Data.Witness.Finite+      Data.Witness.Single+      Data.Witness.Cons+      Data.Witness.Either+      Data.Witness.Submap+      Data.Witness.WitnessDict+      Data.Witness.WitnessFDict+      Data.Witness.Nat+      Data.Witness.BigNat+      Data.Witness.ListElement+      Data.Witness.List+      Data.Witness.Concat+      Data.Witness.ApplyStack+      Data.Witness.HList+      Data.Witness.Representative+      Data.Witness+  other-modules:+      Paths_witness+  default-language: Haskell2010