rename WeakenN -> SWChain, move & export internals

This is so cool :)

CHANGELOG.md

@@ -1,3 +1,9 @@
+## 0.12.0 (unreleased)
+* rename `WeakenN` to `SWChain`
+* 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

src/Strongweak.hs

@@ -10,10 +10,12 @@ module Strongweak
 
   -- * Classes
     Weaken(..)
+  , weakenN
   , Strengthen(..)
+  , strengthenN
 
   -- * Other definitions
-  , WeakenN(..)
+  , SWChain(..)
   , SWCoercibly(..)
   , liftWeakF
 
@@ -27,7 +29,7 @@ module Strongweak
 import Strongweak.Weaken
 import Strongweak.Strengthen
 import Strongweak.Strength
-import Strongweak.WeakenN
+import Strongweak.Chain
 
 {- $strongweak-instance-design
 

src/Strongweak/Chain.hs

@@ -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/Strength.hs

@@ -5,7 +5,7 @@ module Strongweak.Strength where
 import Strongweak.Weaken ( type Weakened )
 import Data.Kind ( type Type )
 
-import Strongweak.WeakenN
+import Strongweak.Chain
 import GHC.TypeNats ( type Natural )
 
 -- | Strength enumeration: it's either strong, or weak.
@@ -30,5 +30,5 @@ type family SW (s :: Strength) a :: Type where
     SW Strong a =          a
     SW Weak   a = Weakened a
 
--- | Shortcut for a 'SW'-wrapped 'WeakenN'.
-type SWN (s :: Strength) (n :: Natural) a = SW s (WeakenN n a)
+-- | Shortcut for a 'SW'-wrapped 'SWChain'.
+type SWN (s :: Strength) (n :: Natural) a = SW s (SWChain n a)

src/Strongweak/Strengthen.hs

@@ -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
@@ -46,6 +49,11 @@ import Data.Bits ( FiniteBits )
 
 import Data.Typeable ( Typeable, TypeRep, typeRep, Proxy(Proxy) )
 
+-- 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
@@ -250,3 +258,22 @@ f .> g = g . f
 
 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/Weaken.hs

@@ -1,9 +1,11 @@
 {-# LANGUAGE UndecidableInstances #-} -- for WeakenedN
+{-# LANGUAGE AllowAmbiguousTypes #-} -- for weakenN
 
 module Strongweak.Weaken
   (
     Weaken(Weakened, weaken)
   , type WeakenedN
+  , WeakenN(weakenN)
   , liftWeakF
   , SWCoercibly(..)
   ) where
@@ -20,6 +22,8 @@ import Data.List.NonEmpty qualified as NonEmpty
 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.
@@ -128,3 +132,23 @@ instance (Weaken a, Weaken b) => Weaken (Either a b) where
     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

strongweak.cabal

@@ -30,6 +30,7 @@ source-repository head
 library
   exposed-modules:
       Strongweak
+      Strongweak.Chain
       Strongweak.Generic
       Strongweak.Strength
       Strongweak.Strengthen
@@ -38,8 +39,6 @@ library
       Strongweak.Util.TypeNats
       Strongweak.Weaken
       Strongweak.Weaken.Generic
-      Strongweak.WeakenN
-      Strongweak.WeakenN.Internal
   other-modules:
       Paths_strongweak
   hs-source-dirs: