strongweak 0.9.1 → 0.10.0

raw patch · 11 files changed

+93/−87 lines, 11 filesdep ~rerefined

Dependency ranges changed: rerefined

Files

• CHANGELOG.md +4/−0
• README.md +10/−8
• src/Strongweak/Generic.hs +2/−2
• src/Strongweak/Strengthen.hs +5/−5
• src/Strongweak/Strengthen/Generic.hs +1/−1
• src/Strongweak/Strengthen/Unsafe.hs +4/−4
• src/Strongweak/Weaken.hs +38/−38
• src/Strongweak/Weaken/Generic.hs +1/−1
• strongweak.cabal +5/−5
• test/Common.hs +20/−20
• test/Strongweak/LawsSpec.hs +3/−3

@@ -1,3 +1,7 @@+## 0.10.0 (2024-10-13)+* rename `Weak` to `Weakened`, to separate from `Weak :: Strength`+* update rerefined dependency+ ## 0.9.1 (2024-10-01) * update rerefined dependency 

@@ -37,8 +37,8 @@  Let's formalize the above as a pair of types `S` and `W`. -  * Given a `strong :: S`, we can always turn it into a `weak :: W`.-  * Given a `weak :: W`, we can only turn it into a `strong :: S` if it passes+  * given a `strong :: S`, we can always turn it into a `weak :: W`+  * given a `weak :: W`, we can only turn it into a `strong :: S` if it passes     all the checks  We can write these as pure functions.@@ -57,8 +57,8 @@   * `Word8` is a bounded natural number. `Natural` can represent any natural     number. So `Natural` is a weak type, which can be strengthened into `Word8`     (or `Word16`, `Word32`, ...) by asserting well-boundedness.-  * `[a]` doesn't have state any predicates. But we could weaken every `a` in-    the list. So `[a]` is a strong type, which can be weakened to `[Weak a]`.+  * `[a]` doesn't state any predicates. But we could weaken every `a` in the+    list. So `[a]` is a strong type, which can be weakened to `[Weak a]`.   * `NonEmpty a` *does* have a predicate. For useability and other reasons, we     only handle this predicate, and don't also weaken each `a` like above.     `NonEmpty a` weakens to `[a]`.@@ -77,13 +77,11 @@  ```haskell class Weaken a where-    type Weak a :: Type+    type Weakened a :: Type     weaken :: a :: Weak a -type Result = Validation Fails-type Fails = NeAcc Fail class Weaken a => Strengthen a where-    strengthen :: Weak a -> Result a+    strengthen :: Weakened a -> Either Failure a ```  Note that a strong type may have only one associated weak type. The same weak@@ -139,6 +137,10 @@ strengthening may fail while weakening cannot. For safe conversion enumeration via typeclasses, consider Taylor Fausak's [witch](https://hackage.haskell.org/package/witch) library.++### Not a generic `coerce`+strongweak isn't intended for automatic `coerce`ing between pairs of types.+For that, check out `gcoerce` at Lysxia's generic-data package.  ### Not particularly speedy The emphasis is on safety, which may come at the detriment of performance:

@@ -18,7 +18,7 @@ import Strongweak.Weaken.Generic import Strongweak.Strengthen.Generic -import Strongweak.Weaken ( Weaken(Weak, weaken) )+import Strongweak.Weaken ( Weaken(Weakened, weaken) ) import Strongweak.Strengthen ( Strengthen(strengthen) ) import GHC.Generics import Data.Kind ( Type )@@ -79,7 +79,7 @@   ( Generic s, Generic w   , GWeaken (Rep s) (Rep w)   ) => Weaken (GenericallySW s w) where-    type Weak (GenericallySW s w) = w+    type Weakened (GenericallySW s w) = w     weaken = weakenGeneric . unGenericallySW  instance

