strongweak 0.4.1 → 0.5.0
raw patch · 12 files changed
+465/−215 lines, 12 filesdep +accdep +text
Dependencies added: acc, text
Files
- CHANGELOG.md +5/−0
- README.md +123/−42
- src/Strongweak.hs +16/−4
- src/Strongweak/Generic/Strengthen.hs +75/−52
- src/Strongweak/Strengthen.hs +157/−72
- src/Strongweak/Util/Text.hs +7/−0
- src/Strongweak/Util/Typeable.hs +8/−0
- src/Strongweak/Weaken.hs +14/−4
- strongweak.cabal +8/−2
- test/Common.hs +5/−0
- test/Strongweak/LawsSpec.hs +4/−3
- test/Strongweak/StrengthenSpec.hs +43/−36
CHANGELOG.md view
@@ -1,3 +1,8 @@+## 0.5.0 (2023-05-05)+ * allow text-2.0+ * refactor strengthening code, rename some definitions+ * use NeAcc instead of NonEmpty for strengthening failures+ ## 0.4.1 (2023-02-22) * add `DerivingVia` wrapper for generic instances (like `Generically`)
README.md view
@@ -2,64 +2,132 @@ [lib-barbies-hackage]: https://hackage.haskell.org/package/barbies # strongweak-Purely convert between pairs of "weak" and "strong"/"validated" types, with good-errors and generic derivers.+Purely convert between pairs of "weak" and "strong"/"validated" types, with+extensive failure reporting and powerful generic derivers. Alexis King's [Parse,+don't validate][parse-dont-validate] pattern as a library. -## Definition of strong and weak types-Take a pair of types `(strong, weak)`. We state the following:+## What? Why?+[refined-blog]: http://nikita-volkov.github.io/refined/ - * You may safely convert ("weaken") any `strong` value to a `weak` value.- * You can try to convert ("strengthen") any `weak` value to a `strong` value,- but it may fail.+Haskell is a wonderful language for accurate data modelling. Algebraic data+types (and GADTs as a fancy extension) enable defining highly restricted types+which prevent even *representing* invalid or unwanted values. Great! And for the+common case where you want to assert some predicate on a value but not change it+(i.e. validate), we have the powerful [refined][refined-blog] library to reflect+the existence of an asserted predicate in types. Fantastic! -As a rule, a weak type should be *easier to use* than its related strong type.-That is, it should have fewer invariants to consider or maintain. You could-weaken an `a` to a `Maybe a`, but since a `Maybe a` is harder to use, it's not a-candidate for this library.+Sadly I'm often grounded by "Reality", who insists that we don't use these+features everywhere because manipulating more complex types often means more+busywork on the term level. So I resort to less accurate data models, or+validating somewhat arbitrarily without assistance from the type system. I can+often feel Alexis King looking disapprovingly at me. -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.+What if we defined two separate representations for a given model? -### Examples-The [refined][lib-refined-hackage] library defines a `newtype Refined p a =-Refined a`. To get a `Refined`, you must test its associated predicate. You may-recover the unrefined value by removing the newtype wrapper. Thus, you may-strengthen `a`s into `Refined p a`s, and weaken vice versa.+ * A **strong** representation, where no invalid values are permitted.+ (Promise.)+ * A **weak** representation, which doesn't necessarily enforce all the+ invariants that the strong representation does, but is easier to manipulate. -The `WordX` family are like bounded `Natural`s. We can consider `Natural` as a-weak type, which can be strengthened into e.g. `Word8` by asserting-well-boundedness.+This way, we can use strong representations wherever possible e.g. passing+between subsystems, and shift to the weak representation for intensive+manipulation (and then back to strong at the end). Potential wins for+simplicity, brevity and performance, albeit for some conversion overhead. +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+ all the checks++We can write these as pure functions.++```haskell+weaken :: S -> W+strengthen :: W -> Maybe S+```++Oh! So this is like a parser-printer pair for arbitrary data. It seems like a+useful enough pattern. Let's think of some strongweak pairs:++ * `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]`.+ * `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]`.++But there's a hefty amount of boilerplate:++ * You need to model all the data types you want to use like this twice.+ * You need to write tons more definitions.++Aaaand it's already not worth it. Sigh.++## Library introduction+strongweak encodes the above strong/weak representation pattern for convenient+use, automating as much as possible. Some decisions restrict usage for nicer+behaviour. The primary definitions are below:++```haskell+class Weaken a where+ type Weak 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+```++Note that a strong type may have 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, and aids type+inference.++See the documentation on Hackage for further details.+ ## Cool points-### Validates as much as possible-This is primarily a validation library. Thus, we don't fail on the first error--- we attempt to validate every part of a data type, and collate the errors into-a big list. (`ApplicativeDo` plus `Validation` is magical.)+### Extreme error clarity+strongweak is primarily a validation library. As such, strengthening failure+handling receives special attention: + * Failures do not short-circuit; if a strengthening is made up of multiple+ smaller strengthenings, all are run and any failures collated.+ * Failures display the weak and strong (target) type.+ * Generic strengthening is scarily verbose: see below for details.+ ### One definition, strong + weak views Using a type-level `Strength` switch and the `SW` type family, you can write a single datatype definition and receive both a strong and a weak representation, which the generic derivers can work with. See the `Strongweak.SW` module for details. -### Generic strengthening is extremely powerful+### Powerful generic instances There are generic derivers for generating `Strengthen` and `Weaken` instances-between arbitrary data types. The `Strengthen` instances annotate errors-extensively, telling you the datatype & record for which strengthening failed --recursively, for nested types!+between *compatible* data types. The `Strengthen` instances annotate errors+extensively, telling you the datatype, constructor and field for which+strengthening failed! -Note that the generic derivers work with any pair of matching data types. But-they must match very closely: both types are traversed in tandem, so every pair-of fields must be compatible. If you need to do calculation to move between your-strong and weak types, consider splitting it into calculation -> strengthening-and using the generic derivers. Or write your own instances.+Two types are *compatible* if + * their generic SOP representations match precisely, and+ * every pair of leaf types is either identical or has the appropriate+ strengthen/weaken instance++The `SW` type family is here to help for accomplishing that. Otherwise, if your+types don't fit:++ * convert to a "closer" representation first+ * write your own instances (fairly simple with `ApplicativeDo`).+ ### Backdoors included Sometimes you have can guarantee that a weak value can be safely strengthened, but the compiler doesn't know - a common problem in parsing. In such cases, you may use efficient unsafe strengthenings, which don't perform invariant checks.+Even better, they might explode your computer if you use them wrong! ## What this library isn't ### Not a convertible@@ -70,13 +138,19 @@ [witch](https://hackage.haskell.org/package/witch) library. ### Not particularly speedy-The emphasis is on safety, possibly at the detriment of performance. However, my-expectation is that you only strengthen & weaken at the "edges" of your program,-and most of the time will be spent transforming weak representations. This may-improve performance if it means invariants don't have to be continually asserted-inline, but it also may slow things down e.g. `Natural`s are slower than-`Word`s.+The emphasis is on safety, which may come at the detriment of performance: + * Strengthening and weakening might be slow. This depends on the type and the+ implementation. I try a little to ensure good performance, but not a lot.+ * Strong types can be more performant than their weak counterparts. For+ example, swapping all integrals for `Natural`s and `Integer`s will make your+ program slow.+ * You may avoid this fairly easily by simply not wrapping certain fields.++On the other hand, by only strengthening at the "edges" of your program and+knowing that between those you may transform the weak representation as you+like, you may find good performance easier to maintain.+ ## Related projects ### barbies The [barbies][lib-barbies-hackage] library is an investigation into how far the@@ -97,3 +171,10 @@ 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.)*++## Other+### Can this be formalized or generalized in some useful way?+I note that this library is basically a couple of type classes and utilities for+automating writing parsers and printers for types which are "close". I can't+find anything in the literature that discusses this sort of thing. If you would+have some info there, please do let me know!
src/Strongweak.hs view
@@ -1,12 +1,24 @@-{-# LANGUAGE UndecidableInstances #-}+{- | Main import module for basic use.++For defining 'Strengthen' instances, import "Strongweak.Strengthen".+-}+ module Strongweak ( -- * Instance design -- $strongweak-instance-design - -- * Re-exports- module Strongweak.Weaken- , module Strongweak.Strengthen+ -- * Classes+ Weaken(..)+ , Strengthen(..)++ -- * Other definitions+ , liftWeakF++ -- * Strength switch wrapper+ , Strength(..)+ , type SW+ ) where import Strongweak.Weaken
src/Strongweak/Generic/Strengthen.hs view
@@ -7,16 +7,19 @@ (D), constructor (C) and selector (S). -} +-- both required due to type class design {-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE UndecidableInstances #-} module Strongweak.Generic.Strengthen where import Strongweak.Strengthen import Data.Either.Validation-import Data.List.NonEmpty import GHC.Generics+import Data.Kind+import GHC.TypeNats+import GHC.Exts ( proxy#, Proxy# ) -import Numeric.Natural import Control.Applicative ( liftA2 ) -- | Strengthen a value generically.@@ -25,78 +28,88 @@ -- the definition of compatibility in this context. strengthenGeneric :: (Generic w, Generic s, GStrengthenD (Rep w) (Rep s))- => w -> Validation (NonEmpty StrengthenFail) s+ => w -> Result s strengthenGeneric = fmap to . gstrengthenD . from -- | Generic strengthening at the datatype level. class GStrengthenD w s where- gstrengthenD :: w p -> Validation (NonEmpty StrengthenFail) (s p)+ gstrengthenD :: w p -> Result (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+instance GStrengthenC wcd scd w s => GStrengthenD (D1 wcd w) (D1 scd s) where+ gstrengthenD = fmap M1 . gstrengthenC @wcd @scd . unM1 -- | Generic strengthening at the constructor sum level.-class GStrengthenC w s where- gstrengthenC :: String -> String -> w p -> Validation (NonEmpty StrengthenFail) (s p)+class GStrengthenC wcd scd w s where+ gstrengthenC :: w p -> Result (s p) -- | Nothing to do for empty datatypes.-instance GStrengthenC V1 V1 where- gstrengthenC _ _ = Success+instance GStrengthenC wcd scd V1 V1 where gstrengthenC = Success -- | 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+instance+ ( GStrengthenC wcd scd wl sl+ , GStrengthenC wcd scd wr sr+ ) => GStrengthenC wcd scd (wl :+: wr) (sl :+: sr) where+ gstrengthenC = \case L1 l -> L1 <$> gstrengthenC @wcd @scd l+ R1 r -> R1 <$> gstrengthenC @wcd @scd 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.+instance GStrengthenS wcd scd wcc scc 0 w s+ => GStrengthenC wcd scd (C1 wcc w) (C1 scc s) where+ gstrengthenC = fmap M1 . gstrengthenS @wcd @scd @wcc @scc @0 . unM1 -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 -- ^ 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))+-- | Generic strengthening at the constructor level.+class GStrengthenS wcd scd wcc scc (si :: Natural) w s where+ gstrengthenS :: w p -> Result (s p) -- | Nothing to do for empty constructors.-instance GStrengthenS U1 U1 where- gstrengthenS _ _ _ _ n x = (n, Success x)+instance GStrengthenS wcd scd wcc scc si U1 U1 where gstrengthenS = Success -- | 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+instance+ ( GStrengthenS wcd scd wcc scc si wl sl+ , GStrengthenS wcd scd wcc scc (si + ProdArity wl) wr sr+ ) => GStrengthenS wcd scd wcc scc si (wl :*: wr) (sl :*: sr) where+ gstrengthenS (l :*: r) =+ liftA2 (:*:)+ (gstrengthenS @wcd @scd @wcc @scc @si l)+ (gstrengthenS @wcd @scd @wcc @scc @(si + ProdArity wl) 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)))+instance GStrengthenS wcd scd wcc scc si (S1 wcs (Rec0 a)) (S1 scs (Rec0 a)) where+ gstrengthenS = Success . M1 . unM1 -- | Strengthen a field using the existing 'Strengthen' instance.-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 = StrengthenFailField dw ds cw cs n fw n fs es- in (n, Failure $ e :| [])- Success s -> (n, Success $ M1 $ K1 s)+instance {-# OVERLAPS #-}+ ( Weak s ~ w -- has to be here, else "illegal typesym family app in instance"+ , Strengthen s+ , Datatype wcd, Datatype scd+ , Constructor wcc, Constructor scc+ , Selector wcs, Selector scs+ , KnownNat si+ ) => GStrengthenS wcd scd wcc scc si (S1 wcs (Rec0 w)) (S1 scs (Rec0 s)) where+ gstrengthenS = unM1 .> unK1 .> strengthen .> \case+ Success s -> Success $ M1 $ K1 s+ Failure es -> Failure $ pure e+ where+ e = FailField wcd scd wcc scc si wcs si scs es+ wcd = datatypeName' @wcd+ scd = datatypeName' @scd+ wcc = conName' @wcc+ scc = conName' @scc+ wcs = selName'' @wcs+ scs = selName'' @scs+ si = natVal'' @si +--------------------------------------------------------------------------------++-- from flow+(.>) :: (a -> b) -> (b -> c) -> a -> c+f .> g = g . f++--------------------------------------------------------------------------------+ -- | Get the record name for a selector if present. -- -- On the type level, a 'Maybe Symbol' is stored for record names. But the@@ -106,8 +119,6 @@ selName'' = case selName' @s of "" -> Nothing s -> Just s ---------------------------------------------------------------------------------- -- | 'conName' without the value (only used as a proxy). Lets us push our -- 'undefined's into one place. conName' :: forall c. Constructor c => String@@ -122,3 +133,15 @@ -- 'undefined's into one place. selName' :: forall s. Selector s => String selName' = selName @s undefined++--------------------------------------------------------------------------------++type family ProdArity (f :: Type -> Type) :: Natural where+ ProdArity (S1 c f) = 1+ ProdArity (l :*: r) = ProdArity l + ProdArity r++--------------------------------------------------------------------------------++natVal'' :: forall n. KnownNat n => Natural+natVal'' = natVal' (proxy# :: Proxy# n)+{-# INLINE natVal'' #-}
src/Strongweak/Strengthen.hs view
@@ -1,45 +1,60 @@ {-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE CPP #-}+{-# LANGUAGE AllowAmbiguousTypes #-} module Strongweak.Strengthen ( -- * 'Strengthen' class Strengthen(..)-- -- * Strengthen failures- , StrengthenFail(..)- , strengthenFailPretty- , strengthenFailBase-- -- * Restrengthening , restrengthen+ , Result - -- * Helpers+ -- ** Helpers , strengthenBounded + -- * Strengthen failures+ , Fails+ , Fail(..)+ , prettyFail++ -- ** Helpers+ , fail1+ , failOther+ , failShow+ , maybeFailShow+ -- * Re-exports , Strongweak.Weaken.Weak ) where +import Strongweak.Util.Typeable ( typeRep' )+import Strongweak.Util.Text ( tshow ) import Strongweak.Weaken ( Weaken(..) ) import Data.Either.Validation-import Type.Reflection ( Typeable, typeRep )-import Prettyprinter-import Prettyprinter.Render.String+import Data.Typeable ( Typeable, TypeRep )+import Prettyprinter qualified as Pretty+import Prettyprinter ( Pretty(pretty), (<+>) )+import Prettyprinter.Render.String qualified as Pretty+import Prettyprinter.Render.Text qualified as Pretty +import Data.Text ( Text )+import Data.Text.Lazy qualified as Text.Lazy import GHC.TypeNats ( Natural, KnownNat ) import Data.Word import Data.Int-import Refined ( Refined, refine, Predicate )+import Refined hiding ( Weaken, weaken, strengthen, NonEmpty ) import Data.Vector.Generic.Sized qualified as VGS -- Shazbot! import Data.Vector.Generic qualified as VG import Data.Foldable qualified as Foldable import Control.Applicative ( liftA2 ) import Data.Functor.Identity import Data.Functor.Const-import Data.List.NonEmpty ( NonEmpty( (:|) ) )+import Acc.NeAcc import Data.List.NonEmpty qualified as NonEmpty+import Data.List.NonEmpty ( NonEmpty ) +type Result = Validation Fails+type Fails = NeAcc Fail+ {- | Attempt to strengthen some @'Weak' a@, asserting certain invariants. We take 'Weaken' as a superclass in order to maintain strong/weak type pair@@ -53,7 +68,7 @@ class Weaken a => Strengthen a where -- | Attempt to strengthen some @'Weak' a@ to its associated strong type -- @a@.- strengthen :: Weak a -> Validation (NonEmpty StrengthenFail) a+ strengthen :: Weak a -> Result a -- | Weaken a strong value, then strengthen it again. --@@ -65,22 +80,31 @@ -- Failure ... restrengthen :: (Strengthen a, Weaken a)- => a -> Validation (NonEmpty StrengthenFail) a+ => a -> Result a restrengthen = strengthen . weaken --- | 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 StrengthenFail- = StrengthenFailBase- String -- ^ weak type- String -- ^ strong type- String -- ^ weak value- String -- ^ msg+-- | A failure encountered during strengthening.+data Fail+ -- | A failure containing lots of detail. Use in concrete instances where you+ -- already have the 'Show's and 'Typeable's needed.+ = FailShow+ TypeRep -- ^ weak type+ TypeRep -- ^ strong type+ (Maybe Text) -- ^ weak value+ [Text] -- ^ failure description - | StrengthenFailField+ -- | A failure. Use in abstract instances to avoid heavy contexts. (Remember+ -- that generic strengtheners should wrap these nicely anyway!)+ | FailOther+ [Text] -- ^ failure description++ -- | Some failures occurred when strengthening from one data type to another.+ --+ -- Field indices are from 0 in the respective constructor. Field names are+ -- provided if are present in the type.+ --+ -- This is primarily intended to be used by generic strengtheners.+ | FailField String -- ^ weak datatype name String -- ^ strong datatype name String -- ^ weak constructor name@@ -89,56 +113,102 @@ (Maybe String) -- ^ weak field name (if present) Natural -- ^ strong field index (Maybe String) -- ^ strong field name (if present)- (NonEmpty StrengthenFail) -- ^ failures- deriving stock Eq+ Fails -- ^ failures -instance Show StrengthenFail where- showsPrec _ = renderShowS . layoutPretty defaultLayoutOptions . pretty+prettyFail :: Fail -> Text.Lazy.Text+prettyFail = Pretty.renderLazy . prettyLayoutFail +prettyLayoutFail :: Fail -> Pretty.SimpleDocStream ann+prettyLayoutFail = Pretty.layoutPretty Pretty.defaultLayoutOptions . pretty++fail1 :: Fail -> Result a+fail1 = Failure . pure++failOther :: [Text] -> Result a+failOther = fail1 . FailOther++buildFailShow+ :: forall w s. (Typeable w, Typeable s)+ => Maybe Text -> [Text] -> Result s+buildFailShow mwv = fail1 . FailShow (typeRep' @w) (typeRep' @s) mwv++failShow'+ :: forall s w. (Typeable w, Show w, Typeable s)+ => (w -> Text) -> w -> [Text] -> Result s+failShow' f w = buildFailShow @w @s (Just (f w))++failShow+ :: forall s w. (Typeable w, Show w, Typeable s)+ => w -> [Text] -> Result s+failShow = failShow' tshow++-- | This reports the weak and strong type, so no need to include those in the+-- failure detail.+failShowNoVal :: forall w s. (Typeable w, Typeable s) => [Text] -> Result s+failShowNoVal = buildFailShow @w @s Nothing++instance Show Fail where+ showsPrec _ = Pretty.renderShowS . prettyLayoutFail+ -- TODO shorten value if over e.g. 50 chars. e.g. @[0,1,2,...,255] -> FAIL@-instance Pretty StrengthenFail where+instance Pretty Fail where pretty = \case- StrengthenFailBase wt st wv msg ->- vsep [ pretty wt<+>"->"<+>pretty st- , pretty wv<+>"->"<+>"FAIL"- , pretty msg ]- StrengthenFailField dw _ds cw _cs iw fw _is _fs es ->+ FailShow wt st mwv detail -> Pretty.vsep $+ case mwv of+ Nothing -> [typeDoc, detailDoc]+ Just wv ->+ let valueDoc = "value: "<+>pretty wv<+>"->"<+>"FAIL"+ in [typeDoc, valueDoc, detailDoc]+ where+ typeDoc = "type: "<+>prettyTypeRep wt<+>"->"<+>prettyTypeRep st+ detailDoc = case detail of+ [] -> "<no detail>"+ [detailLine] -> "detail:"<+>pretty detailLine+ _ -> "detail:"<>Pretty.line<>prettyList detail++ FailOther detail -> pretty detail++ -- TODO should inspect meta, shorten if identical (currently only using+ -- weak)+ FailField 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<>strengthenFailPretty es+ in Pretty.nest 0 $ pretty dw<>"."<>pretty cw<>"."<>pretty sw<>Pretty.line<>prettyList es -- mutually recursive with its 'Pretty' instance. safe, but a bit confusing - -- clean up-strengthenFailPretty :: NonEmpty StrengthenFail -> Doc a-strengthenFailPretty = vsep . map go . Foldable.toList- where go e = "-"<+>indent 0 (pretty e)+prettyList :: (Foldable f, Pretty a) => f a -> Pretty.Doc ann+prettyList = Pretty.vsep . map go . Foldable.toList+ where go e = "-"<+>Pretty.indent 0 (pretty e) -strengthenFailBase- :: forall s w. (Typeable w, Show w, Typeable s)- => w -> String -> Validation (NonEmpty StrengthenFail) s-strengthenFailBase w msg = Failure (e :| [])- where e = StrengthenFailBase (show $ typeRep @w) (show $ typeRep @s) (show w) msg+-- | Succeed on 'Just', fail with given detail on 'Nothing'.+maybeFailShow+ :: forall a. (Typeable (Weak a), Typeable a)+ => [Text] -> Maybe a -> Result a+maybeFailShow detail = \case+ Just a -> Success a+ Nothing -> failShowNoVal @(Weak a) detail -- | Assert a predicate to refine a type.-instance (Predicate (p :: k) a, Typeable k, Typeable a, Show a) => Strengthen (Refined p a) where- strengthen a =- case refine a of- Left err -> strengthenFailBase a (show err)- Right ra -> Success ra+instance (Predicate (p :: k) a, Typeable k, Typeable a)+ => Strengthen (Refined p a) where+ strengthen = refine .> \case+ Left rex -> failShowNoVal @a+ [ "refinement: "<>tshow (typeRep' @p)+ , "failed with..."+ , tshow (displayRefineException rex)+ ]+ Right ra -> Success ra -- | Strengthen a plain list into a non-empty list by asserting non-emptiness.-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"+instance Typeable a => Strengthen (NonEmpty a) where+ strengthen = NonEmpty.nonEmpty .> maybeFailShow ["empty list"] -- | Strengthen a plain list into a sized vector by asserting length.-instance (VG.Vector v a, KnownNat n, Typeable v, Typeable a, Show a)- => Strengthen (VGS.Vector v n a) where- strengthen w =- case VGS.fromList w of- Nothing -> strengthenFailBase w "TODO bad size vector"- Just s -> Success s+instance+ ( VG.Vector v a, KnownNat n+ , Typeable v, Typeable a+ ) => Strengthen (VGS.Vector v n a) where+ strengthen = VGS.fromList .> maybeFailShow ["incorrect length"] -- | Add wrapper. instance Strengthen (Identity a) where@@ -167,17 +237,23 @@ instance Strengthen Int32 where strengthen = strengthenBounded instance Strengthen Int64 where strengthen = strengthenBounded +-- | Strengthen one numeric type into another.+--+-- @n@ must be "wider" than @m@. strengthenBounded- :: forall b n- . (Integral b, Bounded b, Show b, Typeable b, Integral n, Show n, Typeable n)- => n -> Validation (NonEmpty StrengthenFail) b-strengthenBounded n =- if n <= maxB && n >= minB then Success (fromIntegral n)- else strengthenFailBase n $ "not well bounded, require: "- <>show minB<>" <= n <= "<>show maxB+ :: forall m n+ . ( Typeable n, Integral n, Show n+ , Typeable m, Integral m, Show m, Bounded m+ ) => n -> Result m+strengthenBounded n+ | n <= maxB && n >= minB = Success (fromIntegral n)+ | otherwise = failShow n+ [ "not well bounded, require: "+ <>tshow minB<>" <= n <= "<>tshow maxB+ ] where- maxB = fromIntegral @b @n maxBound- minB = fromIntegral @b @n minBound+ maxB = fromIntegral @m @n maxBound+ minB = fromIntegral @m @n minBound -------------------------------------------------------------------------------- @@ -193,3 +269,12 @@ instance (Strengthen a, Strengthen b) => Strengthen (Either a b) where strengthen = \case Left a -> Left <$> strengthen a Right b -> Right <$> strengthen b++--------------------------------------------------------------------------------++prettyTypeRep :: TypeRep -> Pretty.Doc a+prettyTypeRep = pretty . show++-- from flow+(.>) :: (a -> b) -> (b -> c) -> a -> c+f .> g = g . f
+ src/Strongweak/Util/Text.hs view
@@ -0,0 +1,7 @@+module Strongweak.Util.Text where++import Data.Text qualified as Text+import Data.Text ( Text )++tshow :: Show a => a -> Text+tshow = Text.pack . show
+ src/Strongweak/Util/Typeable.hs view
@@ -0,0 +1,8 @@+{-# LANGUAGE AllowAmbiguousTypes #-}++module Strongweak.Util.Typeable where++import Data.Typeable++typeRep' :: forall a. Typeable a => TypeRep+typeRep' = typeRep (Proxy @a)
src/Strongweak/Weaken.hs view
@@ -1,16 +1,18 @@+{-# LANGUAGE UndecidableInstances #-} -- for SWDepth+ module Strongweak.Weaken ( -- * 'Weaken' class Weaken(..) , liftWeakF - -- * 'SW' helper+ -- * Strength switch helper , Strength(..)- , SW+ , type SW+ , type SWDepth ) where import Refined ( Refined, unrefine )-import Numeric.Natural ( Natural ) import Data.Word import Data.Int import Data.Vector.Generic.Sized qualified as VGS -- Shazbot!@@ -20,6 +22,7 @@ import Data.Functor.Const import Data.List.NonEmpty qualified as NonEmpty import Data.List.NonEmpty ( NonEmpty )+import GHC.TypeNats {- | Weaken some @a@, relaxing certain invariants. @@ -32,7 +35,8 @@ -- | Weaken some @a@ to its associated weak type @'Weak' a@. weaken :: a -> Weak a --- | Lift a function on a weak type to the associated strong type.+-- | Lift a function on a weak type to the associated strong type by weakening+-- first. liftWeakF :: Weaken a => (Weak a -> b) -> (a -> b) liftWeakF f = f . weaken @@ -57,6 +61,12 @@ type family SW (s :: Strength) a :: Type where SW 'Strong a = a SW 'Weak a = Weak a++-- | 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) -- | Strip refined type refinement. instance Weaken (Refined p a) where
strongweak.cabal view
@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack name: strongweak-version: 0.4.1+version: 0.5.0 synopsis: Convert between strong and weak representations of types description: Please see README.md. category: Data@@ -35,6 +35,8 @@ Strongweak.Generic.Weaken Strongweak.Strengthen Strongweak.Strengthen.Unsafe+ Strongweak.Util.Text+ Strongweak.Util.Typeable Strongweak.Weaken other-modules: Paths_strongweak@@ -53,10 +55,12 @@ MagicHash ghc-options: -Wall build-depends:- base >=4.14 && <5+ acc >=0.2.0.1 && <0.3+ , base >=4.14 && <5 , either >=5.0.1.1 && <5.1 , prettyprinter >=1.7.1 && <1.8 , refined >=0.7 && <0.9+ , text >=1.2.5.0 && <2.1 , vector >=0.12.3.1 && <0.14 , vector-sized >=1.5.0 && <1.6 default-language: GHC2021@@ -87,6 +91,7 @@ hspec-discover:hspec-discover >=2.7 && <2.10 build-depends: QuickCheck >=2.14.2 && <2.15+ , acc >=0.2.0.1 && <0.3 , base >=4.14 && <5 , either >=5.0.1.1 && <5.1 , generic-random >=1.5.0.1 && <1.6@@ -95,6 +100,7 @@ , quickcheck-instances >=0.3.26 && <0.4 , refined >=0.7 && <0.9 , strongweak+ , text >=1.2.5.0 && <2.1 , vector >=0.12.3.1 && <0.14 , vector-sized >=1.5.0 && <1.6 default-language: GHC2021
test/Common.hs view
@@ -1,6 +1,7 @@ module Common where import Strongweak+import Strongweak.Strengthen qualified as Strengthen import Strongweak.Generic import Refined hiding ( Weaken, weaken, strengthen, NonEmpty ) import GHC.Generics ( Generic )@@ -9,6 +10,7 @@ import Numeric.Natural ( Natural ) import Data.Word import Test.QuickCheck.Instances.Natural()+import Data.Either.Validation data DS (s :: Strength) = DS0 (SW s Word8) (SW s Word8) Word8 (SW s Word8) (SW s Word8)@@ -48,3 +50,6 @@ type Weak (DP 'Strong) = DP 'Weak weaken = weakenGeneric instance Strengthen (DP 'Strong) where strengthen = strengthenGeneric++tryStrengthenSuccessEq :: Eq a => a -> Strengthen.Result a -> Bool+tryStrengthenSuccessEq a = \case Success a' -> a == a'; Failure{} -> False
test/Strongweak/LawsSpec.hs view
@@ -9,10 +9,11 @@ spec :: Spec spec = modifyMaxSize (+1000) $ do prop "weaken-strengthen roundtrip isomorphism (generic)" $ do- \(d :: DS 'Strong) -> strengthen (weaken d) `shouldBe` Success d+ \(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- Failure _ -> pure ()+ Failure{} -> pure () Success ds ->- strengthen (weaken ds) `shouldBe` Success ds+ strengthen (weaken ds) `shouldSatisfy` tryStrengthenSuccessEq ds
test/Strongweak/StrengthenSpec.hs view
@@ -1,63 +1,70 @@ module Strongweak.StrengthenSpec ( spec ) where +import Strongweak.Util.Typeable+import Strongweak.Util.Text import Strongweak+import Strongweak.Strengthen import Common import Data.Either.Validation import Test.Hspec import Numeric.Natural ( Natural ) import Data.Word-import Data.List.NonEmpty ( NonEmpty(..) ) import Data.Foldable qualified as Foldable+import Data.Typeable ( TypeRep ) spec :: Spec spec = do 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 = sfGeneric1- "DP" "DP" "DP" "DP" 0 (Just "dp1f0") 0 (Just "dp1f0")- "Natural" "Word32" w+ e = sfGenericSW1Show+ "DP" "DP" 0 (Just "dp1f0")+ (typeRep' @Natural) (typeRep' @Word32) w 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 = sfGeneric1- "DS" "DS" "DS0" "DS0" 4 Nothing 4 Nothing- "Natural" "Word8" w+ e = sfGenericSW1Show+ "DS" "DS0" 4 Nothing+ (typeRep' @Natural) (typeRep' @Word8) w strengthen @(DS 'Strong) d `shouldSatisfy` svEqFail e -sfGeneric1+-- build strengthen failure+-- one failure, generic with SW, one wrapped failure (detailed)+sfGenericSW1Show :: Show w- => String -> String -> String -> String- -> Natural -> Maybe String -> Natural -> Maybe String- -> String -> String -> w- -> 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")+ => String -> String -> Natural -> Maybe String+ -> TypeRep -> TypeRep -> w+ -> Fail+sfGenericSW1Show d c i f tw ts w =+ FailField d d c c i f i f (pure e)+ where+ e = FailShow tw ts (Just (tshow w)) detail+ detail = error "tried to check failure descriptions in tests (bad idea)" -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'- && cs == cs'- && iw == iw'- && fw == fw'- && is == is'- && fs == fs'- && and (zipWith sfEqIgnoreMsg (Foldable.toList es) (Foldable.toList es'))+-- only test field and show, and ignore message in latter+sfEq :: Fail -> Fail -> Bool+sfEq s1 s2 = case s1 of+ FailField dw ds cw cs iw fw is fs es -> case s2 of+ FailField dw' ds' cw' cs' iw' fw' is' fs' es' ->+ dw == dw' && ds == ds'+ && cw == cw' && cs == cs'+ && iw == iw' && is == is'+ && fw == fw' && fs == fs'+ && and (zipWith sfEq (Foldable.toList es) (Foldable.toList es')) _ -> False- StrengthenFailBase wt st wv _ -> case s2 of- StrengthenFailBase wt' st' wv' _ ->- wt == wt'- && st == st'- && wv == wv'+ FailShow wt st wv _ -> case s2 of+ FailShow wt' st' wv' _ ->+ wt == wt' && st == st'+ && wv == wv' _ -> False+ _ -> error "unexpected strengthen fail" -svEqFail :: StrengthenFail -> Validation (NonEmpty StrengthenFail) s -> Bool-svEqFail e = \case Failure (e' :| []) -> sfEqIgnoreMsg e e'- _ -> False+svEqFail :: Fail -> Result s -> Bool+svEqFail e = \case+ Success{} -> False+ Failure es ->+ case Foldable.toList es of+ [e'] -> sfEq e e'+ _ -> False