diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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). diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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.)* diff --git a/src/Strongweak.hs b/src/Strongweak.hs --- a/src/Strongweak.hs +++ b/src/Strongweak.hs @@ -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. + +-} diff --git a/src/Strongweak/Example.hs b/src/Strongweak/Example.hs deleted file mode 100644 --- a/src/Strongweak/Example.hs +++ /dev/null @@ -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 diff --git a/src/Strongweak/Generic.hs b/src/Strongweak/Generic.hs --- a/src/Strongweak/Generic.hs +++ b/src/Strongweak/Generic.hs @@ -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. +-} diff --git a/src/Strongweak/Generic/Strengthen.hs b/src/Strongweak/Generic/Strengthen.hs --- a/src/Strongweak/Generic/Strengthen.hs +++ b/src/Strongweak/Generic/Strengthen.hs @@ -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 -------------------------------------------------------------------------------- diff --git a/src/Strongweak/Generic/Weaken.hs b/src/Strongweak/Generic/Weaken.hs --- a/src/Strongweak/Generic/Weaken.hs +++ b/src/Strongweak/Generic/Weaken.hs @@ -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 diff --git a/src/Strongweak/SW.hs b/src/Strongweak/SW.hs deleted file mode 100644 --- a/src/Strongweak/SW.hs +++ /dev/null @@ -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 diff --git a/src/Strongweak/Strengthen.hs b/src/Strongweak/Strengthen.hs --- a/src/Strongweak/Strengthen.hs +++ b/src/Strongweak/Strengthen.hs @@ -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 diff --git a/src/Strongweak/Strengthen/Unsafe.hs b/src/Strongweak/Strengthen/Unsafe.hs --- a/src/Strongweak/Strengthen/Unsafe.hs +++ b/src/Strongweak/Strengthen/Unsafe.hs @@ -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 diff --git a/src/Strongweak/Weaken.hs b/src/Strongweak/Weaken.hs --- a/src/Strongweak/Weaken.hs +++ b/src/Strongweak/Weaken.hs @@ -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 diff --git a/strongweak.cabal b/strongweak.cabal --- a/strongweak.cabal +++ b/strongweak.cabal @@ -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 diff --git a/test/Common.hs b/test/Common.hs --- a/test/Common.hs +++ b/test/Common.hs @@ -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 diff --git a/test/Strongweak/LawsSpec.hs b/test/Strongweak/LawsSpec.hs --- a/test/Strongweak/LawsSpec.hs +++ b/test/Strongweak/LawsSpec.hs @@ -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 diff --git a/test/Strongweak/StrengthenSpec.hs b/test/Strongweak/StrengthenSpec.hs --- a/test/Strongweak/StrengthenSpec.hs +++ b/test/Strongweak/StrengthenSpec.hs @@ -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