packages feed

strongweak 0.9.1 → 0.12.0

raw patch · 14 files changed

Files

CHANGELOG.md view
@@ -1,3 +1,19 @@+## 0.12.0 (2025-03-29)+* rename `WeakenN` to `SWChain`+* remove `SWN`, don't like+* export previous `SWChain` internals `weakenN` and `strengthenN` for magical+  strongweak chaining (!)+  * no need to write `weaken . weaken . weaken` when `weakenN @3` will do!++## 0.11.0 (2024-10-17)+* add `WeakenN` and `SWN` for chaining weakenings+* clarify instance design: even zero-invariant coercible newtypes aren't allowed+  to recursively weaken their inner type!++## 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
README.md view
@@ -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:
src/Strongweak.hs view
@@ -10,9 +10,13 @@    -- * Classes     Weaken(..)+  , weakenN   , Strengthen(..)+  , strengthenN    -- * Other definitions+  , SWChain(..)+  , SWCoercibly(..)   , liftWeakF    -- * Strength switch wrapper@@ -23,10 +27,12 @@  import Strongweak.Weaken import Strongweak.Strengthen+import Strongweak.Strength+import Strongweak.Chain  {- $strongweak-instance-design -A given strong type @a@ has exactly one associated weak type @'Weak' a@.+A given strong type @a@ has exactly one associated weak type @'Weakened' a@. Multiple strong types may weaken to the same weak type.  The following laws must hold:@@ -43,6 +49,12 @@   * Most (all?) instances should handle (relax or assert) a single invariant.   * Most instances should not have a recursive context. +If you want to handle multiple invariants, chain the weakens/strengthens.+You may do this by nesting 'SW' uses, but you will then have to write your own+instances, as the generics cannot handle such chaining. Alternatively, you may+use 'WeakenN'. This will add another newtype layer to the strong representation,+but the generics are happy with it.+ Some types may not have any invariants which may be usefully relaxed e.g. @'Either' a b@. For these, you may write a recursive instance that weakens/strengthens "through" the type e.g. @('Weak' a, 'Weak' b) => Weak@@ -56,5 +68,4 @@ a @'Weak' a = a, weaken = id@ overlapping instance, which I do not want. On the other hand, @[a]@ /does/ weaken to @['Weak' a]@, because there are no invariants present to remove, so decomposing is all the user could hope to do.- -}
+ src/Strongweak/Chain.hs view
@@ -0,0 +1,45 @@+module Strongweak.Chain ( SWChain(..), strengthenN ) where++import Strongweak.Weaken ( Weaken(..), WeakenN(weakenN), type WeakenedN )+import Strongweak.Strengthen ( Strengthen(..), StrengthenN(strengthenN) )+import GHC.TypeNats ( type Natural )++{- | When weakening (or strengthening), chain the operation @n@ times.++You may achieve this without extra newtypes by nesting uses of+'Strongweak.Strength.SW'. However, strongweak generics can't handle this,+forcing you to write manual instances.++'SWChain' provides this nesting behaviour in a type. In return for adding a+boring newtype layer to the strong representation, you can chain weakening and+strengthenings without having to write them manually.++The type works as follows:++@+'Weakened' ('SWChain' 0 a) = a+'Weakened' ('SWChain' 1 a) = 'Weakened' a+'Weakened' ('SWChain' 2 a) = 'Weakened' ('Weakened' a)+'Weakened' ('SWChain' n a) = 'WeakenedN' n a+@++And so on. (This type is only much use from @n = 2@ onwards.)++You may also use this as a "via" type:++@+newtype A (s :: 'Strength') = A { a1 :: 'SW' s (Identity ('SW' s Word8)) }+deriving via 'SWChain' 2 (Identity Word8) instance     'Weaken' (A 'Strong')+deriving via 'SWChain' 2 (Identity Word8) instance 'Strengthen' (A 'Strong')+@+-}+newtype SWChain (n :: Natural) a = SWChain { unSWChain :: a }+    deriving stock Show+    deriving (Ord, Eq) via a++instance WeakenN n a => Weaken (SWChain n a) where+    type Weakened (SWChain n a) = WeakenedN n a+    weaken = weakenN @n . unSWChain++instance StrengthenN n a => Strengthen (SWChain n a) where+    strengthen = fmap SWChain . strengthenN @n
src/Strongweak/Generic.hs view
@@ -11,18 +11,21 @@     weakenGeneric   , strengthenGeneric -  -- * Generic wrapper+  -- * Generic deriving via wrappers   , GenericallySW(..)+  , GenericallySW0(..)   ) where  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 ) +import Strongweak.Strength+ {- $generic-derivation-compatibility  The 'Strengthen' and 'Weaken' generic derivers allow you to derive instances@@ -30,11 +33,9 @@    * Both types' generic representation (the SOP tree structure) match exactly.   * For each leaf pair of types, either the types are identical, or the-  appropriate instance exists to transform from source to target.+    appropriate instance exists to transform from source to target. -If they aren't compatible, the derivation will fail with a type error. I'm-fairly certain that if it succeeds, your instance is guaranteed correct-(assuming the instances it uses internally are all OK!).+If they aren't compatible, the derivation will fail with a type error.  I don't think GHC strongly guarantees the SOP property, so if you receive surprising derivation errors, the types might have differing generic@@ -46,6 +47,11 @@ types: for the datatype, constructors and selectors. GHC will always add this metadata for you, but manually-derived Generic instances (which are usually a bad idea) do not require it.++Note that the generics only handle one "layer" at a time. If you have a data+type with nested 'Strongweak.Strengthen.SW' uses, these generics will fail with+a type error. Either use 'Strongweak.WeakenN.WeakenN', or write the instances+manually. -}  {- | @DerivingVia@ wrapper for strongweak instances.@@ -67,19 +73,15 @@ deriving via (GenericallySW (XYZ 'Strong) (XYZ 'Weak)) instance Strengthen (XYZ 'Strong) @ -TODO can't figure out a way around multiple standalone deriving declarations :(--TODO maybe GenericallySW1? but even so instances differ between weaken and-strengthen (weaken needs nothing) so it's kinda better this way. :)+Regrettably, use of this requires UndecidableInstances. -}- newtype GenericallySW s (w :: Type) = GenericallySW { unGenericallySW :: s }  instance   ( 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@@ -88,3 +90,25 @@   , Weaken (GenericallySW s w)   ) => Strengthen (GenericallySW s w) where     strengthen = fmap GenericallySW . strengthenGeneric++-- | 'GenericallySW' where the type takes a 'Strength' in its last type var.+--+-- Shorter instances for types of a certain shape.+--+-- Regrettably, use of this requires UndecidableInstances.+newtype GenericallySW0 (f :: Strength -> Type)+  = GenericallySW0 { unGenericallySW0 :: f Strong }++instance+  ( Generic (f Strong), Generic (f Weak)+  , GWeaken (Rep (f Strong)) (Rep (f Weak))+  ) => Weaken (GenericallySW0 f) where+    type Weakened (GenericallySW0 f) = f Weak+    weaken = weakenGeneric . unGenericallySW0++instance+  ( Generic (f Strong), Generic (f Weak)+  , GStrengthenD (Rep (f Weak)) (Rep (f Strong))+  , Weaken (GenericallySW0 f)+  ) => Strengthen (GenericallySW0 f) where+    strengthen = fmap GenericallySW0 . strengthenGeneric
+ src/Strongweak/Strength.hs view
@@ -0,0 +1,28 @@+-- | Definitions using a type-level strength switch.++module Strongweak.Strength where++import Strongweak.Weaken ( type Weakened )+import Data.Kind ( type Type )++-- | Strength enumeration: it's either strong, or weak.+--+-- Primarily interesting at the type level (using DataKinds).+data Strength = Strong | Weak++{- | Get either the strong or weak representation of a type, depending on the+     type-level "switch" provided.++This is intended to be used in data types that take a 'Strength' type. Define+your type using strong fields wrapped in @SW s@. You then get the weak+representation for free, using the same definition.++@+data A (s :: Strength) = A+  { a1 :: SW s Word8+  , a2 :: String }+@+-}+type family SW (s :: Strength) a :: Type where+    SW Strong a =          a+    SW Weak   a = Weakened a
src/Strongweak/Strengthen.hs view
@@ -1,11 +1,14 @@ {-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE AllowAmbiguousTypes #-} -- StrengthenN, and typeRep'+-- StrengthenN type families in constraints+{-# LANGUAGE UndecidableInstances #-}  module Strongweak.Strengthen   (   -- * 'Strengthen' class     Strengthen(..)   , restrengthen+  , StrengthenN(strengthenN)    -- ** Helpers   , strengthenBounded@@ -17,11 +20,16 @@   , failStrengthen    -- * Re-exports-  , Strongweak.Weaken.Weak+  , Strongweak.Weaken.Weakened   ) where +import Strongweak.Weaken ( Weaken(Weakened) )++import Strongweak.Weaken ( Weaken(weaken) )++import Strongweak.Weaken ( SWCoercibly(..) )+ import Strongweak.Util.TypeNats ( natVal'' )-import Strongweak.Weaken ( Weaken(..) )  import GHC.TypeNats ( KnownNat ) import Data.Word@@ -41,8 +49,13 @@  import Data.Typeable ( Typeable, TypeRep, typeRep, Proxy(Proxy) ) -{- | Attempt to strengthen some @'Weak' a@, asserting certain invariants.+-- for strengthenN+import GHC.TypeNats ( type Natural, type (-) )+import Strongweak.Weaken ( type WeakenedN, WeakenN )+import Unsafe.Coerce ( unsafeCoerce ) +{- | Attempt to strengthen some @'Weakened' a@, asserting certain invariants.+ We take 'Weaken' as a superclass in order to maintain strong/weak type pair consistency. We choose this dependency direction because we treat the strong type as the "canonical" one, so 'Weaken' is the more natural (and@@ -52,9 +65,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. --@@ -101,6 +114,15 @@ failStrengthen1 :: [text] -> Either (StrengthenFailure text) a failStrengthen1 t = failStrengthen t [] +-- TODO add a via type for obtaining strengthen via unsafestrengthen :)+-- should be permitted only for non-failing, zero invariant strengthens++instance Strengthen (SWCoercibly a) where+    strengthen = Right . SWCoercibly++deriving via SWCoercibly a instance Strengthen (Identity a)+deriving via SWCoercibly a instance Strengthen (Const a b)+ -- | Strengthen a type by refining it with a predicate. instance Refine p a => Strengthen (Refined p a) where     strengthen = refine .> \case@@ -140,14 +162,6 @@             , "fail: wrong length (got "<>TBL.fromDec (length as)<>")" ]       where n = natVal'' @n --- | Add wrapper.-instance Strengthen (Identity a) where-    strengthen = Right . Identity---- | Add wrapper.-instance Strengthen (Const a b) where-    strengthen = Right . Const- {- TODO controversial. seems logical, but also kinda annoying. instance (Show a, Typeable a) => Strengthen (Maybe a) where     strengthen = \case [a] -> pure $ Just a@@ -199,7 +213,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@@ -244,3 +258,22 @@  typeRep' :: forall a. Typeable a => TypeRep typeRep' = typeRep (Proxy @a)++class WeakenN n a => StrengthenN (n :: Natural) a where+    strengthenN :: WeakenedN n a -> Either StrengthenFailure' a++instance {-# OVERLAPPING #-} StrengthenN 0 a where+    strengthenN = Right++instance (Strengthen a, StrengthenN (n-1) (Weakened a))+  => StrengthenN n a where+    strengthenN a =+        case strengthenN @(n-1) @(Weakened a) (weakenedNLR1 @n @a a) of+          Left  e  -> Left e+          Right sa -> strengthen sa++-- | Inductive 'WeakenedN' case.+--+-- @n@ must not be 0.+weakenedNLR1 :: forall n a. WeakenedN n a -> WeakenedN (n-1) (Weakened a)+weakenedNLR1 = unsafeCoerce
src/Strongweak/Strengthen/Generic.hs view
@@ -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
src/Strongweak/Strengthen/Unsafe.hs view
@@ -1,19 +1,21 @@ module Strongweak.Strengthen.Unsafe where -import Strongweak.Weaken+import Strongweak.Weaken ( Weaken(Weakened) ) import Data.Word import Data.Int import Rerefined.Refine import Data.Vector.Generic.Sized qualified as VGS -- Shazbot! import Data.Vector.Generic qualified as VG import Data.Vector.Generic.Sized.Internal qualified-import Data.Functor.Identity-import Data.Functor.Const import Data.List.NonEmpty qualified as NonEmpty import Data.List.NonEmpty ( NonEmpty ) -{- | Unsafely transform a @'Weak' a@ to an @a@, without asserting invariants.+import Strongweak.Weaken ( SWCoercibly(..) )+import Data.Functor.Identity+import Data.Functor.Const +{- | 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,9 +33,15 @@ 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 +instance UnsafeStrengthen (SWCoercibly a) where+    unsafeStrengthen = SWCoercibly++deriving via SWCoercibly a instance UnsafeStrengthen (Identity a)+deriving via SWCoercibly a instance UnsafeStrengthen (Const a b)+ -- | Add a refinement to a type without checking the associated predicate. instance UnsafeStrengthen (Refined p a) where     unsafeStrengthen = unsafeRefine@@ -46,14 +54,6 @@ instance VG.Vector v a => UnsafeStrengthen (VGS.Vector v n a) where     unsafeStrengthen =         Data.Vector.Generic.Sized.Internal.Vector . VG.fromList---- | Add wrapper.-instance UnsafeStrengthen (Identity a) where-    unsafeStrengthen = Identity---- | Add wrapper.-instance UnsafeStrengthen (Const a b) where-    unsafeStrengthen = Const  {- TODO controversial. seems logical, but also kinda annoying. -- | Unsafely grab either 0 or 1 elements from a list.
src/Strongweak/Weaken.hs view
@@ -1,15 +1,13 @@-{-# LANGUAGE UndecidableInstances #-} -- for SWDepth+{-# LANGUAGE UndecidableInstances #-} -- for WeakenedN+{-# LANGUAGE AllowAmbiguousTypes #-} -- for weakenN  module Strongweak.Weaken   (-  -- * 'Weaken' class-    Weaken(..)+    Weaken(Weakened, weaken)+  , type WeakenedN+  , WeakenN(weakenN)   , liftWeakF--  -- * Strength switch helper-  , Strength(..)-  , type SW-  , type SWDepth+  , SWCoercibly(..)   ) where  import Rerefined@@ -24,128 +22,143 @@ import Data.List.NonEmpty ( NonEmpty ) import GHC.TypeNats +import Unsafe.Coerce ( unsafeCoerce )+ {- | Weaken some @a@, relaxing certain invariants.  See "Strongweak" for class design notes and laws. -} class Weaken a where     -- | The weakened type for some type.-    type Weak a :: Type--    -- | Weaken some @a@ to its associated weak type @'Weak' a@.-    weaken :: a -> Weak a+    type Weakened a :: Type --- | Strength enumeration: is it strong, or weak?------ Primarily interesting at the type level (using DataKinds).-data Strength = Strong | Weak+    -- | Weaken some @a@ to its associated weak type @'Weakened' a@.+    weaken :: a -> Weakened a  -- | 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-     type-level "switch" provided.+-- | The type of @a@ after weakening @n@ times.+type family WeakenedN (n :: Natural) a :: Type where+    WeakenedN 0 a = a+    WeakenedN n a = Weakened (WeakenedN (n-1) a) -This is intended to be used in data types that take a 'Strength' type. Define-your type using strong fields wrapped in @SW s@. You then get the weak-representation for free, using the same definition.+{- | A "via type" newtype for defining strongweak instances for zero-invariant,+     coercible newtypes. +Use like so:+ @-data A (s :: Strength) = A-  { a1 :: SW s Word8-  , a2 :: String }+deriving 'Weaken' via 'SWCoercibly' a @++Or standalone:++@+via 'SWCoercibly' a instance 'Weaken' ('Identity' a)+@++Note that usage of this incurs UndecidableInstances. That's life. You can+write the trivial instances this generates yourself if you so wish. -}-type family SW (s :: Strength) a :: Type where-    SW 'Strong a = a-    SW 'Weak   a = Weak a+newtype SWCoercibly a = SWCoercibly { unSWCoercibly :: a }+instance Weaken (SWCoercibly a) where+    type Weakened (SWCoercibly a) = a+    weaken = unSWCoercibly --- | 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)+deriving via SWCoercibly a instance Weaken (Identity a)+deriving via SWCoercibly a instance Weaken (Const a b)  -- | 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-    weaken = runIdentity---- | Strip wrapper.-instance Weaken (Const a b) where-    type Weak (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++class WeakenN (n :: Natural) a where+    weakenN :: a -> WeakenedN n a++-- | Zero case: return the value as-is.+instance {-# OVERLAPPING #-} WeakenN 0 a where+    weakenN = id++-- | Inductive case. @n /= 0@, else this explodes.+instance (Weaken a, WeakenN (n-1) (Weakened a))+  => WeakenN n a where+    weakenN a =+        case weakenN @(n-1) @(Weakened a) (weaken a) of+          x -> weakenedNRL1 @n @a x++-- | Inverted inductive 'WeakenedN'case.+--+-- @n@ must not be 0.+weakenedNRL1 :: forall n a. WeakenedN (n-1) (Weakened a) -> WeakenedN n a+weakenedNRL1 = unsafeCoerce
src/Strongweak/Weaken/Generic.hs view
@@ -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.
strongweak.cabal view
@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           strongweak-version:        0.9.1+version:        0.12.0 synopsis:       Convert between strong and weak representations of types description:    Please see README.md. category:       Data@@ -30,7 +30,9 @@ library   exposed-modules:       Strongweak+      Strongweak.Chain       Strongweak.Generic+      Strongweak.Strength       Strongweak.Strengthen       Strongweak.Strengthen.Generic       Strongweak.Strengthen.Unsafe@@ -52,10 +54,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 +84,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 +93,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
test/Common.hs view
@@ -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
test/Strongweak/LawsSpec.hs view
@@ -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 ()