strongweak 0.1.0 → 0.2.0
raw patch · 13 files changed
+461/−57 lines, 13 filesdep +QuickCheckdep +eitherdep +generic-randomdep −validation
Dependencies added: QuickCheck, either, generic-random, hspec, quickcheck-instances, strongweak, vector
Dependencies removed: validation
Files
- CHANGELOG.md +7/−0
- README.md +89/−16
- src/Strongweak.hs +17/−1
- src/Strongweak/Generic/Strengthen.hs +44/−22
- src/Strongweak/Generic/Weaken.hs +2/−0
- src/Strongweak/Strengthen.hs +44/−15
- src/Strongweak/Strengthen/Unsafe.hs +58/−0
- src/Strongweak/Weaken.hs +1/−1
- strongweak.cabal +71/−2
- test/Common.hs +46/−0
- test/Spec.hs +1/−0
- test/Strongweak/LawsSpec.hs +18/−0
- test/Strongweak/StrengthenSpec.hs +63/−0
CHANGELOG.md view
@@ -1,3 +1,10 @@+## 0.2.0 (2022-05-31)+Initial Hackage release (dependency issues prevented uploading).++ * fix field indexing in generic errors+ * add unsafe strengthening+ * add property and error tests+ ## 0.1.0 (2022-05-16) Initial release.
README.md view
@@ -1,24 +1,97 @@+[lib-refined-hackage]: https://hackage.haskell.org/package/refined+ # strongweak-Definitions for transforming between types.+Convert between pairs of "weak" and "strong"/"validated" types, with good+errors and generic derivers. - * `strong -> weak` drops invariants (e.g. going from a bounded to an unbounded- numeric type)- * `weak -> Maybe strong` introduces invariants+## Definition of strong and weak types+Take a pair of types `(strong, weak)`. We state the following: -This is not a `Convertible` library that enumerates transformations between-types into a dictionary.+ * 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. - * A "strong" type has exactly one "weak" representation.- * Weakening a type is safe.- * Strengthening a type may fail.+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. +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.++### 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.++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.++## 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.)++### 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 There are generic derivers for generating `Strengthen` and `Weaken` instances-for arbitrary data types. The `Strengthen` instances annotate errors+between arbitrary data types. The `Strengthen` instances annotate errors extensively, telling you the datatype & record for which strengthening failed --recursively, for nested types.+recursively, for nested types! -This is a validation library. We don't fail on the first error -- we attempt to-validate every part of a data type, and collate the errors into a list. This-happens magically in the generic deriver, but if you're writing your own-instances, you may want `ApplicativeDo` so you can use do notation. So it'll-monadic, but actually everything will get checked.+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.++### 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.++## What this library isn't+### Not a convertible+This is not a `Convertible` library that enumerates transformations between+types into a dictionary. A strong type has exactly one weak representation, and+strengthening may fail while weakening cannot. For safe conversion enumeration+via typeclasses, consider Taylor Fausak's+[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.++## 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:++ * 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.++Note this may fail for types with a manually-derived `Generic` instance:++ * 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).
src/Strongweak.hs view
@@ -1,9 +1,25 @@ module Strongweak ( module Strongweak.Weaken- , module Strongweak.Strengthen+ , module Strongweak.Strengthen, restrengthen , module Strongweak.SW ) where import Strongweak.Weaken import Strongweak.Strengthen import Strongweak.SW++import Data.Either.Validation+import Data.List.NonEmpty++-- | 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
src/Strongweak/Generic/Strengthen.hs view
@@ -1,22 +1,24 @@-{- |-The generic derivation is split into 3 classes, dealing with different layers of-a Haskell data type: datatype, constructor and selector. 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.+{- | Strengthening for generic data types.++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. -} {-# LANGUAGE AllowAmbiguousTypes #-}-{-# LANGUAGE ApplicativeDo #-} module Strongweak.Generic.Strengthen where import Strongweak.Strengthen-import Data.Validation+import Data.Either.Validation import Data.List.NonEmpty- import GHC.Generics +import Numeric.Natural+import Control.Applicative ( liftA2 )+ strengthenGeneric :: (Generic w, Generic s, GStrengthenD (Rep w) (Rep s)) => w -> Validation (NonEmpty StrengthenError) s@@ -36,7 +38,7 @@ gstrengthenC _ _ = Success instance (GStrengthenS w s, Constructor cw, Constructor cs) => GStrengthenC (C1 cw w) (C1 cs s) where- gstrengthenC dw ds = fmap M1 . gstrengthenS dw ds (conName' @cw) (conName' @cs) . unM1+ gstrengthenC dw ds = fmap M1 . snd . gstrengthenS dw ds (conName' @cw) (conName' @cs) 0 . unM1 -- | Strengthen sum types by strengthening left or right. instance (GStrengthenC lw ls, GStrengthenC rw rs) => GStrengthenC (lw :+: rw) (ls :+: rs) where@@ -44,29 +46,49 @@ R1 r -> R1 <$> gstrengthenC dw ds r class GStrengthenS w s where- gstrengthenS :: String -> String -> String -> String -> w p -> Validation (NonEmpty StrengthenError) (s p)+ gstrengthenS :: String -> String -> String -> String -> Natural -> w p -> (Natural, Validation (NonEmpty StrengthenError) (s p)) -- | Nothing to do for empty constructors. instance GStrengthenS U1 U1 where- gstrengthenS _ _ _ _ = Success+ gstrengthenS _ _ _ _ n x = (n, Success x) -- | 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 _ _ _ _ = Success . M1 . unM1+ 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- gstrengthenS dw ds cw cs (M1 (K1 w)) =+ gstrengthenS dw ds cw cs n (M1 (K1 w)) = case strengthen w of- Failure (e :| es) -> Failure $ StrengthenErrorField dw ds cw cs (selName' @mw) (selName' @ms) e :| es- Success s -> Success $ M1 $ K1 s+ Failure es ->+ let fw = selName'' @mw+ fs = selName'' @ms+ e = StrengthenErrorField dw ds cw cs n fw n fs es+ in (n, Failure $ e :| [])+ Success s -> (n, Success $ M1 $ K1 s) --- | Strengthen product types by strengthening left, then right.+-- | Get the record name for a selector if present.+--+-- On the type level, a 'Maybe Symbol' is stored for record names. But the+-- reification is done using @fromMaybe ""@. So we have to inspect the resulting+-- string to determine whether the field uses record syntax or not. (Silly.)+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 (l :*: r) = do- l' <- gstrengthenS dw ds cw cs l- r' <- gstrengthenS dw ds cw cs r- return $ l' :*: r'+ 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 -------------------------------------------------------------------------------- @@ -80,7 +102,7 @@ datatypeName' :: forall d. Datatype d => String datatypeName' = datatypeName @d undefined --- | 'datatypeName' without the value (only used as a proxy). Lets us push our+-- | 'selName' without the value (only used as a proxy). Lets us push our -- 'undefined's into one place. selName' :: forall s. Selector s => String selName' = selName @s undefined
src/Strongweak/Generic/Weaken.hs view
@@ -1,3 +1,5 @@+-- | Weakening for generic data types.+ module Strongweak.Generic.Weaken where import Strongweak.Weaken
src/Strongweak/Strengthen.hs view
@@ -1,5 +1,6 @@ {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE CPP #-} module Strongweak.Strengthen where @@ -14,7 +15,7 @@ import Prettyprinter import Prettyprinter.Render.String -import Data.Validation+import Data.Either.Validation import Data.List.NonEmpty ( NonEmpty( (:|) ) ) import Data.Foldable qualified as Foldable @@ -28,37 +29,61 @@ -} class Strengthen w s | s -> w where strengthen :: w -> Validation (NonEmpty StrengthenError) s +-- | '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++-- | Strengthen error 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 String String String String- -- ^ weak type, strong type, weak value, msg- | StrengthenErrorField String String String String String String StrengthenError- -- ^ weak datatype name, strong datatype name,- -- weak constructor name, strong constructor name,- -- weak field name, strong field name,- -- error+ = StrengthenErrorBase+ String -- ^ weak type+ String -- ^ strong type+ String -- ^ weak value+ String -- ^ msg + | StrengthenErrorField+ String -- ^ weak datatype name+ String -- ^ strong datatype name+ String -- ^ weak constructor name+ String -- ^ strong constructor name+ Natural -- ^ weak field index+ (Maybe String) -- ^ weak field name (if present)+ Natural -- ^ strong field index+ (Maybe String) -- ^ strong field name (if present)+ (NonEmpty StrengthenError) -- ^ errors+ deriving stock Eq+ instance Show StrengthenError 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 pretty = \case StrengthenErrorBase wt st wv msg -> vsep [ pretty wt<+>"->"<+>pretty st , pretty wv<+>"->"<+>"FAIL" , pretty msg ]- StrengthenErrorField dw _ds cw _cs sw _ss err ->- nest 1 $ pretty dw<>"."<>pretty cw<>"."<>pretty sw<>line<>pretty err+ StrengthenErrorField 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 +-- mutually recursive with its 'Pretty' instance. safe, but a bit confusing -+-- clean up+strengthenErrorPretty :: NonEmpty StrengthenError -> Doc a+strengthenErrorPretty = vsep . map go . Foldable.toList+ where go e = "-"<+>indent 0 (pretty e)+ strengthenErrorBase :: 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 -strengthenErrorPretty :: NonEmpty StrengthenError -> Doc a-strengthenErrorPretty = vsep . map go . Foldable.toList- where go e = "-"<+>indent 0 (pretty e)- -- | Strengthen each element of a list. instance Strengthen w s => Strengthen [w] [s] where strengthen = traverse strengthen@@ -71,7 +96,11 @@ Just s -> Success s -- | Obtain a refined type by applying its associated refinement.-instance (Predicate p a, Typeable a, Show a) => Strengthen a (Refined p a) where+#ifdef REFINED_POLYKIND+instance (Predicate (p :: k) a, Typeable k, Typeable a, Show a) => Strengthen a (Refined p a) where+#else+instance (Predicate p a, Typeable p, Typeable a, Show a) => Strengthen a (Refined p a) where+#endif strengthen a = case refine a of Left err -> strengthenErrorBase a (show err)
+ src/Strongweak/Strengthen/Unsafe.hs view
@@ -0,0 +1,58 @@+{-# LANGUAGE FunctionalDependencies #-}++module Strongweak.Strengthen.Unsafe where++import Numeric.Natural+import Data.Word+import Data.Int+import Refined ( Refined )+import Refined.Unsafe ( reallyUnsafeRefine )+import Data.Vector.Sized ( Vector )+import Data.Vector.Generic.Sized.Internal qualified+import Data.Vector qualified++{- | Any 'w' can be unsafely "strengthened" into an 's' by pretending that we've+ asserted some properties.++For example, you may unsafely strengthen some '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.++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++-- | 'unsafeStrengthen' with reordered type variables for more convenient+-- visible type application.+unsafeStrengthen' :: forall s w. UnsafeStrengthen w s => w -> s+unsafeStrengthen' = unsafeStrengthen++-- | Unsafely strengthen each element of a list.+instance UnsafeStrengthen w s => UnsafeStrengthen [w] [s] where+ unsafeStrengthen = map unsafeStrengthen++-- | Obtain a sized vector by unsafely assuming the size of a plain list.+-- Extremely unsafe.+instance UnsafeStrengthen [a] (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+ 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++-- 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
src/Strongweak/Weaken.hs view
@@ -18,7 +18,7 @@ -} class Weaken s w | s -> w where weaken :: s -> w --- | Weaken each element of a list.+-- | Weaken each element of a list instance Weaken s w => Weaken [s] [w] where weaken = map weaken -- | Weaken sized vectors into plain lists.
strongweak.cabal view
@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack name: strongweak-version: 0.1.0+version: 0.2.0 synopsis: Convert between strong and weak representations of types description: Please see README.md. category: Data@@ -26,6 +26,11 @@ type: git location: https://github.com/raehik/strongweak +flag refined-polykind+ description: assume predicate p in Refined p a is polykinded+ manual: True+ default: False+ library exposed-modules: Strongweak@@ -34,6 +39,7 @@ Strongweak.Generic.Strengthen Strongweak.Generic.Weaken Strongweak.Strengthen+ Strongweak.Strengthen.Unsafe Strongweak.SW Strongweak.Weaken other-modules:@@ -75,8 +81,71 @@ ghc-options: -Wall build-depends: base >=4.14 && <5+ , either >=5.0.1.1 && <5.1 , prettyprinter >=1.7.1 && <1.8 , refined >=0.6.3 && <0.7- , validation >=1.1.2 && <1.2+ , vector >=0.12.3.1 && <0.13 , vector-sized >=1.5.0 && <1.6+ if flag(refined-polykind)+ cpp-options: -DREFINED_POLYKIND+ default-language: Haskell2010++test-suite spec+ type: exitcode-stdio-1.0+ main-is: Spec.hs+ other-modules:+ Common+ Strongweak.LawsSpec+ Strongweak.StrengthenSpec+ Paths_strongweak+ hs-source-dirs:+ test+ default-extensions:+ EmptyCase+ FlexibleContexts+ FlexibleInstances+ InstanceSigs+ MultiParamTypeClasses+ PolyKinds+ LambdaCase+ DerivingStrategies+ StandaloneDeriving+ DeriveAnyClass+ DeriveGeneric+ DeriveDataTypeable+ DeriveFunctor+ DeriveFoldable+ DeriveTraversable+ DeriveLift+ ImportQualifiedPost+ StandaloneKindSignatures+ DerivingVia+ RoleAnnotations+ TypeApplications+ DataKinds+ TypeFamilies+ TypeOperators+ BangPatterns+ GADTs+ DefaultSignatures+ RankNTypes+ UndecidableInstances+ MagicHash+ ScopedTypeVariables+ build-tool-depends:+ hspec-discover:hspec-discover >=2.7 && <2.10+ build-depends:+ QuickCheck >=2.14.2 && <2.15+ , base >=4.14 && <5+ , either >=5.0.1.1 && <5.1+ , generic-random >=1.5.0.1 && <1.6+ , hspec >=2.7 && <2.10+ , prettyprinter >=1.7.1 && <1.8+ , quickcheck-instances >=0.3.26 && <0.4+ , refined >=0.6.3 && <0.7+ , strongweak+ , vector >=0.12.3.1 && <0.13+ , vector-sized >=1.5.0 && <1.6+ if flag(refined-polykind)+ cpp-options: -DREFINED_POLYKIND default-language: Haskell2010
+ test/Common.hs view
@@ -0,0 +1,46 @@+module Common where++import Strongweak+import Strongweak.Generic+import Refined hiding ( Weaken, weaken, strengthen, NonEmpty )+import GHC.Generics ( Generic )+import Generic.Random+import Test.QuickCheck ( Arbitrary )+import Numeric.Natural ( Natural )+import Data.Word+import Test.QuickCheck.Instances.Natural()++data DS (s :: Strength)+ = DS0 (SW s Word8) (SW s Word8) Word8 (SW s Word8) (SW s Word8)+ | DS1 (SW s (Refined (LessThan 100) Natural))+ deriving stock (Generic)++deriving stock instance Eq (DS 'Strong)+deriving stock instance Show (DS 'Strong)+deriving via (GenericArbitraryU `AndShrinking` (DS 'Strong)) instance Arbitrary (DS 'Strong)++deriving stock instance Eq (DS 'Weak)+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++data DP (s :: Strength) = DP+ { dp1f0 :: SW s Word32+ , dp1f1 :: SW s (Refined (GreaterThan 42) Natural)+ , dp1f2 :: SW s Word8+ , dp1f3 :: Word8+ , dp1f4 :: SW s Word8+ } deriving stock (Generic)++deriving stock instance Eq (DP 'Strong)+deriving stock instance Show (DP 'Strong)+deriving via (GenericArbitraryU `AndShrinking` (DP 'Strong)) instance Arbitrary (DP 'Strong)++deriving stock instance Eq (DP 'Weak)+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
+ test/Spec.hs view
@@ -0,0 +1,1 @@+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}
+ test/Strongweak/LawsSpec.hs view
@@ -0,0 +1,18 @@+module Strongweak.LawsSpec ( spec ) where++import Strongweak+import Common+import Data.Either.Validation+import Test.Hspec+import Test.Hspec.QuickCheck++spec :: Spec+spec = modifyMaxSize (+1000) $ do+ prop "weaken-strengthen roundtrip isomorphism (generic)" $ do+ \(d :: DS 'Strong) -> strengthen @(DS 'Weak) (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
+ test/Strongweak/StrengthenSpec.hs view
@@ -0,0 +1,63 @@+module Strongweak.StrengthenSpec ( spec ) where++import Strongweak+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++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 = seGeneric1+ "DP" "DP" "DP" "DP" 0 (Just "dp1f0") 0 (Just "dp1f0")+ "Natural" "Word32" w+ strengthen @_ @(DP 'Strong) d `shouldSatisfy` svEqError 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+ "DS" "DS" "DS0" "DS0" 4 Nothing 4 Nothing+ "Natural" "Word8" w+ strengthen @_ @(DS 'Strong) d `shouldSatisfy` svEqError e++seGeneric1+ :: 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")++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' ->+ dw == dw'+ && ds == ds'+ && cw == cw'+ && cs == cs'+ && iw == iw'+ && fw == fw'+ && is == is'+ && fs == fs'+ && and (zipWith seEqIgnoreMsg (Foldable.toList es) (Foldable.toList es'))+ _ -> False+ StrengthenErrorBase wt st wv _ -> case s2 of+ StrengthenErrorBase 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