@@ -17,11 +17,11 @@   , failStrengthen    -- * Re-exports-  , Strongweak.Weaken.Weak+  , Strongweak.Weaken.Weakened   ) where  import Strongweak.Util.TypeNats ( natVal'' )-import Strongweak.Weaken ( Weaken(..) )+import Strongweak.Weaken ( Weaken(Weakened, weaken) )  import GHC.TypeNats ( KnownNat ) import Data.Word@@ -52,9 +52,9 @@ See "Strongweak" for class design notes and laws. -} class Weaken a => Strengthen a where-    -- | Attempt to strengthen some @'Weak' a@ to its associated strong type+    -- | Attempt to strengthen some @'Weakened' a@ to its associated strong type     --   @a@.-    strengthen :: Weak a -> Either StrengthenFailure' a+    strengthen :: Weakened a -> Either StrengthenFailure' a  -- | Weaken a strong value, then strengthen it again. --@@ -199,7 +199,7 @@     strengthen = strengthenList  -- TODO using reverse, SLOW!! >:(-strengthenList :: Strengthen a => [Weak a] -> Either StrengthenFailure' [a]+strengthenList :: Strengthen a => [Weakened a] -> Either StrengthenFailure' [a] strengthenList = goR (0 :: Int) [] . map strengthen   where     goR i as = \case

@@ -131,7 +131,7 @@  -- | Strengthen a field using the existing 'Strengthen' instance. instance-  ( Weak s ~ w -- has to be here, else "illegal typesym family app in instance"+  ( Weakened s ~ w -- required, else "illegal typesym family app in instance"   , Strengthen s   , ReifySelector i wmr smr   ) => GStrengthenS i

@@ -1,6 +1,6 @@ module Strongweak.Strengthen.Unsafe where -import Strongweak.Weaken+import Strongweak.Weaken ( Weaken(Weakened) ) import Data.Word import Data.Int import Rerefined.Refine@@ -12,7 +12,7 @@ import Data.List.NonEmpty qualified as NonEmpty import Data.List.NonEmpty ( NonEmpty ) -{- | Unsafely transform a @'Weak' a@ to an @a@, without asserting invariants.+{- | Unsafely transform a @'Weakened' a@ to an @a@, without asserting invariants.  Naturally, you must only even /consider/ using this if you have a guarantee that your value is safe to treat as strong.@@ -31,8 +31,8 @@ See "Strongweak" for class design notes and laws. -} class Weaken a => UnsafeStrengthen a where-    -- | Unsafely transform a @'Weak' a@ to its associated strong type @a@.-    unsafeStrengthen :: Weak a -> a+    -- | Unsafely transform a @'Weakened' a@ to its associated strong type @a@.+    unsafeStrengthen :: Weakened a -> a  -- | Add a refinement to a type without checking the associated predicate. instance UnsafeStrengthen (Refined p a) where

@@ -30,10 +30,10 @@ -} class Weaken a where     -- | The weakened type for some type.-    type Weak a :: Type+    type Weakened a :: Type -    -- | Weaken some @a@ to its associated weak type @'Weak' a@.-    weaken :: a -> Weak a+    -- | Weaken some @a@ to its associated weak type @'Weakened' a@.+    weaken :: a -> Weakened a  -- | Strength enumeration: is it strong, or weak? --@@ -42,7 +42,7 @@  -- | Lift a function on a weak type to the associated strong type by weakening --   first.-liftWeakF :: Weaken a => (Weak a -> b) -> (a -> b)+liftWeakF :: Weaken a => (Weakened a -> b) -> (a -> b) liftWeakF f = f . weaken  {- | Get either the strong or weak representation of a type, depending on the@@ -59,93 +59,93 @@ @ -} type family SW (s :: Strength) a :: Type where-    SW 'Strong a = a-    SW 'Weak   a = Weak a+    SW Strong a =          a+    SW Weak   a = Weakened a  -- | Track multiple levels of weakening. Silly thought I had, don't think it's --   useful. type family SWDepth (n :: Natural) a :: Type where     SWDepth 0 a = a-    SWDepth n a = Weak (SWDepth (n-1) a)+    SWDepth n a = Weakened (SWDepth (n-1) a)  -- | Strip refined type refinement.-instance Weaken (Refined p a) where-    type Weak (Refined p a) = a+instance Weaken   (Refined p a) where+    type Weakened (Refined p a) = a     weaken = unrefine  -- | Strip refined functor type refinement.-instance Weaken (Refined1 p f a) where-    type Weak (Refined1 p f a) = f a+instance Weaken   (Refined1 p f a) where+    type Weakened (Refined1 p f a) = f a     weaken = unrefine1  -- | Weaken non-empty lists into plain lists.-instance Weaken (NonEmpty a) where-    type Weak (NonEmpty a) = [a]+instance Weaken   (NonEmpty a) where+    type Weakened (NonEmpty a) = [a]     weaken = NonEmpty.toList  -- | Weaken sized vectors into plain lists. instance VG.Vector v a => Weaken (VGS.Vector v n a) where-    type Weak (VGS.Vector v n a) = [a]+    type Weakened (VGS.Vector v n a) = [a]     weaken = VGS.toList  -- | Strip wrapper.-instance Weaken (Identity a) where-    type Weak (Identity a) = a+instance Weaken   (Identity a) where+    type Weakened (Identity a) = a     weaken = runIdentity  -- | Strip wrapper.-instance Weaken (Const a b) where-    type Weak (Const a b) = a+instance Weaken   (Const a b) where+    type Weakened (Const a b) = a     weaken = getConst  {- TODO controversial. seems logical, but also kinda annoying. -- | Weaken 'Maybe' (0 or 1) into '[]' (0 to n). instance Weaken (Maybe a) where-    type Weak (Maybe a) = [a]+    type Weakened (Maybe a) = [a]     weaken = \case Just a  -> [a]                    Nothing -> [] -}  -- Weaken the bounded Haskell numeric types using 'fromIntegral'.-instance Weaken Word8  where-    type Weak Word8  = Natural+instance Weaken   Word8  where+    type Weakened Word8  = Natural     weaken = fromIntegral-instance Weaken Word16 where-    type Weak Word16 = Natural+instance Weaken   Word16 where+    type Weakened Word16 = Natural     weaken = fromIntegral-instance Weaken Word32 where-    type Weak Word32 = Natural+instance Weaken   Word32 where+    type Weakened Word32 = Natural     weaken = fromIntegral-instance Weaken Word64 where-    type Weak Word64 = Natural+instance Weaken   Word64 where+    type Weakened Word64 = Natural     weaken = fromIntegral-instance Weaken Int8   where-    type Weak Int8   = Integer+instance Weaken   Int8   where+    type Weakened Int8   = Integer     weaken = fromIntegral-instance Weaken Int16  where-    type Weak Int16  = Integer+instance Weaken   Int16  where+    type Weakened Int16  = Integer     weaken = fromIntegral-instance Weaken Int32  where-    type Weak Int32  = Integer+instance Weaken   Int32  where+    type Weakened Int32  = Integer     weaken = fromIntegral-instance Weaken Int64  where-    type Weak Int64  = Integer+instance Weaken   Int64  where+    type Weakened Int64  = Integer     weaken = fromIntegral  --------------------------------------------------------------------------------  -- | Decomposer. Weaken every element in a list. instance Weaken a => Weaken [a] where-    type Weak [a] = [Weak a]+    type Weakened [a] = [Weakened a]     weaken = map weaken  -- | Decomposer. Weaken both elements of a tuple. instance (Weaken a, Weaken b) => Weaken (a, b) where-    type Weak (a, b) = (Weak a, Weak b)+    type Weakened (a, b) = (Weakened a, Weakened b)     weaken (a, b) = (weaken a, weaken b)  -- | Decomposer. Weaken either side of an 'Either'. instance (Weaken a, Weaken b) => Weaken (Either a b) where-    type Weak (Either a b) = Either (Weak a) (Weak b)+    type Weakened (Either a b) = Either (Weakened a) (Weakened b)     weaken = \case Left  a -> Left  $ weaken a                    Right b -> Right $ weaken b

@@ -32,7 +32,7 @@     gweaken = id  -- | Weaken a field using the existing 'Weaken' instance.-instance (Weaken s, Weak s ~ w) => GWeaken (Rec0 s) (Rec0 w) where+instance (Weaken s, Weakened s ~ w) => GWeaken (Rec0 s) (Rec0 w) where     gweaken = K1 . weaken . unK1  -- | Weaken product types by weakening left and right.

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           strongweak-version:        0.9.1+version:        0.10.0 synopsis:       Convert between strong and weak representations of types description:    Please see README.md. category:       Data@@ -52,10 +52,10 @@       TypeFamilies       DataKinds       MagicHash-  ghc-options: -Wall -Wno-unticked-promoted-constructors+  ghc-options: -fhide-source-paths -Wall   build-depends:       base >=4.18 && <5-    , rerefined >=0.6.0 && <0.7+    , rerefined >=0.8.0 && <0.9     , text >=2.0 && <2.2     , text-builder-linear >=0.1.3 && <0.2     , vector >=0.12.3.1 && <0.14@@ -82,7 +82,7 @@       TypeFamilies       DataKinds       MagicHash-  ghc-options: -Wall -Wno-unticked-promoted-constructors+  ghc-options: -fhide-source-paths -Wall   build-tool-depends:       hspec-discover:hspec-discover >=2.7 && <2.12   build-depends:@@ -91,7 +91,7 @@     , generic-random >=1.5.0.1 && <1.6     , hspec >=2.7 && <2.12     , quickcheck-instances >=0.3.26 && <0.4-    , rerefined >=0.6.0 && <0.7+    , rerefined >=0.8.0 && <0.9     , strongweak     , text >=2.0 && <2.2     , text-builder-linear >=0.1.3 && <0.2

@@ -14,42 +14,42 @@  data DS (s :: Strength)   = DS0 (SW s Word8) (SW s Word8) Word8 (SW s Word8) (SW s Word8)-  | DS1 (SW s (Refined (CompareValue LT Pos 100) Natural))+  | DS1 (SW s (Refined (CompareValue RelOpLT Pos 100) Natural))     deriving stock (Generic) -deriving stock instance Eq   (DS 'Strong)-deriving stock instance Show (DS 'Strong)-deriving via (GenericArbitraryU `AndShrinking` (DS 'Strong)) instance Arbitrary (DS 'Strong)+deriving stock instance Eq   (DS Strong)+deriving stock instance Show (DS Strong)+deriving via (GenericArbitraryU `AndShrinking` (DS Strong)) instance Arbitrary (DS Strong) -deriving stock instance Eq   (DS 'Weak)-deriving stock instance Show (DS 'Weak)-deriving via (GenericArbitraryU `AndShrinking` (DS 'Weak))   instance Arbitrary (DS 'Weak)+deriving stock instance Eq   (DS Weak)+deriving stock instance Show (DS Weak)+deriving via (GenericArbitraryU `AndShrinking` (DS Weak))   instance Arbitrary (DS Weak) -instance Weaken (DS 'Strong) where-    type Weak   (DS 'Strong) = DS 'Weak+instance Weaken   (DS Strong) where+    type Weakened (DS Strong) = DS Weak     weaken = weakenGeneric-instance Strengthen (DS 'Strong) where strengthen = strengthenGeneric+instance Strengthen (DS Strong) where strengthen = strengthenGeneric  data DP (s :: Strength) = DP   { dp1f0 :: SW s Word32-  , dp1f1 :: SW s (Refined (CompareValue GT Pos 42) Natural)+  , dp1f1 :: SW s (Refined (CompareValue RelOpGT Pos 42) Natural)   , dp1f2 :: SW s Word8   , dp1f3 :: Word8   , dp1f4 :: SW s Word8   } deriving stock (Generic) -deriving stock instance Eq   (DP 'Strong)-deriving stock instance Show (DP 'Strong)-deriving via (GenericArbitraryU `AndShrinking` (DP 'Strong)) instance Arbitrary (DP 'Strong)+deriving stock instance Eq   (DP Strong)+deriving stock instance Show (DP Strong)+deriving via (GenericArbitraryU `AndShrinking` (DP Strong)) instance Arbitrary (DP Strong) -deriving stock instance Eq   (DP 'Weak)-deriving stock instance Show (DP 'Weak)-deriving via (GenericArbitraryU `AndShrinking` (DP 'Weak))   instance Arbitrary (DP 'Weak)+deriving stock instance Eq   (DP Weak)+deriving stock instance Show (DP Weak)+deriving via (GenericArbitraryU `AndShrinking` (DP Weak))   instance Arbitrary (DP Weak) -instance Weaken     (DP 'Strong) where-    type Weak (DP 'Strong) = DP 'Weak+instance Weaken   (DP Strong) where+    type Weakened (DP Strong) = DP Weak     weaken = weakenGeneric-instance Strengthen (DP 'Strong) where strengthen = strengthenGeneric+instance Strengthen (DP Strong) where strengthen = strengthenGeneric  tryStrengthenSuccessEq :: Eq a => a -> Either StrengthenFailure' a -> Bool tryStrengthenSuccessEq a = \case Right a' -> a == a'; Left{} -> False

@@ -8,11 +8,11 @@ spec :: Spec spec = modifyMaxSize (+1000) $ do     prop "weaken-strengthen roundtrip isomorphism (generic)" $ do-      \(d :: DS 'Strong) ->+      \(d :: DS Strong) ->         strengthen (weaken d) `shouldSatisfy` tryStrengthenSuccessEq d     prop "strengthen-weaken-strengthen roundtrip partial isomorphism (generic)" $ do-      \(dw :: DS 'Weak) ->-        case strengthen @(DS 'Strong) dw of+      \(dw :: DS Weak) ->+        case strengthen @(DS Strong) dw of           Right ds ->             strengthen (weaken ds) `shouldSatisfy` tryStrengthenSuccessEq ds           Left{}  -> pure ()