packages feed

strongweak 0.2.0 → 0.3.0

raw patch · 15 files changed

+488/−294 lines, 15 files

Files

CHANGELOG.md view
@@ -1,3 +1,14 @@+## 0.3.0 (2022-06-08)+  * switch to associated type family for `Weak` inside `Weaken` - `Strengthen`+    now has `Weaken` as a superclass+    * I'm fairly confident that things make more sense this way - we get to+      remove an open type family, improve type inference, and prevent users from+      writing potentially dangerous instances. For that, a bit of asymmetry is+      welcome.+  * better document generic derivers+  * clarify instance design, provide more decomposer instances+  * various refactoring+ ## 0.2.0 (2022-05-31) Initial Hackage release (dependency issues prevented uploading).
README.md view
@@ -1,7 +1,8 @@ [lib-refined-hackage]: https://hackage.haskell.org/package/refined+[lib-barbies-hackage]: https://hackage.haskell.org/package/barbies  # strongweak-Convert between pairs of "weak" and "strong"/"validated" types, with good+Purely convert between pairs of "weak" and "strong"/"validated" types, with good errors and generic derivers.  ## Definition of strong and weak types@@ -18,6 +19,8 @@  As an arbitrary limitation for ease of use, a strong type has only one associated weak type. The same weak type may be used for multiple strong types.+This restriction guides the design of "good" strong-weak type pairs & keeps them+synchronized, plus helps type inference.  ### Examples The [refined][lib-refined-hackage] library defines a `newtype Refined p a =@@ -74,24 +77,23 @@ inline, but it also may slow things down e.g. `Natural`s are slower than `Word`s. -## Generic derivation algorithm-As far as I understand, `Strengthen` and `Weaken` generic derivations are safe,-in that they will either fail with a type error, or give you a correct instance.-Both work in a similar manner:+## Related projects+### barbies+The [barbies][lib-barbies-hackage] library is an investigation into how far the+higher-kinded data pattern can be stretched. strongweak has some similar ideas: -  * Both datatypes are traversed in tandem.-  * When both datatypes are at a field:-    * If both types are identical, the value is rewrapped with no changes.-    * Else, if the input type can be transformed into the output type, it is.-      (Strengthening will wrap any errors at this stage with metadata collected-      from the datatype's generic representation.-    * Else, the pair of fields are not compatible, and the derivation fails.+  * Both treat a type definition as a "skeleton" for further types.+  * strongweak's `SW` type family looks a lot like barbies' `Wear`. -Note this may fail for types with a manually-derived `Generic` instance:+But I believe we're irreconcilable. strongweak is concerned with validation via+types. `SW` is just a convenience to reuse a definition for two otherwise+distinct types, and assist in handling common patterns. Due to the type family+approach, we can rarely be polymorphic over the strong and weak representations.+Whereas barbies wants to help you swap out functors over records, so it's very+polymorphic over those, and makes rules for itself that then apply to its users. -  * The types' SOP tree structures must match.-    * I don't think GHC itself guarantees this, so if you receive surprising-      derivation errors, the types might have differing generic representation-      structure (even if the "flat" representation may be identical).-  * Strengthening requires that metadata is present for all parts of the-    representation (datatype, constructor, selector).+You could stack barbies on top of a `SW` type no problem. It would enable you to+split strengthening into two phases: strengthening each field, then gathering+via traverse (rather than doing both at once via applicative do). That thinking+helps reassure me that these ideas are separate. *(Note: I would hesitate to+write such a type, because the definition would start to get mighty complex.)*
src/Strongweak.hs view
@@ -1,25 +1,35 @@ module Strongweak-  ( module Strongweak.Weaken-  , module Strongweak.Strengthen, restrengthen-  , module Strongweak.SW+  (+  -- * Instance design+  -- $strongweak-instance-design++  -- * Re-exports+    module Strongweak.Weaken+  , module Strongweak.Strengthen   ) where  import Strongweak.Weaken import Strongweak.Strengthen-import Strongweak.SW -import Data.Either.Validation-import Data.List.NonEmpty+{- $strongweak-instance-design --- | Weaken and re-strengthen a strong value.------ In correct operation, @restrengthen === Right@. If your value was--- strengthened incorrectly, or perhaps you cheated via @UnsafeStrengthen@, this--- may not be the case. For example:------ >>> restrengthen $ unsafeStrengthen' @(Vector 2 Natural) [0]--- Failure ...-restrengthen-    :: forall w s. (Weaken s w, Strengthen w s)-    => s -> Validation (NonEmpty StrengthenError) s-restrengthen = strengthen . weaken+We identify two distinct types of instances for strongweak classes:++  * /invariant handler:/ removes or adds an invariant+  * /decomposer:/ transforms through some structural type++In order to provide good behaviour and composability, we don't mix both in a+single instance. The decomposers are really just convenience to ease instance+derivation. In general, decomposers will have a recursive context, and invariant+handlers won't.++An example is @'Data.List.NonEmpty.NonEmpty' a@. We could weaken this to @[a]@,+but also to @['Weak' a]@. However, the latter would mean decomposing and+removing an invariant simultaneously. It would be two separate strengthens in+one instance. And now, your 'a' must be in the strongweak ecosystem, which isn't+necessarily what you want - indeed, it appears this sort of design would require+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/Example.hs 
@@ -1,43 +0,0 @@-module Strongweak.Example where--import Strongweak-import Strongweak.Generic--import GHC.Generics ( Generic )--import Data.Word ( Word8 )--import Refined hiding ( Weaken(..) )-import Numeric.Natural--data Ex1D (s :: Strength) = Ex1C-  { ex1f1 :: SW s Word8-  , ex1f2 :: SW s (Refined (LessThan 100) Natural)-  } deriving stock Generic-deriving stock instance Show (Ex1D 'Strong)-deriving stock instance Show (Ex1D 'Weak)-instance Weaken     (Ex1D 'Strong) (Ex1D 'Weak)   where weaken     = weakenGeneric-instance Strengthen (Ex1D 'Weak)   (Ex1D 'Strong) where strengthen = strengthenGeneric--data Ex2D (s :: Strength) = Ex2C-  { ex2f1 :: Ex1D s-  , ex2f2 :: SW s Word8-  } deriving stock Generic-deriving stock instance Show (Ex2D 'Strong)-deriving stock instance Show (Ex2D 'Weak)-instance Weaken     (Ex2D 'Strong) (Ex2D 'Weak)   where weaken     = weakenGeneric-instance Strengthen (Ex2D 'Weak)   (Ex2D 'Strong) where strengthen = strengthenGeneric--ex1w :: Ex1D 'Weak-ex1w = Ex1C 256 210--ex2w :: Ex2D 'Weak-ex2w = Ex2C ex1w 256--data ExVoid (s :: Strength) deriving stock Generic-instance Weaken     (ExVoid 'Strong) (ExVoid 'Weak)   where weaken     = weakenGeneric-instance Strengthen (ExVoid 'Weak)   (ExVoid 'Strong) where strengthen = strengthenGeneric--data ExUnit (s :: Strength) = ExUnit deriving stock Generic-instance Weaken     (ExUnit 'Strong) (ExUnit 'Weak)   where weaken     = weakenGeneric-instance Strengthen (ExUnit 'Weak)   (ExUnit 'Strong) where strengthen = strengthenGeneric
src/Strongweak/Generic.hs view
@@ -1,7 +1,39 @@+-- | Generic 'strengthen' and 'weaken'.+ module Strongweak.Generic-  ( weakenGeneric+  (+  -- * Generic derivation compatibility+  -- $generic-derivation-compatibility++  -- * Generic derivers+    weakenGeneric   , strengthenGeneric   ) where  import Strongweak.Generic.Weaken import Strongweak.Generic.Strengthen++{- $generic-derivation-compatibility++The 'Strengthen' and 'Weaken' generic derivers allow you to derive instances+between any /compatible/ pair of types. Compatibility is defined as follows:++  * 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.++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!).++I don't think GHC strongly guarantees the SOP property, so if you receive+surprising derivation errors, the types might have differing generic+representation structure, even if their flattened representations are identical.+If you experience this let me know, since in my experience GHC's stock @Generic@+derivation is highly deterministic.++Also, generic strengthening requires that all metadata is present for both+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.+-}
src/Strongweak/Generic/Strengthen.hs view
@@ -1,10 +1,10 @@-{- | Strengthening for generic data types.+{- | 'strengthen' over generic representations. -The generic derivation is split into 3 classes, each dealing with a different-layer of a generic Haskell data type: datatype (D), constructor (C) and selector-(S). At each point, we gather up information about the type and push on.-Strengthening occurs at selectors. If a strengthening fails, the gathered-information is pushed into an error that wraps the original error.+Strengthen failures are annotated with precise information describing where the+failure occurred: datatype name, constructor name, field index (and name if+present). To achieve this, we split the generic derivation into 3 classes, each+handling/"unwrapping" a different layer of the generic representation: datatype+(D), constructor (C) and selector (S). -}  {-# LANGUAGE AllowAmbiguousTypes #-}@@ -19,56 +19,81 @@ import Numeric.Natural import Control.Applicative ( liftA2 ) +-- | Strengthen a value generically.+--+-- The weak and strong types must be /compatible/. See 'Strongweak.Generic' for+-- the definition of compatibility in this context. strengthenGeneric     :: (Generic w, Generic s, GStrengthenD (Rep w) (Rep s))-    => w -> Validation (NonEmpty StrengthenError) s+    => w -> Validation (NonEmpty StrengthenFail) s strengthenGeneric = fmap to . gstrengthenD . from +-- | Generic strengthening at the datatype level. class GStrengthenD w s where-    gstrengthenD :: w p -> Validation (NonEmpty StrengthenError) (s p)+    gstrengthenD :: w p -> Validation (NonEmpty StrengthenFail) (s p) +-- | Enter a datatype, stripping its metadata wrapper. instance (GStrengthenC w s, Datatype dw, Datatype ds) => GStrengthenD (D1 dw w) (D1 ds s) where     gstrengthenD = fmap M1 . gstrengthenC (datatypeName' @dw) (datatypeName' @ds) . unM1 +-- | Generic strengthening at the constructor sum level. class GStrengthenC w s where-    gstrengthenC :: String -> String -> w p -> Validation (NonEmpty StrengthenError) (s p)+    gstrengthenC :: String -> String -> w p -> Validation (NonEmpty StrengthenFail) (s p)  -- | Nothing to do for empty datatypes. instance GStrengthenC V1 V1 where     gstrengthenC _ _ = Success -instance (GStrengthenS w s, Constructor cw, Constructor cs) => GStrengthenC (C1 cw w) (C1 cs s) where-    gstrengthenC dw ds = fmap M1 . snd . gstrengthenS dw ds (conName' @cw) (conName' @cs) 0 . unM1---- | Strengthen sum types by strengthening left or right.+-- | Strengthen sum types by casing and strengthening left or right. instance (GStrengthenC lw ls, GStrengthenC rw rs) => GStrengthenC (lw :+: rw) (ls :+: rs) where     gstrengthenC dw ds = \case L1 l -> L1 <$> gstrengthenC dw ds l                                R1 r -> R1 <$> gstrengthenC dw ds r +-- | Enter a constructor, stripping its metadata wrapper.+instance (GStrengthenS w s, Constructor cw, Constructor cs) => GStrengthenC (C1 cw w) (C1 cs s) where+    gstrengthenC dw ds = fmap M1 . snd . gstrengthenS dw ds (conName' @cw) (conName' @cs) 0 . unM1++{- | Generic strengthening at the selector product level.++In order to calculate field indices, we return the current field index alongside+the result. This way, the product case can strengthen the left branch, then+increment the returned field index and use it for strengthening the right+branch.+-} class GStrengthenS w s where-    gstrengthenS :: String -> String -> String -> String -> Natural -> w p -> (Natural, Validation (NonEmpty StrengthenError) (s p))+    gstrengthenS+        :: String  -- ^ weak   datatype name+        -> String  -- ^ strong datatype name+        -> String  -- ^ weak   constructor name+        -> String  -- ^ strong constructor name+        -> Natural -- ^ current field index (0, from left)+        -> w p -> (Natural, Validation (NonEmpty StrengthenFail) (s p))  -- | Nothing to do for empty constructors. instance GStrengthenS U1 U1 where     gstrengthenS _ _ _ _ n x = (n, Success x) +-- | Strengthen product types by strengthening left and right.+--+-- This is ordered (left then right) in order to pass the field index along.+instance (GStrengthenS lw ls, GStrengthenS rw rs) => GStrengthenS (lw :*: rw) (ls :*: rs) where+    gstrengthenS dw ds cw cs n (l :*: r) = (n'', liftA2 (:*:) l' r')+      where+        (n',  l') = gstrengthenS dw ds cw cs n      l+        (n'', r') = gstrengthenS dw ds cw cs (n'+1) r+ -- | Special case: if source and target types are equal, copy the value through. instance GStrengthenS (S1 mw (Rec0 w)) (S1 ms (Rec0 w)) where     gstrengthenS _ _ _ _ n x = (n, Success (M1 (unM1 x)))  -- | Strengthen a field using the existing 'Strengthen' instance.------ On strengthen failure, the errors are annotated with all the datatype--- information we've hoarded. The upshot is that if you strengthen a type with--- lots of types inside it, all with generically-derived 'Strengthen' instances,--- you'll get a precise zoom-in of exactly where each error occurred.-instance {-# OVERLAPS #-} (Strengthen w s, Selector mw, Selector ms) => GStrengthenS (S1 mw (Rec0 w)) (S1 ms (Rec0 s)) where+instance {-# OVERLAPS #-} (Strengthen s, Weak s ~ w, Selector mw, Selector ms) => GStrengthenS (S1 mw (Rec0 w)) (S1 ms (Rec0 s)) where     gstrengthenS dw ds cw cs n (M1 (K1 w)) =         case strengthen w of           Failure es ->             let fw = selName'' @mw                 fs = selName'' @ms-                e  = StrengthenErrorField dw ds cw cs n fw n fs es+                e  = StrengthenFailField dw ds cw cs n fw n fs es             in  (n, Failure $ e :| [])           Success s   -> (n, Success $ M1 $ K1 s) @@ -80,15 +105,6 @@ selName'' :: forall s. Selector s => Maybe String selName'' = case selName' @s of "" -> Nothing                                 s  -> Just s---- | Strengthen product types by strengthening left and right.------ This is ordered (left then right), but only to pass the index along.-instance (GStrengthenS lw ls, GStrengthenS rw rs) => GStrengthenS (lw :*: rw) (ls :*: rs) where-    gstrengthenS dw ds cw cs n (l :*: r) = (n'', liftA2 (:*:) l' r')-      where-        (n',  l') = gstrengthenS dw ds cw cs n      l-        (n'', r') = gstrengthenS dw ds cw cs (n'+1) r  --------------------------------------------------------------------------------
src/Strongweak/Generic/Weaken.hs view
@@ -1,4 +1,4 @@--- | Weakening for generic data types.+-- | 'weaken' over generic representations.  module Strongweak.Generic.Weaken where @@ -6,6 +6,10 @@  import GHC.Generics +-- | Weaken a value generically.+--+-- The weak and strong types must be /compatible/. See 'Strongweak.Generic' for+-- the definition of compatibility in this context. weakenGeneric :: (Generic s, Generic w, GWeaken (Rep s) (Rep w)) => s -> w weakenGeneric = to . gweaken . from @@ -29,14 +33,14 @@     gweaken = id  -- | Weaken a field using the existing 'Weaken' instance.-instance {-# OVERLAPS #-} Weaken s w => GWeaken (Rec0 s) (Rec0 w) where+instance {-# OVERLAPS #-} (Weaken s, Weak s ~ w) => GWeaken (Rec0 s) (Rec0 w) where     gweaken = K1 . weaken . unK1  -- | Weaken product types by weakening left and right. instance (GWeaken ls lw, GWeaken rs rw) => GWeaken (ls :*: rs) (lw :*: rw) where     gweaken (l :*: r) = gweaken l :*: gweaken r --- | Weaken sum types by weakening left or right.+-- | Weaken sum types by casing and weakening left or right. instance (GWeaken ls lw, GWeaken rs rw) => GWeaken (ls :+: rs) (lw :+: rw) where     gweaken = \case L1 l -> L1 $ gweaken l                     R1 r -> R1 $ gweaken r
− src/Strongweak/SW.hs 
@@ -1,45 +0,0 @@-module Strongweak.SW where--import Refined ( Refined )-import Data.Vector.Sized ( Vector )-import Data.Kind ( Type )-import Data.Word-import Data.Int-import Numeric.Natural ( Natural )--data Strength = Strong | Weak---- | Obtain the weak representation of the given type.-type family Weak (a :: Type) :: Type---- machine integers-type instance Weak Word8  = Natural-type instance Weak Word16 = Natural-type instance Weak Word32 = Natural-type instance Weak Word64 = Natural-type instance Weak Int8   = Integer-type instance Weak Int16  = Integer-type instance Weak Int32  = Integer-type instance Weak Int64  = Integer---- other-type instance Weak (Vector n a) = [a]-type instance Weak (Refined p a) = a--{- |-Obtain either the strong or weak representation of a type, depending on the-type-level strength "switch" provided.--This is intended to be used in data types that take a 'Strength' type. Define-your type using strong fields wrapped in @Switch s@. You then get the weak-representation for free, using the same definition.--@-data A (s :: Strength) = A-  { aField1 :: Switch s Word8-  , aField2 :: String }-@--}-type family SW (s :: Strength) a :: Type where-    SW 'Strong a = a-    SW 'Weak   a = Weak a
src/Strongweak/Strengthen.hs view
@@ -1,52 +1,90 @@-{-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE CPP #-} -module Strongweak.Strengthen where+module Strongweak.Strengthen+  (+  -- * 'Strengthen' class+    Strengthen(..) +  -- * Strengthen failures+  , StrengthenFail(..)+  , strengthenFailPretty+  , strengthenFailBase++  -- * Restrengthening+  , restrengthen++  -- * Helpers+  , strengthenBounded++  -- * Re-exports+  , Strongweak.Weaken.Weak+  ) where++import Strongweak.Weaken ( Weaken(..) )+import Data.Either.Validation+import Type.Reflection ( Typeable, typeRep )+import Prettyprinter+import Prettyprinter.Render.String+ import GHC.TypeNats ( Natural, KnownNat ) import Data.Word import Data.Int import Refined ( Refined, refine, Predicate ) import Data.Vector.Sized qualified as Vector import Data.Vector.Sized ( Vector )-import Type.Reflection ( Typeable, typeRep )+import Data.Foldable qualified as Foldable+import Control.Applicative ( liftA2 )+import Data.Functor.Identity+import Data.Functor.Const+import Data.List.NonEmpty ( NonEmpty( (:|) ) )+import Data.List.NonEmpty qualified as NonEmpty -import Prettyprinter-import Prettyprinter.Render.String+{- | You may attempt to transform a @'Weak' a@ to an @a@. -import Data.Either.Validation-import Data.List.NonEmpty ( NonEmpty( (:|) ) )-import Data.Foldable qualified as Foldable+Laws: -{- | Any 'w' can be "strengthened" into an 's' by asserting some properties.+  * @a === b -> 'strengthen' a === 'strengthen' b@+  * @'strengthen' ('weaken' a) === 'Success' a@ -For example, you may strengthen some 'Natural' @n@ into a 'Word8' by asserting-@0 <= n <= 255@.+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+straightforward) class to define. -Note that we restrict strengthened types to having only one corresponding weak-representation using functional dependencies.+Instances should /either/ handle an invariant, or decompose. See "Strongweak"+for a discussion on this design. -}-class Strengthen w s | s -> w where strengthen :: w -> Validation (NonEmpty StrengthenError) s+class Weaken a => Strengthen a where+    -- | Attempt to transform a weak value to its associated strong one.+    strengthen :: Weak a -> Validation (NonEmpty StrengthenFail) a --- | 'strengthen' with reordered type variables for more convenient visible type---   application.-strengthen' :: forall s w. Strengthen w s => w -> Validation (NonEmpty StrengthenError) s-strengthen' = strengthen+-- | Weaken a strong value, then strengthen it again.+--+-- Potentially useful if you have previously used+-- 'Strongweak.Strengthen.Unsafe.unsafeStrengthen' and now wish to check the+-- invariants. For example:+--+-- >>> restrengthen $ unsafeStrengthen @(Vector 2 Natural) [0]+-- Failure ...+restrengthen+    :: (Strengthen a, Weaken a)+    => a -> Validation (NonEmpty StrengthenFail) a+restrengthen = strengthen . weaken --- | Strengthen error data type. Don't use these constructors directly, use+-- | Strengthen failure data type. Don't use these constructors directly, use --   the existing helper functions. -- -- Field indices are from 0 in the respective constructor. Field names are -- provided if present.-data StrengthenError-  = StrengthenErrorBase+data StrengthenFail+  = StrengthenFailBase         String -- ^ weak   type         String -- ^ strong type         String -- ^ weak value         String -- ^ msg -  | StrengthenErrorField+  | StrengthenFailField         String                      -- ^ weak   datatype name         String                      -- ^ strong datatype name         String                      -- ^ weak   constructor name@@ -55,77 +93,108 @@         (Maybe String)              -- ^ weak   field name (if present)         Natural                     -- ^ strong field index         (Maybe String)              -- ^ strong field name (if present)-        (NonEmpty StrengthenError)  -- ^ errors+        (NonEmpty StrengthenFail)   -- ^ failures     deriving stock Eq -instance Show StrengthenError where+instance Show StrengthenFail where     showsPrec _ = renderShowS . layoutPretty defaultLayoutOptions . pretty  -- TODO shorten value if over e.g. 50 chars. e.g. @[0,1,2,...,255] -> FAIL@-instance Pretty StrengthenError where+instance Pretty StrengthenFail where     pretty = \case-      StrengthenErrorBase wt st wv msg ->+      StrengthenFailBase wt st wv msg ->         vsep [ pretty wt<+>"->"<+>pretty st              , pretty wv<+>"->"<+>"FAIL"              , pretty msg ]-      StrengthenErrorField dw _ds cw _cs iw fw _is _fs es ->+      StrengthenFailField dw _ds cw _cs iw fw _is _fs es ->         let sw = maybe (show iw) id fw-        in  nest 0 $ pretty dw<>"."<>pretty cw<>"."<>pretty sw<>line<>strengthenErrorPretty es+        in  nest 0 $ pretty dw<>"."<>pretty cw<>"."<>pretty sw<>line<>strengthenFailPretty es  -- mutually recursive with its 'Pretty' instance. safe, but a bit confusing - -- clean up-strengthenErrorPretty :: NonEmpty StrengthenError -> Doc a-strengthenErrorPretty = vsep . map go . Foldable.toList+strengthenFailPretty :: NonEmpty StrengthenFail -> Doc a+strengthenFailPretty = vsep . map go . Foldable.toList   where go e = "-"<+>indent 0 (pretty e) -strengthenErrorBase+strengthenFailBase     :: forall s w. (Typeable w, Show w, Typeable s)-    => w -> String -> Validation (NonEmpty StrengthenError) s-strengthenErrorBase w msg = Failure (e :| [])-  where e = StrengthenErrorBase (show $ typeRep @w) (show $ typeRep @s) (show w) msg+    => w -> String -> Validation (NonEmpty StrengthenFail) s+strengthenFailBase w msg = Failure (e :| [])+  where e = StrengthenFailBase (show $ typeRep @w) (show $ typeRep @s) (show w) msg --- | Strengthen each element of a list.-instance Strengthen w s => Strengthen [w] [s] where-    strengthen = traverse strengthen+-- | Obtain a non-empty list by asserting non-emptiness of a plain list.+instance (Typeable a, Show a) => Strengthen (NonEmpty a) where+    strengthen a =+        case NonEmpty.nonEmpty a of+          Just a' -> Success a'+          Nothing -> strengthenFailBase a "empty list"  -- | Obtain a sized vector by asserting the size of a plain list.-instance (KnownNat n, Typeable a, Show a) => Strengthen [a] (Vector n a) where+instance (KnownNat n, Typeable a, Show a) => Strengthen (Vector n a) where     strengthen w =         case Vector.fromList w of-          Nothing -> strengthenErrorBase w "TODO bad size vector"+          Nothing -> strengthenFailBase w "TODO bad size vector"           Just s  -> Success s  -- | Obtain a refined type by applying its associated refinement. #ifdef REFINED_POLYKIND-instance (Predicate (p :: k) a, Typeable k, Typeable a, Show a) => Strengthen a (Refined p a) where+instance (Predicate (p :: k) a, Typeable k, Typeable a, Show a) => Strengthen (Refined p a) where #else-instance (Predicate p a, Typeable p, Typeable a, Show a) => Strengthen a (Refined p a) where+instance (Predicate p a, Typeable p, Typeable a, Show a) => Strengthen (Refined p a) where #endif     strengthen a =         case refine a of-          Left  err -> strengthenErrorBase a (show err)+          Left  err -> strengthenFailBase a (show err)           Right ra  -> Success ra  -- Strengthen 'Natural's into Haskell's bounded unsigned numeric types.-instance Strengthen Natural Word8  where strengthen = strengthenBounded-instance Strengthen Natural Word16 where strengthen = strengthenBounded-instance Strengthen Natural Word32 where strengthen = strengthenBounded-instance Strengthen Natural Word64 where strengthen = strengthenBounded+instance Strengthen Word8  where strengthen = strengthenBounded+instance Strengthen Word16 where strengthen = strengthenBounded+instance Strengthen Word32 where strengthen = strengthenBounded+instance Strengthen Word64 where strengthen = strengthenBounded  -- Strengthen 'Integer's into Haskell's bounded signed numeric types.-instance Strengthen Integer Int8   where strengthen = strengthenBounded-instance Strengthen Integer Int16  where strengthen = strengthenBounded-instance Strengthen Integer Int32  where strengthen = strengthenBounded-instance Strengthen Integer Int64  where strengthen = strengthenBounded+instance Strengthen Int8   where strengthen = strengthenBounded+instance Strengthen Int16  where strengthen = strengthenBounded+instance Strengthen Int32  where strengthen = strengthenBounded+instance Strengthen Int64  where strengthen = strengthenBounded  strengthenBounded     :: forall b n     .  (Integral b, Bounded b, Show b, Typeable b, Integral n, Show n, Typeable n)-    => n -> Validation (NonEmpty StrengthenError) b+    => n -> Validation (NonEmpty StrengthenFail) b strengthenBounded n =     if   n <= maxB && n >= minB then Success (fromIntegral n)-    else strengthenErrorBase n $ "not well bounded, require: "+    else strengthenFailBase n $ "not well bounded, require: "                                  <>show minB<>" <= n <= "<>show maxB   where     maxB = fromIntegral @b @n maxBound     minB = fromIntegral @b @n minBound++--------------------------------------------------------------------------------++-- | Decomposer. Strengthen every element in a list.+instance Strengthen a => Strengthen [a] where+    strengthen = traverse strengthen++-- | Decomposer.+instance (Strengthen a, Strengthen b) => Strengthen (a, b) where+    strengthen (a, b) = liftA2 (,) (strengthen a) (strengthen b)++-- | Decomposer.+instance Strengthen a => Strengthen (Maybe a) where+    strengthen = \case Just a  -> Just <$> strengthen a+                       Nothing -> pure Nothing++-- | Decomposer.+instance (Strengthen a, Strengthen b) => Strengthen (Either a b) where+    strengthen = \case Left  a -> Left  <$> strengthen a+                       Right b -> Right <$> strengthen b++-- | Decomposer.+instance Strengthen a => Strengthen (Identity a) where+    strengthen = fmap Identity . strengthen . runIdentity++-- | Decomposer.+instance Strengthen a => Strengthen (Const a b) where+    strengthen = fmap Const . strengthen . getConst
src/Strongweak/Strengthen/Unsafe.hs view
@@ -1,8 +1,6 @@-{-# LANGUAGE FunctionalDependencies #-}- module Strongweak.Strengthen.Unsafe where -import Numeric.Natural+import Strongweak.Weaken import Data.Word import Data.Int import Refined ( Refined )@@ -10,49 +8,85 @@ import Data.Vector.Sized ( Vector ) import Data.Vector.Generic.Sized.Internal qualified import Data.Vector qualified+import Data.Functor.Identity+import Data.Functor.Const+import Data.List.NonEmpty qualified as NonEmpty+import Data.List.NonEmpty ( NonEmpty ) -{- | Any 'w' can be unsafely "strengthened" into an 's' by pretending that we've-     asserted some properties.+{- | Unsafely transform a @'Weak' a@ to an @a@, without asserting invariants. -For example, you may unsafely strengthen some 'Natural' @n@ into a 'Word8' by-unsafely coercing the value, ignoring the possibility that @n >= 255@.+For example, you may unsafely strengthen some @'Numeric.Natural.Natural' n@ into+a 'Word8' by unsafely coercing the value, ignoring the possibility that @n >=+255@. -Currently, this class is more of a thought experiment than something to use.-That is to say, do not use this.+What happens if it turns out you're lying to the computer and your weak value+doesn't fit in its strong counterpart? That depends on the strengthen. -This typeclass should probably follow its big sis 'Strengthen'. Only provide-'UnsafeStrengthen' instances for types that have similar 'Strengthen' instances.--}-class UnsafeStrengthen w s | s -> w where unsafeStrengthen :: w -> s+  * Numeric coercions should safely overflow.+  * Some will raise an error (e.g. 'NonEmpty').+  * Others will appear to work, but later explode your computer (sized vectors+    will probably do this). --- | 'unsafeStrengthen' with reordered type variables for more convenient---   visible type application.-unsafeStrengthen' :: forall s w. UnsafeStrengthen w s => w -> s-unsafeStrengthen' = unsafeStrengthen+Only consider using this if you have a guarantee that your value is safe to+treat as strong. --- | Unsafely strengthen each element of a list.-instance UnsafeStrengthen w s => UnsafeStrengthen [w] [s] where-    unsafeStrengthen = map unsafeStrengthen+Instances should /either/ handle an invariant, or decompose. See "Strongweak"+for a discussion on this design.+-}+class Weaken a => UnsafeStrengthen a where+    -- | Unsafely transform a weak value to its associated strong one.+    unsafeStrengthen :: Weak a -> a --- | Obtain a sized vector by unsafely assuming the size of a plain list.---   Extremely unsafe.-instance UnsafeStrengthen [a] (Vector n a) where+-- | Unsafely assume a list is non-empty.+instance UnsafeStrengthen (NonEmpty a) where+    unsafeStrengthen = NonEmpty.fromList++-- | Unsafely assume the size of a plain list.+instance UnsafeStrengthen (Vector n a) where     unsafeStrengthen = Data.Vector.Generic.Sized.Internal.Vector . Data.Vector.fromList --- | Obtain a refined type by ignoring the predicate.-instance UnsafeStrengthen a (Refined p a) where+-- | Wrap a value to a refined one without checking the predicate.+instance UnsafeStrengthen (Refined p a) where     unsafeStrengthen = reallyUnsafeRefine  -- Coerce 'Natural's into Haskell's bounded unsigned numeric types. Poorly-sized -- values will safely overflow according to the type's behaviour.-instance UnsafeStrengthen Natural Word8  where unsafeStrengthen = fromIntegral-instance UnsafeStrengthen Natural Word16 where unsafeStrengthen = fromIntegral-instance UnsafeStrengthen Natural Word32 where unsafeStrengthen = fromIntegral-instance UnsafeStrengthen Natural Word64 where unsafeStrengthen = fromIntegral+instance UnsafeStrengthen Word8  where unsafeStrengthen = fromIntegral+instance UnsafeStrengthen Word16 where unsafeStrengthen = fromIntegral+instance UnsafeStrengthen Word32 where unsafeStrengthen = fromIntegral+instance UnsafeStrengthen Word64 where unsafeStrengthen = fromIntegral  -- Coerce 'Integer's into Haskell's bounded signed numeric types. Poorly-sized -- values will safely overflow according to the type's behaviour.-instance UnsafeStrengthen Integer Int8   where unsafeStrengthen = fromIntegral-instance UnsafeStrengthen Integer Int16  where unsafeStrengthen = fromIntegral-instance UnsafeStrengthen Integer Int32  where unsafeStrengthen = fromIntegral-instance UnsafeStrengthen Integer Int64  where unsafeStrengthen = fromIntegral+instance UnsafeStrengthen Int8   where unsafeStrengthen = fromIntegral+instance UnsafeStrengthen Int16  where unsafeStrengthen = fromIntegral+instance UnsafeStrengthen Int32  where unsafeStrengthen = fromIntegral+instance UnsafeStrengthen Int64  where unsafeStrengthen = fromIntegral++--------------------------------------------------------------------------------++-- | Decomposer. Unsafely strengthen every element in a list.+instance UnsafeStrengthen a => UnsafeStrengthen [a] where+    unsafeStrengthen = map unsafeStrengthen++-- | Decomposer.+instance (UnsafeStrengthen a, UnsafeStrengthen b) => UnsafeStrengthen (a, b) where+    unsafeStrengthen (a, b) = (unsafeStrengthen a, unsafeStrengthen b)++-- | Decomposer.+instance UnsafeStrengthen a => UnsafeStrengthen (Maybe a) where+    unsafeStrengthen = \case Just a  -> Just $ unsafeStrengthen a+                             Nothing -> Nothing++-- | Decomposer.+instance (UnsafeStrengthen a, UnsafeStrengthen b) => UnsafeStrengthen (Either a b) where+    unsafeStrengthen = \case Left  a -> Left  $ unsafeStrengthen a+                             Right b -> Right $ unsafeStrengthen b++-- | Decomposer.+instance UnsafeStrengthen a => UnsafeStrengthen (Identity a) where+    unsafeStrengthen = Identity . unsafeStrengthen . runIdentity++-- | Decomposer.+instance UnsafeStrengthen a => UnsafeStrengthen (Const a b) where+    unsafeStrengthen = Const . unsafeStrengthen . getConst
src/Strongweak/Weaken.hs view
@@ -1,6 +1,13 @@-{-# LANGUAGE FunctionalDependencies #-}+module Strongweak.Weaken+  (+  -- * 'Weaken' class+    Weaken(..)+  , liftWeakF -module Strongweak.Weaken where+  -- * 'SW' helper+  , Strength(..)+  , SW+  ) where  import Refined ( Refined, unrefine ) import Numeric.Natural ( Natural )@@ -8,31 +15,126 @@ import Data.Int import Data.Vector.Sized qualified as Vector import Data.Vector.Sized ( Vector )+import Data.Kind ( Type )+import Data.Functor.Identity+import Data.Functor.Const+import Data.List.NonEmpty qualified as NonEmpty+import Data.List.NonEmpty ( NonEmpty ) -{- | Any 's' can be "weakened" into a 'w'.+{- | Transform an @a@ to a @'Weak' a@. -For example, you may weaken a 'Word8' into a 'Natural'.+A given strong type @a@ has exactly one associated weak type @'Weak' a@.+Multiple strong types may weaken to the same weak type. -Note that we restrict strengthened types to having only one corresponding weak-representation using functional dependencies.+Law: @a === b -> 'weaken' a === 'weaken' b@++Instances should /either/ handle an invariant, or decompose. See "Strongweak"+for a discussion on this design. -}-class Weaken s w | s -> w where weaken :: s -> w+class Weaken a where+    -- | The type to weaken to.+    type Weak a :: Type --- | Weaken each element of a list-instance Weaken s w => Weaken [s] [w] where weaken = map weaken+    -- | Transform a strong value to its associated weak one.+    weaken :: a -> Weak a +-- | Lift a function on a weak type to the associated strong type.+liftWeakF :: Weaken a => (Weak a -> b) -> (a -> b)+liftWeakF f = f . weaken++-- | Strength enumeration: is it 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 = Weak a++-- | Weaken non-empty lists into plain lists.+instance Weaken (NonEmpty a) where+    type Weak (NonEmpty a) = [a]+    weaken = NonEmpty.toList+ -- | Weaken sized vectors into plain lists.-instance Weaken (Vector n a) [a] where weaken = Vector.toList+instance Weaken (Vector n a) where+    type Weak (Vector n a) = [a]+    weaken = Vector.toList  -- | Strip the refinement from refined types.-instance Weaken (Refined p a) a where weaken = unrefine+instance Weaken (Refined p a) where+    type Weak (Refined p a) = a+    weaken = unrefine  -- Weaken the bounded Haskell numeric types using 'fromIntegral'.-instance Weaken Word8  Natural where weaken = fromIntegral-instance Weaken Word16 Natural where weaken = fromIntegral-instance Weaken Word32 Natural where weaken = fromIntegral-instance Weaken Word64 Natural where weaken = fromIntegral-instance Weaken Int8   Integer where weaken = fromIntegral-instance Weaken Int16  Integer where weaken = fromIntegral-instance Weaken Int32  Integer where weaken = fromIntegral-instance Weaken Int64  Integer where weaken = fromIntegral+instance Weaken Word8  where+    type Weak Word8  = Natural+    weaken = fromIntegral+instance Weaken Word16 where+    type Weak Word16 = Natural+    weaken = fromIntegral+instance Weaken Word32 where+    type Weak Word32 = Natural+    weaken = fromIntegral+instance Weaken Word64 where+    type Weak Word64 = Natural+    weaken = fromIntegral+instance Weaken Int8   where+    type Weak Int8   = Integer+    weaken = fromIntegral+instance Weaken Int16  where+    type Weak Int16  = Integer+    weaken = fromIntegral+instance Weaken Int32  where+    type Weak Int32  = Integer+    weaken = fromIntegral+instance Weaken Int64  where+    type Weak Int64  = Integer+    weaken = fromIntegral++--------------------------------------------------------------------------------++-- | Decomposer. Weaken every element in a list.+instance Weaken a => Weaken [a] where+    type Weak [a] = [Weak a]+    weaken = map weaken++-- | Decomposer.+instance (Weaken a, Weaken b) => Weaken (a, b) where+    type Weak (a, b) = (Weak a, Weak b)+    weaken (a, b) = (weaken a, weaken b)++-- | Decomposer.+instance Weaken a => Weaken (Maybe a) where+    type Weak (Maybe a) = Maybe (Weak a)+    weaken = \case Just a  -> Just $ weaken a+                   Nothing -> Nothing++-- | Decomposer.+instance (Weaken a, Weaken b) => Weaken (Either a b) where+    type Weak (Either a b) = Either (Weak a) (Weak b)+    weaken = \case Left  a -> Left  $ weaken a+                   Right b -> Right $ weaken b++-- | Decomposer.+instance Weaken a => Weaken (Identity a) where+    type Weak (Identity a) = Identity (Weak a)+    weaken = Identity . weaken . runIdentity++-- | Decomposer.+instance Weaken a => Weaken (Const a b) where+    type Weak (Const a b) = Const (Weak a) b+    weaken = Const . weaken . getConst
strongweak.cabal view
@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           strongweak-version:        0.2.0+version:        0.3.0 synopsis:       Convert between strong and weak representations of types description:    Please see README.md. category:       Data@@ -34,13 +34,11 @@ library   exposed-modules:       Strongweak-      Strongweak.Example       Strongweak.Generic       Strongweak.Generic.Strengthen       Strongweak.Generic.Weaken       Strongweak.Strengthen       Strongweak.Strengthen.Unsafe-      Strongweak.SW       Strongweak.Weaken   other-modules:       Paths_strongweak
test/Common.hs view
@@ -23,8 +23,10 @@ deriving stock instance Show (DS 'Weak) deriving via (GenericArbitraryU `AndShrinking` (DS 'Weak))   instance Arbitrary (DS 'Weak) -instance Weaken     (DS 'Strong) (DS 'Weak)   where weaken     = weakenGeneric-instance Strengthen (DS 'Weak)   (DS 'Strong) where strengthen = strengthenGeneric+instance Weaken     (DS 'Strong) where+    type Weak (DS 'Strong) = DS 'Weak+    weaken = weakenGeneric+instance Strengthen (DS 'Strong) where strengthen = strengthenGeneric  data DP (s :: Strength) = DP   { dp1f0 :: SW s Word32@@ -42,5 +44,7 @@ deriving stock instance Show (DP 'Weak) deriving via (GenericArbitraryU `AndShrinking` (DP 'Weak))   instance Arbitrary (DP 'Weak) -instance Weaken     (DP 'Strong) (DP 'Weak)   where weaken     = weakenGeneric-instance Strengthen (DP 'Weak)   (DP 'Strong) where strengthen = strengthenGeneric+instance Weaken     (DP 'Strong) where+    type Weak (DP 'Strong) = DP 'Weak+    weaken = weakenGeneric+instance Strengthen (DP 'Strong) where strengthen = strengthenGeneric
test/Strongweak/LawsSpec.hs view
@@ -9,10 +9,10 @@ spec :: Spec spec = modifyMaxSize (+1000) $ do     prop "weaken-strengthen roundtrip isomorphism (generic)" $ do-      \(d :: DS 'Strong) -> strengthen @(DS 'Weak) (weaken d) `shouldBe` Success d+      \(d :: DS 'Strong) -> strengthen (weaken d) `shouldBe` Success d     prop "strengthen-weaken-strengthen roundtrip partial isomorphism (generic)" $ do       \(dw :: DS 'Weak) ->-        case strengthen dw of-          Failure _ -> pure ()-          Success (ds :: DS 'Strong) ->-            strengthen @(DS 'Weak) (weaken ds) `shouldBe` Success ds+        case strengthen @(DS 'Strong) dw of+          Failure _  -> pure ()+          Success ds ->+            strengthen (weaken ds) `shouldBe` Success ds
test/Strongweak/StrengthenSpec.hs view
@@ -15,32 +15,32 @@     it "returns a precise error for failed generic strengthening (named field)" $ do         let w = fromIntegral (maxBound @Word32) + 1             d = DP w 43 1 2 3 :: DP 'Weak-            e = seGeneric1+            e = sfGeneric1                     "DP" "DP" "DP" "DP" 0 (Just "dp1f0") 0 (Just "dp1f0")                     "Natural" "Word32" w-        strengthen @_ @(DP 'Strong) d `shouldSatisfy` svEqError e+        strengthen @(DP 'Strong) d `shouldSatisfy` svEqFail e     it "returns a precise error for failed generic strengthening (unnamed field)" $ do         let w = fromIntegral (maxBound @Word8) + 1             d = DS0 0 1 2 3 w :: DS 'Weak-            e = seGeneric1+            e = sfGeneric1                     "DS" "DS" "DS0" "DS0" 4 Nothing 4 Nothing                     "Natural" "Word8" w-        strengthen @_ @(DS 'Strong) d `shouldSatisfy` svEqError e+        strengthen @(DS 'Strong) d `shouldSatisfy` svEqFail e -seGeneric1+sfGeneric1     :: Show w     => String -> String -> String -> String     -> Natural -> Maybe String -> Natural -> Maybe String     -> String -> String -> w-    -> StrengthenError-seGeneric1 dw ds cw cs iw fw is fs tw ts w =-    StrengthenErrorField dw ds cw cs iw fw is fs (e :| [])-  where e = StrengthenErrorBase tw ts (show w) (error "TODO ignoring msg")+    -> StrengthenFail+sfGeneric1 dw ds cw cs iw fw is fs tw ts w =+    StrengthenFailField dw ds cw cs iw fw is fs (e :| [])+  where e = StrengthenFailBase tw ts (show w) (error "TODO ignoring msg") -seEqIgnoreMsg :: StrengthenError -> StrengthenError -> Bool-seEqIgnoreMsg s1 s2 = case s1 of-  StrengthenErrorField   dw  ds  cw  cs  iw  fw  is  fs  es -> case s2 of-    StrengthenErrorField dw' ds' cw' cs' iw' fw' is' fs' es' ->+sfEqIgnoreMsg :: StrengthenFail -> StrengthenFail -> Bool+sfEqIgnoreMsg s1 s2 = case s1 of+  StrengthenFailField   dw  ds  cw  cs  iw  fw  is  fs  es -> case s2 of+    StrengthenFailField dw' ds' cw' cs' iw' fw' is' fs' es' ->          dw == dw'       && ds == ds'       && cw == cw'@@ -49,15 +49,15 @@       && fw == fw'       && is == is'       && fs == fs'-      && and (zipWith seEqIgnoreMsg (Foldable.toList es) (Foldable.toList es'))+      && and (zipWith sfEqIgnoreMsg (Foldable.toList es) (Foldable.toList es'))     _ -> False-  StrengthenErrorBase   wt  st  wv  _ -> case s2 of-    StrengthenErrorBase wt' st' wv' _ ->+  StrengthenFailBase   wt  st  wv  _ -> case s2 of+    StrengthenFailBase wt' st' wv' _ ->          wt == wt'       && st == st'       && wv == wv'     _ -> False -svEqError :: StrengthenError -> Validation (NonEmpty StrengthenError) s -> Bool-svEqError e = \case Failure (e' :| []) -> seEqIgnoreMsg e e'-                    _ -> False+svEqFail :: StrengthenFail -> Validation (NonEmpty StrengthenFail) s -> Bool+svEqFail e = \case Failure (e' :| []) -> sfEqIgnoreMsg e e'+                   _ -> False