witness 0.6.2 → 0.7

raw patch · 22 files changed

+96/−45 lines, 22 filesdep ~basedep ~constraintsdep ~containersPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base, constraints, containers

API changes (from Hackage documentation)

Files

• changelog.md +6/−0
• src/Data/PeanoNat.hs +1/−1
• src/Data/Type/Witness/General/HetConstraint.hs +1/−0
• src/Data/Type/Witness/General/Order.hs +1/−0
• src/Data/Type/Witness/General/TestHetEquality.hs +1/−0
• src/Data/Type/Witness/Specific/All.hs +5/−0
• src/Data/Type/Witness/Specific/Either.hs +2/−1
• src/Data/Type/Witness/Specific/Empty.hs +2/−1
• src/Data/Type/Witness/Specific/FiniteAllFor.hs +1/−0
• src/Data/Type/Witness/Specific/FixedList.hs +1/−0
• src/Data/Type/Witness/Specific/List/Element.hs +3/−2
• src/Data/Type/Witness/Specific/List/List.hs +7/−2
• src/Data/Type/Witness/Specific/List/Product.hs +28/−1
• src/Data/Type/Witness/Specific/List/Sum.hs +4/−1
• src/Data/Type/Witness/Specific/Natural.hs +1/−0
• src/Data/Type/Witness/Specific/OrderedWitnessMap/For.hs +3/−2
• src/Data/Type/Witness/Specific/Pair.hs +1/−0
• src/Data/Type/Witness/Specific/PeanoNat.hs +3/−0
• src/Data/Type/Witness/Specific/Some.hs +2/−1
• src/Data/Type/Witness/Specific/Symbol.hs +1/−0
• src/Data/Type/Witness/Specific/WitnessMap/For.hs +2/−1
• witness.cabal +20/−32

@@ -1,3 +1,9 @@+## [0.7] - UNRELEASED+- listProductSequence, matchListProduct+- sequenceComposeListType+- mapAllFor+- fix for GHC 9.10+ ## [0.6.2] - 2023-07-25 - withAllConstraint, withSomeAllConstraint - listTypeToListM, listTypeForList, listTypeFind

@@ -43,4 +43,4 @@ type ListLength :: forall k. [k] -> PeanoNat type family ListLength l where     ListLength '[] = 'Zero-    ListLength (a ': aa) = 'Succ (ListLength aa)+    ListLength (_ ': aa) = 'Succ (ListLength aa)

@@ -3,6 +3,7 @@ import Import  type HetConstraintWitness :: forall k1. (k1 -> Constraint) -> forall k2. k2 -> Type+type role HetConstraintWitness representational nominal data HetConstraintWitness c t where     MkHetConstraintWitness         :: forall k (c :: k -> Constraint) (t :: k). c t

@@ -2,6 +2,7 @@  import Import +type role WOrdering nominal nominal data WOrdering (a :: k) (b :: k) where     WLT :: forall k (a :: k) (b :: k). WOrdering a b     WEQ :: forall k (a :: k). WOrdering a a

@@ -20,6 +20,7 @@  -- | Equivalent to ':~~:', but can be made an instance of 'TestHetEquality' type HetEqual :: forall ka. ka -> forall kb. kb -> Type+type role HetEqual nominal nominal data HetEqual a b where     HetRefl :: forall k (a :: k). HetEqual a a 

@@ -5,11 +5,16 @@ import Import  type AllFor :: forall k. (k -> Type) -> (k -> Type) -> Type+type role AllFor representational representational newtype AllFor f w = MkAllFor     { unAllFor :: forall t. w t -> f t     } +mapAllFor :: (forall a. f1 a -> f2 a) -> AllFor f1 w -> AllFor f2 w+mapAllFor ff (MkAllFor wtft) = MkAllFor $ ff . wtft+ type AllOf :: (Type -> Type) -> Type+type role AllOf representational newtype AllOf w = MkAllOf     { unAllOf :: forall t. w t -> t     }

@@ -10,6 +10,7 @@ import Import  type EitherType :: forall k. (k -> Type) -> (k -> Type) -> (k -> Type)+type role EitherType representational representational nominal data EitherType w1 w2 t     = LeftType (w1 t)     | RightType (w2 t)@@ -71,7 +72,7 @@ type ConsType a = EitherType (SingleType a)  instance ListElementWitness lt => ListElementWitness (ConsType a lt) where-    type WitnessTypeList (ConsType a lt) = a : (WitnessTypeList lt)+    type WitnessTypeList (ConsType a lt) = a ': (WitnessTypeList lt)     toListElementWitness (LeftType Refl) = FirstElementType     toListElementWitness (RightType sel) = RestElementType $ toListElementWitness sel     fromListElementWitness FirstElementType = LeftType Refl

@@ -9,9 +9,10 @@ import Import  type EmptyType :: forall k. k -> Type+type role EmptyType phantom newtype EmptyType t =     MkEmptyType Void-    deriving (Eq, Countable, Searchable, Empty)+    deriving newtype (Eq, Countable, Searchable, Empty)  instance Finite (EmptyType t) where     allValues = []

@@ -7,6 +7,7 @@ import Import  type FiniteAllFor :: forall k. (k -> Type) -> (k -> Type) -> Type+type role FiniteAllFor representational representational data FiniteAllFor f w = MkFiniteAllFor     { finiteDomain :: [Some w]     , finiteGetAllFor :: forall t. w t -> f t

@@ -7,6 +7,7 @@ import Import  type FixedList :: PeanoNat -> Type -> Type+type role FixedList nominal representational data FixedList n a where     NilFixedList :: FixedList 'Zero a     ConsFixedList :: a -> FixedList n a -> FixedList ('Succ n) a

@@ -8,9 +8,10 @@ import Import  type ListElementType :: forall k. [k] -> k -> Type+type role ListElementType nominal nominal data ListElementType kk t where-    FirstElementType :: ListElementType (t : tt) t-    RestElementType :: ListElementType aa t -> ListElementType (a : aa) t+    FirstElementType :: ListElementType (t ': tt) t+    RestElementType :: ListElementType aa t -> ListElementType (a ': aa) t  instance TestEquality (ListElementType tt) where     testEquality FirstElementType FirstElementType = Just Refl

@@ -11,9 +11,10 @@ -- | a witness type for lists of types -- The @w@ parameter is the witness type of the elements. type ListType :: (k -> Type) -> ([k] -> Type)+type role ListType representational nominal data ListType w lt where     NilListType :: ListType w '[]-    ConsListType :: w a -> ListType w lt -> ListType w (a : lt)+    ConsListType :: w a -> ListType w lt -> ListType w (a ': lt)  instance Representative w => Representative (ListType w) where     getRepWitness NilListType = Dict@@ -24,7 +25,7 @@ instance Representative w => Is (ListType w) '[] where     representative = NilListType -instance (Is w a, Is (ListType w) lt) => Is (ListType w) (a : lt) where+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@@ -111,3 +112,7 @@     case f a of         Just r -> Just r         Nothing -> listTypeFind f aa++sequenceComposeListType :: Applicative f => ListType (Compose f w) lt -> f (ListType w lt)+sequenceComposeListType NilListType = pure NilListType+sequenceComposeListType (ConsListType (Compose fwa) tt) = liftA2 ConsListType fwa $ sequenceComposeListType tt

@@ -1,16 +1,19 @@+{-# OPTIONS -Wno-redundant-constraints #-}+ module Data.Type.Witness.Specific.List.Product where  import Data.Type.Witness.General.Representative import Data.Type.Witness.General.WitnessConstraint import Data.Type.Witness.Specific.List.Element import Data.Type.Witness.Specific.List.List+import Data.Type.Witness.Specific.Some import Import import Unsafe.Coerce  type ListProduct :: [Type] -> Type type family ListProduct w = r | r -> w where     ListProduct '[] = ()-    ListProduct (t : tt) = (t, ListProduct tt)+    ListProduct (t ': tt) = (t, ListProduct tt)  -- | workaround for https://gitlab.haskell.org/ghc/ghc/issues/10833 injectiveListProduct ::@@ -61,7 +64,31 @@ listProductModifyElement :: ListElementType list t -> (t -> t) -> ListProduct list -> ListProduct list listProductModifyElement n aa t = listProductPutElement n (aa (listProductGetElement n t)) t +listProductSequence ::+       forall f list. Applicative f+    => ListType f list+    -> f (ListProduct list)+listProductSequence NilListType = pure ()+listProductSequence (ConsListType t tt) = liftA2 (,) t $ listProductSequence tt++pickListProduct :: TestEquality w => ListType w lta -> w b -> Maybe (ListProduct lta -> b)+pickListProduct NilListType _ = Nothing+pickListProduct (ConsListType wa _) wb+    | Just Refl <- testEquality wa wb = Just fst+pickListProduct (ConsListType _ la) wb = fmap (\f -> f . snd) $ pickListProduct la wb++matchListProduct ::+       TestEquality w => ListType w lta -> ListType w ltb -> Either (Some w) (ListProduct lta -> ListProduct ltb)+matchListProduct _ NilListType = return $ \_ -> ()+matchListProduct la (ConsListType wb lb) =+    case pickListProduct la wb of+        Nothing -> Left $ MkSome wb+        Just f1 -> do+            fr <- matchListProduct la lb+            return $ \pa -> (f1 pa, fr pa)+ type ListProductType :: (Type -> Type) -> (Type -> Type)+type role ListProductType representational nominal data ListProductType wit t where     MkListProductType         :: forall (wit :: Type -> Type) (lt :: [Type]). ListType wit lt -> ListProductType wit (ListProduct lt)

@@ -1,3 +1,5 @@+{-# OPTIONS -Wno-redundant-constraints #-}+ module Data.Type.Witness.Specific.List.Sum where  import Data.Type.Witness.General.Representative@@ -9,7 +11,7 @@ type ListSum :: [Type] -> Type type family ListSum w = r | r -> w where     ListSum '[] = Void-    ListSum (t : tt) = Either t (ListSum tt)+    ListSum (t ': tt) = Either t (ListSum tt)  -- | workaround for https://gitlab.haskell.org/ghc/ghc/issues/10833 injectiveListSum ::@@ -35,6 +37,7 @@ mapListSum (ConsListType _wa wr) f (Right rest) = Right $ mapListSum wr f rest  type ListSumType :: (Type -> Type) -> (Type -> Type)+type role ListSumType representational nominal data ListSumType wit t where     MkListSumType :: forall (wit :: Type -> Type) (lt :: [Type]). ListType wit lt -> ListSumType wit (ListSum lt) 

@@ -30,6 +30,7 @@ import Unsafe.Coerce  type NaturalType :: Nat -> Type+type role NaturalType nominal data NaturalType bn where     MkNaturalType :: KnownNat bn => NaturalType bn 

@@ -1,6 +1,6 @@ module Data.Type.Witness.Specific.OrderedWitnessMap.For where -import qualified Data.Map as Map+import Data.Map qualified as Map import Data.Type.Witness.General.Order import Data.Type.Witness.Specific.Some import Import@@ -8,9 +8,10 @@ -- | 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. type OrderedWitnessMapFor :: forall k. (k -> Type) -> (k -> Type) -> Type+type role OrderedWitnessMapFor representational nominal newtype OrderedWitnessMapFor f w =     MkOrderedWitnessMapFor (Map.Map (Some w) (SomeFor f w))-    deriving (Semigroup, Monoid)+    deriving newtype (Semigroup, Monoid)  -- | An empty dictionary. emptyOrderedWitnessMapFor :: TestOrder w => OrderedWitnessMapFor f w

@@ -7,6 +7,7 @@  -- | a witness for pairs of witnesses type PairType :: (k -> Type) -> (k -> Type) -> (k -> Type)+type role PairType representational representational nominal data PairType w1 w2 t =     MkPairType (w1 t)                (w2 t)

@@ -7,6 +7,7 @@ import Import  type PeanoNatType :: PeanoNat -> Type+type role PeanoNatType nominal data PeanoNatType t where     ZeroType :: PeanoNatType 'Zero     SuccType :: PeanoNatType t -> PeanoNatType ('Succ t)@@ -49,6 +50,7 @@     valueToWitness (Succ n) cont = valueToWitness n $ \t -> cont $ SuccType t  type GreaterEqual :: PeanoNat -> PeanoNat -> Type+type role GreaterEqual nominal nominal data GreaterEqual a b where     ZeroGreaterEqual :: GreaterEqual a 'Zero     SuccGreaterEqual :: GreaterEqual a b -> GreaterEqual ('Succ a) ('Succ b)@@ -100,6 +102,7 @@         Refl -> diff1GreaterEqual $ addPeanoNatTypeGE a b  type Greater :: PeanoNat -> PeanoNat -> Type+type role Greater nominal nominal data Greater a b where     MkGreater :: GreaterEqual a b -> Greater ('Succ a) b 

@@ -7,6 +7,7 @@  -- | Any value with a witness to a parameter of its type. type SomeFor :: forall k. (k -> Type) -> (k -> Type) -> Type+type role SomeFor representational representational data SomeFor f w =     forall a. MkSomeFor (w a)                         (f a)@@ -50,7 +51,7 @@     return a  type Some :: forall k. (k -> Type) -> Type-type Some = SomeFor (Const ())+type Some @k = SomeFor @k (Const ())  pattern MkSome :: w a -> Some w 

@@ -12,6 +12,7 @@ import Import  type SymbolType :: Symbol -> Type+type role SymbolType nominal data SymbolType symbol where     MkSymbolType :: KnownSymbol symbol => SymbolType symbol 

@@ -6,9 +6,10 @@ -- | 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. type WitnessMapFor :: forall k. (k -> Type) -> (k -> Type) -> Type+type role WitnessMapFor representational representational newtype WitnessMapFor f w = MkWitnessMapFor     { witnessMapForToList :: [SomeFor f w]-    } deriving (Semigroup, Monoid)+    } deriving newtype (Semigroup, Monoid)  -- | An empty dictionary. emptyWitnessMapFor :: WitnessMapFor f w

@@ -1,25 +1,32 @@ cabal-version: 2.2 --- This file has been generated from package.yaml by hpack version 0.35.2.+-- This file has been generated from package.yaml by hpack version 0.37.0. -- -- see: https://github.com/sol/hpack  name:           witness-version:        0.6.2+version:        0.7 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 a wide variety of witness types. It also provides classes for /representatives/, which are values that represent types. category:       Data-homepage:       https://github.com/AshleyYakeley/witness+homepage:       https://github.com/AshleyYakeley/witness#readme bug-reports:    https://github.com/AshleyYakeley/witness/issues author:         Ashley Yakeley maintainer:     <ashley@semantic.org>-copyright:      (c) 2017-2022 Ashley Yakeley+copyright:      (c) 2017-2024 Ashley Yakeley license:        BSD-2-Clause license-file:   LICENSE build-type:     Simple-extra-source-files:+tested-with:+    GHC == 9.8.4+  , GHC == 9.10.1+extra-doc-files:     changelog.md +source-repository head+  type: git+  location: https://github.com/AshleyYakeley/witness+ library   exposed-modules:       Data.Type.Witness.Apply@@ -62,52 +69,33 @@   default-extensions:       AllowAmbiguousTypes       Arrows-      ConstraintKinds       DataKinds       DefaultSignatures-      EmptyCase-      EmptyDataDecls-      ExistentialQuantification-      FlexibleContexts-      FlexibleInstances-      ForeignFunctionInterface+      DerivingStrategies       FunctionalDependencies-      GADTs-      GeneralizedNewtypeDeriving       ImplicitParams       NoImplicitPrelude-      InstanceSigs-      KindSignatures       LambdaCase-      MultiParamTypeClasses       OverloadedLabels       OverloadedStrings       PartialTypeSignatures-      PatternGuards       PatternSynonyms-      PolyKinds       QuantifiedConstraints-      RankNTypes       RecordWildCards       RecursiveDo-      ScopedTypeVariables-      StandaloneDeriving-      StandaloneKindSignatures+      RoleAnnotations       NoStarIsType       TemplateHaskell-      TypeApplications+      TypeAbstractions       TypeFamilies       TypeFamilyDependencies-      TypeInType-      TypeOperators-      TypeSynonymInstances       UndecidableInstances       UndecidableSuperClasses       ViewPatterns-  ghc-options: -Wall -Wincomplete-uni-patterns -Wincomplete-record-updates -Wcompat -Wnoncanonical-monad-instances+  ghc-options: -Weverything -Wno-missing-import-lists -Wno-missing-export-lists -Wno-unsafe -Wno-missing-safe-haskell-mode -Wno-missing-kind-signatures -Wno-partial-type-signatures -Wno-monomorphism-restriction -Wno-missing-local-signatures -Wno-partial-fields -Wno-all-missed-specialisations -Wno-missed-specialisations   build-depends:-      base >=4.16 && <5-    , constraints >=0.13-    , containers >=0.4+      base >=4.19 && <5+    , constraints >=0.14+    , containers >=0.6     , countable >=1.2-  default-language: Haskell2010+  default-language: GHC2021