strongweak 0.6.1 → 0.7.0
raw patch · 15 files changed
+455/−509 lines, 15 filesdep +rerefineddep +text-builder-lineardep −accdep −prettyprinterdep −refined1dep ~QuickCheckdep ~basedep ~text
Dependencies added: rerefined, text-builder-linear
Dependencies removed: acc, prettyprinter, refined1
Dependency ranges changed: QuickCheck, base, text
Files
- CHANGELOG.md +4/−0
- README.md +0/−1
- src/Strongweak/Generic.hs +50/−3
- src/Strongweak/Generic/Strengthen.hs +0/−147
- src/Strongweak/Generic/Via.hs +0/−47
- src/Strongweak/Generic/Weaken.hs +0/−46
- src/Strongweak/Strengthen.hs +103/−163
- src/Strongweak/Strengthen/Generic.hs +213/−0
- src/Strongweak/Strengthen/Unsafe.hs +2/−3
- src/Strongweak/Util/TypeNats.hs +10/−0
- src/Strongweak/Weaken.hs +6/−6
- src/Strongweak/Weaken/Generic.hs +45/−0
- strongweak.cabal +17/−19
- test/Common.hs +5/−4
- test/Strongweak/StrengthenSpec.hs +0/−70
CHANGELOG.md view
@@ -1,3 +1,7 @@+## 0.7.0 (2024-05-11)+* replaced refined1 with rerefined+* simplify failures+ ## 0.6.1 (2024-04-03) * tests: relax hspec upper bound
README.md view
@@ -100,7 +100,6 @@ * 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
src/Strongweak/Generic.hs view
@@ -1,3 +1,5 @@+{-# LANGUAGE UndecidableInstances #-} -- required due to nested constraints+ -- | Generic 'strengthen' and 'weaken'. module Strongweak.Generic@@ -13,10 +15,14 @@ , GenericallySW(..) ) where -import Strongweak.Generic.Weaken-import Strongweak.Generic.Strengthen-import Strongweak.Generic.Via+import Strongweak.Weaken.Generic+import Strongweak.Strengthen.Generic +import Strongweak.Weaken ( Weaken(Weak, weaken) )+import Strongweak.Strengthen ( Strengthen(strengthen) )+import GHC.Generics+import Data.Kind ( Type )+ {- $generic-derivation-compatibility The 'Strengthen' and 'Weaken' generic derivers allow you to derive instances@@ -41,3 +47,44 @@ metadata for you, but manually-derived Generic instances (which are usually a bad idea) do not require it. -}++{- | @DerivingVia@ wrapper for strongweak instances.++We can't use 'Generically' conveniently because we need to talk about two data+types, not one -- we would have to do something like @'Generically' ('Tagged' w+s)@, which is ugly. So we instead define our own adorable little "via type"+here!++Use like so:++@+data XYZ (s :: Strength) = XYZ+ { xyz1 :: SW s Word8+ , xyz2 :: Word8+ , xyz3 :: ()+ } deriving stock Generic+deriving via (GenericallySW (XYZ 'Strong) (XYZ 'Weak)) instance Weaken (XYZ 'Strong)+deriving via (GenericallySW (XYZ 'Strong) (XYZ 'Weak)) instance Strengthen (XYZ 'Strong)+@++TODO can't figure out a way around multiple standalone deriving declarations :(++TODO maybe GenericallySW1? but even so instances differ between weaken and+strengthen (weaken needs nothing) so it's kinda better this way. :)+-}++newtype GenericallySW s (w :: Type) = GenericallySW { unGenericallySW :: s }++instance+ ( Generic s, Generic w+ , GWeaken (Rep s) (Rep w)+ ) => Weaken (GenericallySW s w) where+ type Weak (GenericallySW s w) = w+ weaken = weakenGeneric . unGenericallySW++instance+ ( Generic s, Generic w+ , GStrengthenD (Rep w) (Rep s)+ , Weaken (GenericallySW s w)+ ) => Strengthen (GenericallySW s w) where+ strengthen = fmap GenericallySW . strengthenGeneric
− src/Strongweak/Generic/Strengthen.hs
@@ -1,147 +0,0 @@-{- | 'strengthen' over generic representations.--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).--}---- both required due to type class design-{-# LANGUAGE AllowAmbiguousTypes #-}-{-# LANGUAGE UndecidableInstances #-}--module Strongweak.Generic.Strengthen where--import Strongweak.Strengthen-import Data.Either.Validation-import GHC.Generics-import Data.Kind-import GHC.TypeNats-import GHC.Exts ( proxy#, Proxy# )--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 -> Result s-strengthenGeneric = fmap to . gstrengthenD . from---- | Generic strengthening at the datatype level.-class GStrengthenD w s where- gstrengthenD :: w p -> Result (s p)---- | Enter a datatype, stripping its metadata wrapper.-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 wcd scd w s where- gstrengthenC :: w p -> Result (s p)---- | Nothing to do for empty datatypes.-instance GStrengthenC wcd scd V1 V1 where gstrengthenC = Success---- | Strengthen sum types by casing and strengthening left or right.-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 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---- | 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 wcd scd wcc scc si U1 U1 where gstrengthenS = Success---- | Strengthen product types by strengthening left and right.-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 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 #-}- ( 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--- 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---- | 'conName' without the value (only used as a proxy). Lets us push our--- 'undefined's into one place.-conName' :: forall c. Constructor c => String-conName' = conName @c undefined---- | 'datatypeName' without the value (only used as a proxy). Lets us push our--- 'undefined's into one place.-datatypeName' :: forall d. Datatype d => String-datatypeName' = datatypeName @d undefined---- | '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------------------------------------------------------------------------------------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/Generic/Via.hs
@@ -1,47 +0,0 @@-{-# LANGUAGE UndecidableInstances #-} -- required due to nested constraints--module Strongweak.Generic.Via where--import Strongweak.Generic.Weaken-import Strongweak.Generic.Strengthen-import Strongweak-import GHC.Generics-import Data.Kind--{- | @DerivingVia@ wrapper for strongweak instances.--We can't use 'Generically' conveniently because we need to talk about two data-types, not one -- we would have to do something like @'Generically' ('Tagged' w-s)@, which is ugly. So we instead define our own adorable little "via type"-here!--Use like so:--@-data XYZ (s :: Strength) = XYZ- { xyz1 :: SW s Word8- , xyz2 :: Word8- , xyz3 :: ()- } deriving stock Generic-deriving via (GenericallySW (XYZ 'Strong) (XYZ 'Weak)) instance Weaken (XYZ 'Strong)-deriving via (GenericallySW (XYZ 'Strong) (XYZ 'Weak)) instance Strengthen (XYZ 'Strong)-@--TODO can't figure out a way around multiple standalone deriving declarations :(--}--newtype GenericallySW s (w :: Type) = GenericallySW { unGenericallySW :: s }--instance- ( Generic s, Generic w- , GWeaken (Rep s) (Rep w)- ) => Weaken (GenericallySW s w) where- type Weak (GenericallySW s w) = w- weaken = weakenGeneric . unGenericallySW--instance- ( Generic s, Generic w- , GStrengthenD (Rep w) (Rep s)- , Weaken (GenericallySW s w)- ) => Strengthen (GenericallySW s w) where- strengthen = fmap GenericallySW . strengthenGeneric
− src/Strongweak/Generic/Weaken.hs
@@ -1,46 +0,0 @@--- | 'weaken' over generic representations.--module Strongweak.Generic.Weaken where--import Strongweak.Weaken--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--class GWeaken s w where- gweaken :: s p -> w p---- | Strip all meta.-instance GWeaken s w => GWeaken (M1 is ms s) (M1 iw mw w) where- gweaken = M1 . gweaken . unM1---- | Nothing to do for empty datatypes.-instance GWeaken V1 V1 where- gweaken = id---- | Nothing to do for empty constructors.-instance GWeaken U1 U1 where- gweaken = id---- | Special case: if source and target types are equal, copy the value through.-instance GWeaken (Rec0 s) (Rec0 s) where- gweaken = id---- | Weaken a field using the existing 'Weaken' instance.-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 casing and weakening left or right.-instance (GWeaken ls lw, GWeaken rs rw) => GWeaken (ls :+: rs) (lw :+: rw) where- gweaken = \case L1 l -> L1 $ gweaken l- R1 r -> R1 $ gweaken r
src/Strongweak/Strengthen.hs view
@@ -12,49 +12,38 @@ , strengthenBounded -- * Strengthen failures- , Fails- , Fail(..)- , prettyFail-- -- ** Helpers- , fail1- , failOther- , failShow- , maybeFailShow+ , StrengthenFailure(..)+ , failStrengthen1+ , failStrengthen -- * Re-exports , Strongweak.Weaken.Weak ) where import Strongweak.Util.Typeable ( typeRep' )-import Strongweak.Util.Text ( tshow )+import Strongweak.Util.TypeNats ( natVal'' ) import Strongweak.Weaken ( Weaken(..) ) import Data.Either.Validation-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.Typeable ( Typeable ) -import Data.Text ( Text )-import Data.Text.Lazy qualified as Text.Lazy-import GHC.TypeNats ( Natural, KnownNat )+import GHC.TypeNats ( KnownNat ) import Data.Word import Data.Int-import Refined hiding ( Weaken, weaken, strengthen, NonEmpty )+import Rerefined 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 Acc.NeAcc import Data.List.NonEmpty qualified as NonEmpty import Data.List.NonEmpty ( NonEmpty ) -type Result = Validation Fails-type Fails = NeAcc Fail+import Data.Text.Builder.Linear qualified as TBL+import GHC.Exts ( fromString ) +import Data.Bits ( FiniteBits )++type Result = Validation StrengthenFailure+ {- | Attempt to strengthen some @'Weak' a@, asserting certain invariants. We take 'Weaken' as a superclass in order to maintain strong/weak type pair@@ -84,150 +73,67 @@ restrengthen = strengthen . weaken -- | 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-- -- | 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.+data StrengthenFailure = StrengthenFailure+ { strengthenFailDetail :: [TBL.Builder]+ -- ^ Detail on strengthen failure. --- -- This is primarily intended to be used by generic strengtheners.- | FailField- 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)- Fails -- ^ failures--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 Fail where- pretty = \case- 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+ -- We use a list here for the cases where you want multiple lines of detail.+ -- Separating with a newline would make prettifying later harder, so we delay. - -- 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 Pretty.nest 0 $ pretty dw<>"."<>pretty cw<>"."<>pretty sw<>Pretty.line<>prettyList es+ , strengthenFailInner :: [(TBL.Builder, StrengthenFailure)]+ -- ^ Indexed.+ } deriving stock Show --- mutually recursive with its 'Pretty' instance. safe, but a bit confusing ---- clean up-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)+failStrengthen+ :: [TBL.Builder] -> [(TBL.Builder, StrengthenFailure)] -> Result a+failStrengthen t fs = Failure $ StrengthenFailure t fs --- | 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+failStrengthen1 :: [TBL.Builder] -> Result a+failStrengthen1 t = failStrengthen t [] --- | Assert a predicate to refine a type.-instance (Predicate p a, Typeable a)- => Strengthen (Refined p a) where+-- | Strengthen a type by refining it with a predicate.+instance Refine p 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+ Right ra -> Success ra+ Left rf -> failStrengthen1+ [ "refinement failure:"+ , TBL.fromText (prettyRefineFailure rf) ]+ -- ^ TODO rerefined: provide a TBL pretty function --- | Assert a functor predicate to refine a type.-instance (Predicate1 p f, Typeable f, Typeable (a :: ak), Typeable ak)- => Strengthen (Refined1 p f a) where+-- | Strengthen a type by refining it with a functor predicate.+instance Refine1 p f => Strengthen (Refined1 p f a) where strengthen = refine1 .> \case- Left rex -> failShowNoVal @(f a)- [ "refinement: "<>tshow (typeRep' @p)- , "failed with..."- , tshow (displayRefineException rex)- ]- Right ra -> Success ra+ Right ra -> Success ra+ Left rf -> failStrengthen1+ [ "refinement failure:"+ , TBL.fromText (prettyRefineFailure rf) ] -- | Strengthen a plain list into a non-empty list by asserting non-emptiness.-instance Typeable a => Strengthen (NonEmpty a) where- strengthen = NonEmpty.nonEmpty .> maybeFailShow ["empty list"]+instance Strengthen (NonEmpty a) where+ strengthen = NonEmpty.nonEmpty .> \case+ Just neas -> Success neas+ Nothing -> failStrengthen1 $+ [ "type: [a] -> NonEmpty a"+ , "fail: empty list" ] -- | Strengthen a plain list into a sized vector by asserting length.-instance- ( VG.Vector v a, KnownNat n- , Typeable v, Typeable a- ) => Strengthen (VGS.Vector v n a) where- strengthen = VGS.fromList .> maybeFailShow ["incorrect length"]+instance (VG.Vector v a, KnownNat n) => Strengthen (VGS.Vector v n a) where+ -- TODO another case of TBL not supporting unbounded integrals+ strengthen as =+ case VGS.fromList as of+ Just va -> Success va+ Nothing -> failStrengthen1 $+ [ "type: [a] -> Vector v "<>fromString (show n)<>" a"+ , "fail: wrong length (got "<>TBL.fromDec (length as)<>")" ]+ where n = natVal'' @n -- | Add wrapper. instance Strengthen (Identity a) where- strengthen = pure <$> Identity+ strengthen = Success . Identity -- | Add wrapper. instance Strengthen (Const a b) where- strengthen = pure <$> Const+ strengthen = Success . Const {- TODO controversial. seems logical, but also kinda annoying. instance (Show a, Typeable a) => Strengthen (Maybe a) where@@ -251,30 +157,67 @@ -- | Strengthen one numeric type into another. -- -- @n@ must be "wider" than @m@.+--+-- @'FiniteBits' m@ and @'Show' n@ are for error printing. We're forced to+-- @'Show' n@ because linear-text-builder can't print unbounded integrals. PR:+-- https://github.com/Bodigrim/linear-builder/pull/20 strengthenBounded :: forall m n . ( Typeable n, Integral n, Show n- , Typeable m, Integral m, Show m, Bounded m+ , Typeable m, Integral m, Bounded m, FiniteBits 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+ | n <= maxBn && n >= minBn = Success (fromIntegral n)+ | otherwise = failStrengthen1+ [ "numeric strengthen: "<>fromString (show (typeRep' @n))+ <>" -> "<>fromString (show (typeRep' @m))+ , "bounds check does not hold: "+ <>TBL.fromDec minBm<>" <= "<>fromString (show n)+ <>" <= "<>TBL.fromDec maxBm ] where- maxB = fromIntegral @m @n maxBound- minB = fromIntegral @m @n minBound+ maxBn = fromIntegral @m @n maxBm+ minBn = fromIntegral @m @n minBm+ maxBm = maxBound @m+ minBm = minBound @m -------------------------------------------------------------------------------- -- | Decomposer. Strengthen every element in a list. instance Strengthen a => Strengthen [a] where- strengthen = traverse strengthen+ strengthen = strengthenList +strengthenList :: Strengthen a => [Weak a] -> Result [a]+strengthenList = goR (0 :: Int) [] . map strengthen+ where+ goR i as = \case+ r:rs ->+ case r of+ Success a -> goR (i+1) (a:as) rs+ Failure e -> goL (i+1) [(TBL.fromDec i, e)] rs+ [] -> Success as+ goL i es = \case+ r:rs ->+ case r of+ Success _ -> goL (i+1) es rs+ Failure e -> goL (i+1) ((TBL.fromDec i, e):es) rs+ [] -> failStrengthen ["list had failures"] es+ -- | Decomposer. Strengthen both elements of a tuple.-instance (Strengthen a, Strengthen b) => Strengthen (a, b) where- strengthen (a, b) = liftA2 (,) (strengthen a) (strengthen b)+instance (Strengthen l, Strengthen r) => Strengthen (l, r) where+ strengthen (l, r) =+ case strengthen l of+ Success sl ->+ case strengthen r of+ Success sr -> Success (sl, sr)+ Failure er -> failStrengthen ["2-tuple: right failed"]+ [("R", er)]+ Failure el ->+ case strengthen @r r of+ Success _ -> failStrengthen ["2-tuple: left failed"]+ [("L", el)]+ Failure er -> failStrengthen ["2-tuple: l&r failed"]+ [("R", er), ("L", el)] -- | Decomposer. Strengthen either side of an 'Either'. instance (Strengthen a, Strengthen b) => Strengthen (Either a b) where@@ -282,9 +225,6 @@ Right b -> Right <$> strengthen b ----------------------------------------------------------------------------------prettyTypeRep :: TypeRep -> Pretty.Doc a-prettyTypeRep = pretty . show -- from flow (.>) :: (a -> b) -> (b -> c) -> a -> c
+ src/Strongweak/Strengthen/Generic.hs view
@@ -0,0 +1,213 @@+{- | 'strengthen' over generic representations.++As with base instances, generic strengthening collates all failures rather than+short-circuiting on the first failure. Failures are annotated with precise+information describing where the failure occurred:++ * data type name+ * constructor name+ * field index+ * field name (if present)+-}++-- required due to type class design+{-# LANGUAGE AllowAmbiguousTypes, UndecidableInstances #-}++{-# LANGUAGE OverloadedStrings #-} -- required for failure++module Strongweak.Strengthen.Generic where++import Strongweak.Strengthen+import GHC.Generics+import Data.Either.Validation+import Data.Kind ( Type )+import GHC.TypeNats ( Natural, type (+), KnownNat )+import Control.Applicative qualified as A -- liftA2 export workaround+import Strongweak.Util.TypeNats ( natVal'' )+import Data.Text.Builder.Linear qualified as TBL+import GHC.Exts ( Symbol, fromString, proxy# )+import GHC.TypeLits ( KnownSymbol, symbolVal' )++{- TODO+So, now that we're improving the error story, we can do so here as well.++At product level in these generics, we know that neither data type names or+constructor names (weak or strong) will change. So individual fields can simply+annotate themselves with the weak & strong field identifiers. Then those can get+wrapped into a nice clean error higher up, that says "this constructor had the+following errors".++It's gonna look like the tuple and list 'Strengthen' instances but worse. Lots+of fiddly stuff.++Also, we can do the data type equality check I noted earlier. If weak & strong+data type names/constructor names match, we're probably doing @SW@ tricks, and+could probably shorten the error a bit.+-}++-- | 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 -> Result s+strengthenGeneric = fmap to . gstrengthenD . from++-- | Generic strengthening at the datatype level.+class GStrengthenD w s where+ gstrengthenD :: w p -> Result (s p)++-- | Strengthen a generic data type, replacing its metadata wrapping.+instance GStrengthenC wdn sdn w s+ => GStrengthenD+ (D1 (MetaData wdn _wmd2 _wmd3 _wmd4) w)+ (D1 (MetaData sdn _smd2 _smd3 _smd4) s) where+ gstrengthenD = fmap M1 . gstrengthenC @wdn @sdn . unM1++-- | Generic strengthening at the constructor sum level.+class GStrengthenC (wdn :: Symbol) (sdn :: Symbol) w s where+ gstrengthenC :: w p -> Result (s p)++-- | Nothing to do for empty datatypes.+instance GStrengthenC wdn sdn V1 V1 where gstrengthenC = Success++-- | Strengthen sum types by casing and strengthening left or right.+instance+ ( GStrengthenC wdn sdn wl sl+ , GStrengthenC wdn sdn wr sr+ ) => GStrengthenC wdn sdn (wl :+: wr) (sl :+: sr) where+ gstrengthenC = \case L1 l -> L1 <$> gstrengthenC @wdn @sdn l+ R1 r -> R1 <$> gstrengthenC @wdn @sdn r++-- | Enter a constructor, stripping its metadata wrapper.+instance (GStrengthenS 0 w s, ReifyCstrs wcd wcn scd scn)+ => GStrengthenC wcd scd+ (C1 (MetaCons wcn _wmc2 _wmc3) w)+ (C1 (MetaCons scn _smc2 _smc3) s) where+ gstrengthenC (M1 w) =+ case gstrengthenS @0 w of+ Success s -> Success (M1 s)+ Failure es -> failStrengthen [reifyCstrs @wcd @wcn @scd @scn] es++class ReifyCstrs (ld :: Symbol) (lc :: Symbol) (rd :: Symbol) (rc :: Symbol) where+ reifyCstrs :: TBL.Builder++-- | Special case: data type and constructor names are equivalent: simplify+instance {-# OVERLAPPING #-} (KnownSymbol d, KnownSymbol c)+ => ReifyCstrs d c d c where+ {-# INLINE reifyCstrs #-}+ reifyCstrs = d<>"."<>c+ where+ d = fromString (symbolVal' (proxy# @d))+ c = fromString (symbolVal' (proxy# @c))++instance (KnownSymbol ld, KnownSymbol lc, KnownSymbol rd, KnownSymbol rc)+ => ReifyCstrs ld lc rd rc where+ {-# INLINE reifyCstrs #-}+ reifyCstrs = ld<>"."<>lc<>" -> "<>rd<>"."<>rc+ where+ ld = fromString (symbolVal' (proxy# @ld))+ lc = fromString (symbolVal' (proxy# @lc))+ rd = fromString (symbolVal' (proxy# @rd))+ rc = fromString (symbolVal' (proxy# @rc))++-- | Generic strengthening at the constructor level.+class GStrengthenS (i :: Natural) w s where+ gstrengthenS :: w p -> Validation [(TBL.Builder, StrengthenFailure)] (s p)++-- | Nothing to do for empty constructors.+instance GStrengthenS i U1 U1 where gstrengthenS = Success++-- | Strengthen product types by strengthening left and right.+instance+ ( GStrengthenS i wl sl+ , GStrengthenS (i + ProdArity wl) wr sr+ ) => GStrengthenS i (wl :*: wr) (sl :*: sr) where+ gstrengthenS (l :*: r) =+ A.liftA2 (:*:)+ (gstrengthenS @i l)+ (gstrengthenS @(i + ProdArity wl) r)++-- | Special case: if source and target types are equivalent, just replace meta.+--+-- Note that we have to expand the metadata awkwardly for the overlapping+-- instances to work correctly. (There should be a better way to write this, but+-- it's purely style, so light TODO.)+instance {-# OVERLAPPING #-} GStrengthenS i+ (S1 (MetaSel _wms1 _wms2 _wms3 _wms4) (Rec0 a))+ (S1 (MetaSel _sms1 _sms2 _sms3 _sms4) (Rec0 a)) where+ gstrengthenS = Success . M1 . unM1++-- | Strengthen a field using the existing 'Strengthen' instance.+instance+ ( Weak s ~ w -- has to be here, else "illegal typesym family app in instance"+ , Strengthen s+ , ReifySelector i wmr smr+ ) => GStrengthenS i+ (S1 (MetaSel wmr _wms2 _wms3 _wms4) (Rec0 w))+ (S1 (MetaSel smr _sms2 _sms3 _sms4) (Rec0 s)) where+ gstrengthenS = unM1 .> unK1 .> strengthen .> \case+ Success s -> Success $ M1 $ K1 s+ Failure e -> Failure [(reifySelector @i @wmr @smr, e)]++{- TODO+* how to separate index and record name? @.@ is good and bad, uses same syntax+ as @dt.cstr@ for different reason BUT is pretty clear+* how to lay out precisely? fairly arbitrary+-}+class ReifySelector (i :: Natural) (l :: Maybe Symbol) (r :: Maybe Symbol) where+ reifySelector :: TBL.Builder++-- | Special case: both types had a record name, and they're equal+instance {-# OVERLAPPING #-} (KnownNat i, KnownSymbol lnm)+ => ReifySelector i (Just lnm) (Just lnm) where+ -- TODO check overlap works correct+ {-# INLINE reifySelector #-}+ reifySelector = i<>"."<>lnm+ where+ i = fromString $ show $ natVal'' @i+ lnm = fromString $ symbolVal' (proxy# @lnm)++instance (KnownNat i, KnownSymbol lnm, KnownSymbol rnm)+ => ReifySelector i (Just lnm) (Just rnm) where+ {-# INLINE reifySelector #-}+ reifySelector = i<>"."<>lnm<>" -> "<>rnm+ where+ i = fromString $ show $ natVal'' @i+ lnm = fromString $ symbolVal' (proxy# @lnm)+ rnm = fromString $ symbolVal' (proxy# @rnm)++instance KnownNat i => ReifySelector i Nothing Nothing where+ {-# INLINE reifySelector #-}+ reifySelector = fromString $ show $ natVal'' @i++instance (KnownNat i, KnownSymbol lnm)+ => ReifySelector i (Just lnm) Nothing where+ {-# INLINE reifySelector #-}+ reifySelector = i<>"."<>lnm+ where+ i = fromString $ show $ natVal'' @i+ lnm = fromString $ symbolVal' (proxy# @lnm)++instance (KnownNat i, KnownSymbol rnm)+ => ReifySelector i Nothing (Just rnm) where+ {-# INLINE reifySelector #-}+ reifySelector = i<>" -> "<>rnm+ where+ i = fromString $ show $ natVal'' @i+ rnm = fromString $ symbolVal' (proxy# @rnm)++--------------------------------------------------------------------------------++-- from flow+(.>) :: (a -> b) -> (b -> c) -> a -> c+f .> g = g . f++--------------------------------------------------------------------------------++-- could define this with @Generic.Type.Function.FoldMap.GTFoldMapC (+) 0 _@...+-- but pretty dumb LOL+type family ProdArity (f :: k -> Type) :: Natural where+ ProdArity (S1 c f) = 1+ ProdArity (l :*: r) = ProdArity l + ProdArity r
src/Strongweak/Strengthen/Unsafe.hs view
@@ -3,8 +3,7 @@ import Strongweak.Weaken import Data.Word import Data.Int-import Refined ( Refined )-import Refined.Unsafe ( reallyUnsafeRefine )+import Rerefined.Refine import Data.Vector.Generic.Sized qualified as VGS -- Shazbot! import Data.Vector.Generic qualified as VG import Data.Vector.Generic.Sized.Internal qualified@@ -37,7 +36,7 @@ -- | Add a refinement to a type without checking the associated predicate. instance UnsafeStrengthen (Refined p a) where- unsafeStrengthen = reallyUnsafeRefine+ unsafeStrengthen = unsafeRefine -- | Assume a plain list is non-empty. instance UnsafeStrengthen (NonEmpty a) where
+ src/Strongweak/Util/TypeNats.hs view
@@ -0,0 +1,10 @@+{-# LANGUAGE AllowAmbiguousTypes #-}++module Strongweak.Util.TypeNats where++import GHC.TypeNats+import GHC.Exts ( proxy# )++natVal'' :: forall n. KnownNat n => Natural+natVal'' = natVal' (proxy# @n)+{-# INLINE natVal'' #-}
src/Strongweak/Weaken.hs view
@@ -12,7 +12,7 @@ , type SWDepth ) where -import Refined ( Refined, unrefine, Refined1, unrefine1 )+import Rerefined import Data.Word import Data.Int import Data.Vector.Generic.Sized qualified as VGS -- Shazbot!@@ -35,15 +35,15 @@ -- | 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 by weakening--- first.-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++-- | 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 {- | Get either the strong or weak representation of a type, depending on the type-level "switch" provided.
+ src/Strongweak/Weaken/Generic.hs view
@@ -0,0 +1,45 @@+-- | 'weaken' over generic representations.++module Strongweak.Weaken.Generic where++import Strongweak.Weaken+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++class GWeaken s w where+ gweaken :: s p -> w p++-- | Strip all meta.+instance GWeaken s w => GWeaken (M1 is ms s) (M1 iw mw w) where+ gweaken = M1 . gweaken . unM1++-- | Nothing to do for empty datatypes.+instance GWeaken V1 V1 where+ gweaken = id++-- | Nothing to do for empty constructors.+instance GWeaken U1 U1 where+ gweaken = id++-- | Special case: if source and target types are equal, copy the value through.+instance {-# OVERLAPPING #-} GWeaken (Rec0 s) (Rec0 s) where+ gweaken = id++-- | Weaken a field using the existing 'Weaken' instance.+instance (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 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
strongweak.cabal view
@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack name: strongweak-version: 0.6.1+version: 0.7.0 synopsis: Convert between strong and weak representations of types description: Please see README.md. category: Data@@ -17,7 +17,8 @@ license-file: LICENSE build-type: Simple tested-with:- GHC ==9.2.2+ GHC==9.8+ , GHC==9.6 extra-source-files: README.md CHANGELOG.md@@ -30,14 +31,14 @@ exposed-modules: Strongweak Strongweak.Generic- Strongweak.Generic.Strengthen- Strongweak.Generic.Via- Strongweak.Generic.Weaken Strongweak.Strengthen+ Strongweak.Strengthen.Generic Strongweak.Strengthen.Unsafe Strongweak.Util.Text Strongweak.Util.Typeable+ Strongweak.Util.TypeNats Strongweak.Weaken+ Strongweak.Weaken.Generic other-modules: Paths_strongweak hs-source-dirs:@@ -53,14 +54,13 @@ TypeFamilies DataKinds MagicHash- ghc-options: -Wall+ ghc-options: -Wall -Wno-unticked-promoted-constructors build-depends:- acc >=0.2.0.1 && <0.3- , base >=4.14 && <5+ base >=4.17 && <5 , either >=5.0.1.1 && <5.1- , prettyprinter >=1.7.1 && <1.8- , refined1 ==0.9.*- , text >=1.2.5.0 && <2.1+ , rerefined >=0.4.0 && <0.5+ , text >=1.2.5.0 && <2.2+ , text-builder-linear >=0.1.2 && <0.2 , vector >=0.12.3.1 && <0.14 , vector-sized >=1.5.0 && <1.6 default-language: GHC2021@@ -71,7 +71,6 @@ other-modules: Common Strongweak.LawsSpec- Strongweak.StrengthenSpec Paths_strongweak hs-source-dirs: test@@ -86,21 +85,20 @@ TypeFamilies DataKinds MagicHash- ghc-options: -Wall+ ghc-options: -Wall -Wno-unticked-promoted-constructors build-tool-depends: hspec-discover:hspec-discover >=2.7 && <2.12 build-depends:- QuickCheck >=2.14.2 && <2.15- , acc >=0.2.0.1 && <0.3- , base >=4.14 && <5+ QuickCheck >=2.14.2 && <2.16+ , base >=4.17 && <5 , either >=5.0.1.1 && <5.1 , generic-random >=1.5.0.1 && <1.6 , hspec >=2.7 && <2.12- , prettyprinter >=1.7.1 && <1.8 , quickcheck-instances >=0.3.26 && <0.4- , refined1 ==0.9.*+ , rerefined >=0.4.0 && <0.5 , strongweak- , text >=1.2.5.0 && <2.1+ , text >=1.2.5.0 && <2.2+ , text-builder-linear >=0.1.2 && <0.2 , vector >=0.12.3.1 && <0.14 , vector-sized >=1.5.0 && <1.6 default-language: GHC2021
test/Common.hs view
@@ -3,9 +3,10 @@ import Strongweak import Strongweak.Strengthen qualified as Strengthen import Strongweak.Generic-import Refined hiding ( Weaken, weaken, strengthen, NonEmpty )+import Rerefined+import Rerefined.Predicates import GHC.Generics ( Generic )-import Generic.Random+import Generic.Random ( GenericArbitraryU(..), AndShrinking(..) ) import Test.QuickCheck ( Arbitrary ) import Numeric.Natural ( Natural ) import Data.Word@@ -14,7 +15,7 @@ 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))+ | DS1 (SW s (Refined (CompareValue LT Pos 100) Natural)) deriving stock (Generic) deriving stock instance Eq (DS 'Strong)@@ -32,7 +33,7 @@ data DP (s :: Strength) = DP { dp1f0 :: SW s Word32- , dp1f1 :: SW s (Refined (GreaterThan 42) Natural)+ , dp1f1 :: SW s (Refined (CompareValue GT Pos 42) Natural) , dp1f2 :: SW s Word8 , dp1f3 :: Word8 , dp1f4 :: SW s Word8
− test/Strongweak/StrengthenSpec.hs
@@ -1,70 +0,0 @@-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.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 = 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 = sfGenericSW1Show- "DS" "DS0" 4 Nothing- (typeRep' @Natural) (typeRep' @Word8) w- strengthen @(DS 'Strong) d `shouldSatisfy` svEqFail e---- build strengthen failure--- one failure, generic with SW, one wrapped failure (detailed)-sfGenericSW1Show- :: Show w- => 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)"---- 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- FailShow wt st wv _ -> case s2 of- FailShow wt' st' wv' _ ->- wt == wt' && st == st'- && wv == wv'- _ -> False- _ -> error "unexpected strengthen fail"--svEqFail :: Fail -> Result s -> Bool-svEqFail e = \case- Success{} -> False- Failure es ->- case Foldable.toList es of- [e'] -> sfEq e e'- _ -> False