strongweak (empty) → 0.1.0

raw patch · 13 files changed

+504/−0 lines, 13 filesdep +basedep +prettyprinterdep +refinedsetup-changed

Dependencies added: base, prettyprinter, refined, validation, vector-sized

Files

• CHANGELOG.md +6/−0
• LICENSE +20/−0
• README.md +24/−0
• Setup.hs +2/−0
• src/Strongweak.hs +9/−0
• src/Strongweak/Example.hs +43/−0
• src/Strongweak/Generic.hs +7/−0
• src/Strongweak/Generic/Strengthen.hs +86/−0
• src/Strongweak/Generic/Weaken.hs +40/−0
• src/Strongweak/SW.hs +45/−0
• src/Strongweak/Strengthen.hs +102/−0
• src/Strongweak/Weaken.hs +38/−0
• strongweak.cabal +82/−0

@@ -0,0 +1,6 @@+## 0.1.0 (2022-05-16)+Initial release.++  * basic instances (lists, numerics)+  * generic derivations+  * super explicit errors

@@ -0,0 +1,20 @@+Copyright (c) 2022 Ben Orchard (@raehik) <thefirstmuffinman@gmail.com>++Permission is hereby granted, free of charge, to any person obtaining+a copy of this software and associated documentation files (the+"Software"), to deal in the Software without restriction, including+without limitation the rights to use, copy, modify, merge, publish,+distribute, sublicense, and/or sell copies of the Software, and to+permit persons to whom the Software is furnished to do so, subject to+the following conditions:++The above copyright notice and this permission notice shall be included+in all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

@@ -0,0 +1,24 @@+# strongweak+Definitions for transforming between types.++  * `strong -> weak` drops invariants (e.g. going from a bounded to an unbounded+    numeric type)+  * `weak -> Maybe strong` introduces invariants++This is not a `Convertible` library that enumerates transformations between+types into a dictionary.++  * A "strong" type has exactly one "weak" representation.+  * Weakening a type is safe.+  * Strengthening a type may fail.++There are generic derivers for generating `Strengthen` and `Weaken` instances+for arbitrary data types. The `Strengthen` instances annotate errors+extensively, telling you the datatype & record for which strengthening failed -+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.

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

@@ -0,0 +1,9 @@+module Strongweak+  ( module Strongweak.Weaken+  , module Strongweak.Strengthen+  , module Strongweak.SW+  ) where++import Strongweak.Weaken+import Strongweak.Strengthen+import Strongweak.SW

@@ -0,0 +1,43 @@+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

@@ -0,0 +1,7 @@+module Strongweak.Generic+  ( weakenGeneric+  , strengthenGeneric+  ) where++import Strongweak.Generic.Weaken+import Strongweak.Generic.Strengthen

