packages feed

strongweak 0.11.0 → 0.12.0

raw patch · 9 files changed

+128/−114 lines, 9 files

Files

CHANGELOG.md view
@@ -1,3 +1,10 @@+## 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
src/Strongweak.hs view
@@ -10,24 +10,25 @@    -- * Classes     Weaken(..)+  , weakenN   , Strengthen(..)+  , strengthenN    -- * Other definitions-  , WeakenN(..)+  , SWChain(..)   , SWCoercibly(..)   , liftWeakF    -- * Strength switch wrapper   , Strength(..)   , type SW-  , type SWN    ) where  import Strongweak.Weaken import Strongweak.Strengthen import Strongweak.Strength-import Strongweak.WeakenN+import Strongweak.Chain  {- $strongweak-instance-design
+ 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/Strength.hs view
@@ -5,9 +5,6 @@ import Strongweak.Weaken ( type Weakened ) import Data.Kind ( type Type ) -import Strongweak.WeakenN-import GHC.TypeNats ( type Natural )- -- | Strength enumeration: it's either strong, or weak. -- -- Primarily interesting at the type level (using DataKinds).@@ -29,6 +26,3 @@ 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)
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@@ -46,6 +49,11 @@  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 @@  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 view
@@ -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 ( NonEmpty ) import GHC.TypeNats +import Unsafe.Coerce ( unsafeCoerce )+ {- | Weaken some @a@, relaxing certain invariants.  See "Strongweak" for class design notes and laws.@@ -41,14 +45,24 @@     WeakenedN 0 a = a     WeakenedN n a = Weakened (WeakenedN (n-1) a) --- | A "via type" newtype for defining strongweak instances for zero-invariant,---   coercible newtypes.------ Use like so:------ @--- deriving via 'SWCoercibly' a instance 'Weaken' ('Identity' a)--- @+{- | A "via type" newtype for defining strongweak instances for zero-invariant,+     coercible newtypes.++Use like so:++@+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.+-} newtype SWCoercibly a = SWCoercibly { unSWCoercibly :: a } instance Weaken (SWCoercibly a) where     type Weakened (SWCoercibly a) = a@@ -128,3 +142,23 @@     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/WeakenN.hs 
@@ -1,38 +0,0 @@-module Strongweak.WeakenN ( WeakenN(..) ) where--import Strongweak.WeakenN.Internal-import Strongweak.Weaken ( Weaken(..), type WeakenedN )-import Strongweak.Strengthen ( Strengthen(..) )-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.Weaken.SW'. However, strongweak generics can't handle this, forcing-you to write manual instances.--'WeakenN' 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 (WeakenN 0 a) = a-Weakened (WeakenN 1 a) = Weakened a-Weakened (WeakenN 2 a) = Weakened (Weakened a)-Weakened (WeakenN n a) = WeakenedN n a-@--And so on. (This type is only much use from @n = 2@ onwards.)--}-newtype WeakenN (n :: Natural) a = WeakenN { unWeakenN :: a }-    deriving stock Show-    deriving (Ord, Eq) via a--instance WeakenWeakenN n a => Weaken (WeakenN n a) where-    type Weakened (WeakenN n a) = WeakenedN n a-    weaken = weakenWeakenN @n @a . unWeakenN--instance StrengthenWeakenN n a => Strengthen (WeakenN n a) where-    strengthen = fmap WeakenN . strengthenWeakenN @n @a
− src/Strongweak/WeakenN/Internal.hs 
@@ -1,55 +0,0 @@-{-# LANGUAGE UndecidableInstances #-} -- type family 'Weakened' in constraints-{-# LANGUAGE AllowAmbiguousTypes #-} -- ambiguous intermediate type classes--{- | 'Strongweak.WeakenN.WeakenN' internals.--Just in case. You shouldn't need these, but they might be fun to look at.--__Internal module. Exports may change without warning. Try not to use.__--}--module Strongweak.WeakenN.Internal where--import Strongweak.Weaken ( Weaken(weaken), type WeakenedN )-import Strongweak.Strengthen-import GHC.TypeNats ( type Natural, type (-) )-import Unsafe.Coerce ( unsafeCoerce )--class WeakenWeakenN (n :: Natural) a where-    weakenWeakenN :: a -> WeakenedN n a---- | Zero case: return the value as-is.-instance {-# OVERLAPPING #-} WeakenWeakenN 0 a where-    weakenWeakenN = id---- | Inductive case. @n /= 0@, else this explodes.-instance (Weaken a, WeakenWeakenN (n-1) (Weakened a))-  => WeakenWeakenN n a where-    weakenWeakenN a =-        case weakenWeakenN @(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--class WeakenWeakenN n a => StrengthenWeakenN (n :: Natural) a where-    strengthenWeakenN :: WeakenedN n a -> Either StrengthenFailure' a--instance {-# OVERLAPPING #-} StrengthenWeakenN 0 a where-    strengthenWeakenN = Right--instance (Strengthen a, StrengthenWeakenN (n-1) (Weakened a))-  => StrengthenWeakenN n a where-    strengthenWeakenN a =-        case strengthenWeakenN @(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
strongweak.cabal view
@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           strongweak-version:        0.11.0+version:        0.12.0 synopsis:       Convert between strong and weak representations of types description:    Please see README.md. category:       Data@@ -30,6 +30,7 @@ library   exposed-modules:       Strongweak+      Strongweak.Chain       Strongweak.Generic       Strongweak.Strength       Strongweak.Strengthen@@ -38,8 +39,6 @@       Strongweak.Util.TypeNats       Strongweak.Weaken       Strongweak.Weaken.Generic-      Strongweak.WeakenN-      Strongweak.WeakenN.Internal   other-modules:       Paths_strongweak   hs-source-dirs: