witness 0.6.1 → 0.6.2

raw patch · 8 files changed

+92/−47 lines, 8 filesdep ~basePVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• changelog.md +5/−0
• src/Data/PeanoNat.hs +0/−1
• src/Data/Type/Witness/General/AllConstraint.hs +9/−0
• src/Data/Type/Witness/Specific/FixedList.hs +15/−0
• src/Data/Type/Witness/Specific/List/List.hs +16/−3
• src/Data/Type/Witness/Specific/Natural.hs +0/−1
• src/Data/Type/Witness/Specific/Some.hs +8/−1
• witness.cabal +39/−41

@@ -1,3 +1,8 @@+## [0.6.2] - 2023-07-25+- withAllConstraint, withSomeAllConstraint+- listTypeToListM, listTypeForList, listTypeFind+- fixedListLength, fixedListGenerate, Eq FixedList+ ## [0.6.1] - 2022-09-12 - new ListLength type family and associated functions - new Greater type family and associated functions

@@ -2,7 +2,6 @@  import GHC.TypeNats import Import-import Numeric.Natural  -- | Inductive natural numbers. data PeanoNat

@@ -6,6 +6,15 @@ class AllConstraint c w where     allConstraint :: forall t. Dict (c (w t)) +withAllConstraint ::+       forall k (c :: Type -> Constraint) (w :: k -> Type) (a :: k) (r :: Type). AllConstraint c w+    => w a+    -> (c (w a) => r)+    -> r+withAllConstraint _ call =+    case allConstraint @Type @k @c @w @a of+        Dict -> call+ instance AllConstraint Show ((:~:) t) where     allConstraint = Dict 

@@ -35,6 +35,21 @@     sequenceA NilFixedList = pure NilFixedList     sequenceA (ConsFixedList fa l) = liftA2 ConsFixedList fa $ sequenceA l +instance Eq a => Eq (FixedList n a) where+    NilFixedList == NilFixedList = True+    (ConsFixedList a la) == (ConsFixedList b lb) =+        if a == b+            then la == lb+            else False++fixedListLength :: FixedList n a -> PeanoNatType n+fixedListLength NilFixedList = ZeroType+fixedListLength (ConsFixedList _ l) = SuccType $ fixedListLength l++fixedListGenerate :: Applicative m => PeanoNatType n -> m a -> m (FixedList n a)+fixedListGenerate ZeroType _ = pure NilFixedList+fixedListGenerate (SuccType n) ma = liftA2 ConsFixedList ma $ fixedListGenerate n ma+ fixedFromList :: [a] -> (forall n. PeanoNatType n -> FixedList n a -> r) -> r fixedFromList [] call = call ZeroType NilFixedList fixedFromList (a:aa) call = fixedFromList aa $ \n l -> call (SuccType n) $ ConsFixedList a l

@@ -78,10 +78,16 @@ listTypeToList _wr NilListType = [] listTypeToList wr (ConsListType wa rest) = (wr wa) : (listTypeToList wr rest) -listTypeFor :: Applicative m => ListType w t -> (forall a. w a -> m r) -> m [r]-listTypeFor NilListType _ = pure []-listTypeFor (ConsListType t tt) f = liftA2 (:) (f t) $ listTypeFor tt f+listTypeToListM :: Applicative m => (forall a. w a -> m r) -> ListType w t -> m [r]+listTypeToListM _ NilListType = pure []+listTypeToListM f (ConsListType t tt) = liftA2 (:) (f t) $ listTypeToListM f tt +listTypeFor :: Applicative m => ListType w1 t -> (forall a. w1 a -> m (w2 a)) -> m (ListType w2 t)+listTypeFor lt f = mapMListType f lt++listTypeForList :: Applicative m => ListType w t -> (forall a. w a -> m r) -> m [r]+listTypeForList lt f = listTypeToListM f lt+ 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@@ -98,3 +104,10 @@ listTypeFromFixedList NilFixedList call = call NilListType listTypeFromFixedList (ConsFixedList (MkSome wa) l) call =     listTypeFromFixedList l $ \rest -> call $ ConsListType wa rest++listTypeFind :: (forall a. w a -> Maybe r) -> ListType w tt -> Maybe r+listTypeFind _ NilListType = Nothing+listTypeFind f (ConsListType a aa) =+    case f a of+        Just r -> Just r+        Nothing -> listTypeFind f aa

@@ -27,7 +27,6 @@ import Data.Type.Witness.Specific.PeanoNat import GHC.TypeNats import Import-import Numeric.Natural import Unsafe.Coerce  type NaturalType :: Nat -> Type

@@ -71,8 +71,15 @@ instance forall k (w :: k -> Type). TestOrder w => Ord (Some w) where     compare (MkSome wa) (MkSome wb) = wOrderingToOrdering $ testCompare wa wb +withSomeAllConstraint ::+       forall k (c :: Type -> Constraint) (w :: k -> Type) (r :: Type). AllConstraint c w+    => Some w+    -> (forall a. c (w a) => w a -> r)+    -> r+withSomeAllConstraint (MkSome wa) call = withAllConstraint @k @c wa $ call wa+ instance forall k (w :: k -> Type). AllConstraint Show w => Show (Some w) where-    show (MkSome wa) = allShow wa+    show swa = withSomeAllConstraint @k @Show swa show  someForToSome :: SomeFor f w -> Some w someForToSome (MkSomeFor wa _) = MkSome wa

@@ -1,13 +1,11 @@ cabal-version: 2.2 --- This file has been generated from package.yaml by hpack version 0.34.4.+-- This file has been generated from package.yaml by hpack version 0.35.2. -- -- see: https://github.com/sol/hpack------ hash: aae0fd4e94350169efa7229b1559a55e3b9d2ed3d389f607534a15403307b6b1  name:           witness-version:        0.6.1+version:        0.6.2 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@@ -23,6 +21,42 @@     changelog.md  library+  exposed-modules:+      Data.Type.Witness.Apply+      Data.PeanoNat+      Data.Type.Witness.General.TestHetEquality+      Data.Type.Witness.General.HetConstraint+      Data.Type.Witness.Specific.Some+      Data.Type.Witness.Specific.All+      Data.Type.Witness.General.AllConstraint+      Data.Type.Witness.General.WitnessConstraint+      Data.Type.Witness.General.WitnessValue+      Data.Type.Witness.General.ListElement+      Data.Type.Witness.Specific.Symbol+      Data.Type.Witness.General.Finite+      Data.Type.Witness.Specific.Single+      Data.Type.Witness.Specific.Pair+      Data.Type.Witness.Specific.Empty+      Data.Type.Witness.Specific.Either+      Data.Type.Witness.Specific.FiniteAllFor+      Data.Type.Witness.Specific.WitnessMap.Of+      Data.Type.Witness.Specific.WitnessMap.For+      Data.Type.Witness.Specific.OrderedWitnessMap.Of+      Data.Type.Witness.Specific.OrderedWitnessMap.For+      Data.Type.Witness.Specific.PeanoNat+      Data.Type.Witness.Specific.Natural+      Data.Type.Witness.Specific.FixedList+      Data.Type.Witness.Specific.List.Element+      Data.Type.Witness.Specific.List.List+      Data.Type.Witness.Specific.Concat+      Data.Type.Witness.Specific.ApplyStack+      Data.Type.Witness.Specific.List.Product+      Data.Type.Witness.Specific.List.Sum+      Data.Type.Witness.General.Representative+      Data.Type.Witness.General.Order+      Data.Type.Witness+  other-modules:+      Import   hs-source-dirs:       src   default-extensions:@@ -72,44 +106,8 @@       ViewPatterns   ghc-options: -Wall -Wincomplete-uni-patterns -Wincomplete-record-updates -Wcompat -Wnoncanonical-monad-instances   build-depends:-      base >=4.15 && <5+      base >=4.16 && <5     , constraints >=0.13     , containers >=0.4     , countable >=1.2-  exposed-modules:-      Data.Type.Witness.Apply-      Data.PeanoNat-      Data.Type.Witness.General.TestHetEquality-      Data.Type.Witness.General.HetConstraint-      Data.Type.Witness.Specific.Some-      Data.Type.Witness.Specific.All-      Data.Type.Witness.General.AllConstraint-      Data.Type.Witness.General.WitnessConstraint-      Data.Type.Witness.General.WitnessValue-      Data.Type.Witness.General.ListElement-      Data.Type.Witness.Specific.Symbol-      Data.Type.Witness.General.Finite-      Data.Type.Witness.Specific.Single-      Data.Type.Witness.Specific.Pair-      Data.Type.Witness.Specific.Empty-      Data.Type.Witness.Specific.Either-      Data.Type.Witness.Specific.FiniteAllFor-      Data.Type.Witness.Specific.WitnessMap.Of-      Data.Type.Witness.Specific.WitnessMap.For-      Data.Type.Witness.Specific.OrderedWitnessMap.Of-      Data.Type.Witness.Specific.OrderedWitnessMap.For-      Data.Type.Witness.Specific.PeanoNat-      Data.Type.Witness.Specific.Natural-      Data.Type.Witness.Specific.FixedList-      Data.Type.Witness.Specific.List.Element-      Data.Type.Witness.Specific.List.List-      Data.Type.Witness.Specific.Concat-      Data.Type.Witness.Specific.ApplyStack-      Data.Type.Witness.Specific.List.Product-      Data.Type.Witness.Specific.List.Sum-      Data.Type.Witness.General.Representative-      Data.Type.Witness.General.Order-      Data.Type.Witness-  other-modules:-      Import   default-language: Haskell2010