@@ -0,0 +1,86 @@+{- |+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.+-}++{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ApplicativeDo #-}++module Strongweak.Generic.Strengthen where++import Strongweak.Strengthen+import Data.Validation+import Data.List.NonEmpty++import GHC.Generics++strengthenGeneric+    :: (Generic w, Generic s, GStrengthenD (Rep w) (Rep s))+    => w -> Validation (NonEmpty StrengthenError) s+strengthenGeneric = fmap to . gstrengthenD . from++class GStrengthenD w s where+    gstrengthenD :: w p -> Validation (NonEmpty StrengthenError) (s p)++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++class GStrengthenC w s where+    gstrengthenC :: String -> String -> w p -> Validation (NonEmpty StrengthenError) (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 . gstrengthenS dw ds (conName' @cw) (conName' @cs) . unM1++-- | Strengthen sum types by 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++class GStrengthenS w s where+    gstrengthenS :: String -> String -> String -> String -> w p -> Validation (NonEmpty StrengthenError) (s p)++-- | Nothing to do for empty constructors.+instance GStrengthenS U1 U1 where+    gstrengthenS _ _ _ _ = Success++-- | 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++-- | Strengthen a field using the existing 'Strengthen' instance.+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)) =+        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++-- | Strengthen product types by strengthening left, then right.+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'++--------------------------------------------------------------------------------++-- | '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++-- | 'datatypeName' 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

@@ -0,0 +1,40 @@+module Strongweak.Generic.Weaken where++import Strongweak.Weaken++import GHC.Generics++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 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.+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

@@ -0,0 +1,45 @@+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

@@ -0,0 +1,102 @@+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE OverloadedStrings #-}++module Strongweak.Strengthen where++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 Prettyprinter+import Prettyprinter.Render.String++import Data.Validation+import Data.List.NonEmpty ( NonEmpty( (:|) ) )+import Data.Foldable qualified as Foldable++{- | Any 'w' can be "strengthened" into an 's' by asserting some properties.++For example, you may strengthen some 'Natural' @n@ into a 'Word8' by asserting+@0 <= n <= 255@.++Note that we restrict strengthened types to having only one corresponding weak+representation using functional dependencies.+-}+class Strengthen w s | s -> w where strengthen :: w -> Validation (NonEmpty StrengthenError) s++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++instance Show StrengthenError where+    showsPrec _ = renderShowS . layoutPretty defaultLayoutOptions . pretty++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++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++-- | 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+    strengthen w =+        case Vector.fromList w of+          Nothing -> strengthenErrorBase w "TODO bad size vector"+          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+    strengthen a =+        case refine a of+          Left  err -> strengthenErrorBase 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++-- 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++strengthenBounded+    :: forall b n+    .  (Integral b, Bounded b, Show b, Typeable b, Integral n, Show n, Typeable n)+    => n -> Validation (NonEmpty StrengthenError) b+strengthenBounded n =+    if   n <= maxB && n >= minB then Success (fromIntegral n)+    else strengthenErrorBase n $ "not well bounded, require: "+                                 <>show minB<>" <= n <= "<>show maxB+  where+    maxB = fromIntegral @b @n maxBound+    minB = fromIntegral @b @n minBound

@@ -0,0 +1,38 @@+{-# LANGUAGE FunctionalDependencies #-}++module Strongweak.Weaken where++import Refined ( Refined, unrefine )+import Numeric.Natural ( Natural )+import Data.Word+import Data.Int+import Data.Vector.Sized qualified as Vector+import Data.Vector.Sized ( Vector )++{- | Any 's' can be "weakened" into a 'w'.++For example, you may weaken a 'Word8' into a 'Natural'.++Note that we restrict strengthened types to having only one corresponding weak+representation using functional dependencies.+-}+class Weaken s w | s -> w where weaken :: s -> w++-- | Weaken each element of a list.+instance Weaken s w => Weaken [s] [w] where weaken = map weaken++-- | Weaken sized vectors into plain lists.+instance Weaken (Vector n a) [a] where weaken = Vector.toList++-- | Strip the refinement from refined types.+instance Weaken (Refined p a) a where 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

@@ -0,0 +1,82 @@+cabal-version: 1.12++-- This file has been generated from package.yaml by hpack version 0.34.4.+--+-- see: https://github.com/sol/hpack++name:           strongweak+version:        0.1.0+synopsis:       Convert between strong and weak representations of types+description:    Please see README.md.+category:       Data+homepage:       https://github.com/raehik/strongweak#readme+bug-reports:    https://github.com/raehik/strongweak/issues+author:         Ben Orchard+maintainer:     Ben Orchard <thefirstmuffinman@gmail.com>+license:        MIT+license-file:   LICENSE+build-type:     Simple+tested-with:+    GHC ==9.2.2+extra-source-files:+    README.md+    CHANGELOG.md++source-repository head+  type: git+  location: https://github.com/raehik/strongweak++library+  exposed-modules:+      Strongweak+      Strongweak.Example+      Strongweak.Generic+      Strongweak.Generic.Strengthen+      Strongweak.Generic.Weaken+      Strongweak.Strengthen+      Strongweak.SW+      Strongweak.Weaken+  other-modules:+      Paths_strongweak+  hs-source-dirs:+      src+  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+  ghc-options: -Wall+  build-depends:+      base >=4.14 && <5+    , prettyprinter >=1.7.1 && <1.8+    , refined >=0.6.3 && <0.7+    , validation >=1.1.2 && <1.2+    , vector-sized >=1.5.0 && <1.6+  default-language: Haskell2010