packages feed

strongweak 0.10.0 → 0.11.0

raw patch · 10 files changed

+231/−77 lines, 10 files

Files

CHANGELOG.md view
@@ -1,3 +1,8 @@+## 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
src/Strongweak.hs view
@@ -13,20 +13,25 @@   , Strengthen(..)    -- * Other definitions+  , WeakenN(..)+  , SWCoercibly(..)   , liftWeakF    -- * Strength switch wrapper   , Strength(..)   , type SW+  , type SWN    ) where  import Strongweak.Weaken import Strongweak.Strengthen+import Strongweak.Strength+import Strongweak.WeakenN  {- $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 +48,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 +67,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/Generic.hs view
@@ -11,8 +11,9 @@     weakenGeneric   , strengthenGeneric -  -- * Generic wrapper+  -- * Generic deriving via wrappers   , GenericallySW(..)+  , GenericallySW0(..)   ) where  import Strongweak.Weaken.Generic@@ -23,6 +24,8 @@ 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,12 +73,8 @@ 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@@ -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,34 @@+-- | Definitions using a type-level strength switch.++module Strongweak.Strength where++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).+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++-- | Shortcut for a 'SW'-wrapped 'WeakenN'.+type SWN (s :: Strength) (n :: Natural) a = SW s (WeakenN n a)
src/Strongweak/Strengthen.hs view
@@ -20,8 +20,13 @@   , 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(Weakened, weaken) )  import GHC.TypeNats ( KnownNat ) import Data.Word@@ -41,7 +46,7 @@  import Data.Typeable ( Typeable, TypeRep, typeRep, Proxy(Proxy) ) -{- | Attempt to strengthen some @'Weak' a@, asserting certain invariants.+{- | 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@@ -101,6 +106,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@@ -139,14 +153,6 @@             [ "type: [a] -> Vector v "<>TBL.fromUnboundedDec n<>" a"             , "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
src/Strongweak/Strengthen/Unsafe.hs view
@@ -7,11 +7,13 @@ 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 ) +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@@ -34,6 +36,12 @@     -- | 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,11 @@-{-# LANGUAGE UndecidableInstances #-} -- for SWDepth+{-# LANGUAGE UndecidableInstances #-} -- for WeakenedN  module Strongweak.Weaken   (-  -- * 'Weaken' class-    Weaken(..)+    Weaken(Weakened, weaken)+  , type WeakenedN   , liftWeakF--  -- * Strength switch helper-  , Strength(..)-  , type SW-  , type SWDepth+  , SWCoercibly(..)   ) where  import Rerefined@@ -35,38 +31,31 @@     -- | Weaken some @a@ to its associated weak type @'Weakened' a@.     weaken :: a -> Weakened a --- | Strength enumeration: is it strong, or weak?------ Primarily interesting at the type level (using DataKinds).-data Strength = Strong | Weak- -- | Lift a function on a weak type to the associated strong type by weakening --   first.-liftWeakF :: Weaken a => (Weakened 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.--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.+-- | 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) -@-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+-- | A "via type" newtype for defining strongweak instances for zero-invariant,+--   coercible newtypes.+--+-- Use like so:+--+-- @+-- deriving via 'SWCoercibly' a instance 'Weaken' ('Identity' 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 = Weakened (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@@ -87,16 +76,6 @@ instance VG.Vector v a => Weaken (VGS.Vector v n a) where     type Weakened (VGS.Vector v n a) = [a]     weaken = VGS.toList---- | Strip wrapper.-instance Weaken   (Identity a) where-    type Weakened (Identity a) = a-    weaken = runIdentity---- | Strip wrapper.-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).
+ src/Strongweak/WeakenN.hs view
@@ -0,0 +1,38 @@+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 view
@@ -0,0 +1,55 @@+{-# 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.10.0+version:        0.11.0 synopsis:       Convert between strong and weak representations of types description:    Please see README.md. category:       Data@@ -31,12 +31,15 @@   exposed-modules:       Strongweak       Strongweak.Generic+      Strongweak.Strength       Strongweak.Strengthen       Strongweak.Strengthen.Generic       Strongweak.Strengthen.Unsafe       Strongweak.Util.TypeNats       Strongweak.Weaken       Strongweak.Weaken.Generic+      Strongweak.WeakenN+      Strongweak.WeakenN.Internal   other-modules:       Paths_strongweak   hs-source-dirs: