refined-with (empty) → 0.1.0

raw patch · 6 files changed

+283/−0 lines, 6 filesdep +aesondep +basedep +deepseqsetup-changed

Dependencies added: aeson, base, deepseq, hashable, refined

Files

CHANGELOG.md +4/−0
LICENSE +20/−0
README.md +7/−0
Setup.hs +2/−0
refined-with.cabal +74/−0
src/Refined/WithRefine.hs +176/−0

+ CHANGELOG.md view

@@ -0,0 +1,4 @@+## 0.1.0 (2022-04-22)+Initial release.++  * extracted from gtvm-hs

+ LICENSE view

@@ -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.

+ README.md view

@@ -0,0 +1,7 @@+# refined-with+Layer on top of Nikita Volkov's+[refined](https://hackage.haskell.org/package/refined) library to allow+annotating data types with refinements, and a flag that indicates whether that+refinement has been "applied".++See the Hackage documentation for details.

+ Setup.hs view

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

+ refined-with.cabal view

@@ -0,0 +1,74 @@+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:           refined-with+version:        0.1.0+synopsis:       Refinement types with an "refinement applied" switch.+description:    Please see README.md.+category:       Data+homepage:       https://github.com/raehik/refined-with#readme+bug-reports:    https://github.com/raehik/refined-with/issues+author:         Ben Orchard+maintainer:     Ben Orchard <thefirstmuffinman@gmail.com>+license:        MIT+license-file:   LICENSE+build-type:     Simple+tested-with:+    GHC ==8.10.7 || ==9.2.2+extra-source-files:+    README.md+    CHANGELOG.md++source-repository head+  type: git+  location: https://github.com/raehik/refined-with++library+  exposed-modules:+      Refined.WithRefine+  other-modules:+      Paths_refined_with+  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+  build-depends:+      aeson ==2.0.*+    , base >=4.14 && <5+    , deepseq ==1.4.*+    , hashable ==1.4.*+    , refined >=0.6.3 && <0.7+  default-language: Haskell2010

+ src/Refined/WithRefine.hs view

@@ -0,0 +1,176 @@+{-|+A wrapper on top of "Refined" that encourages using the same type for refined+and unrefined views of the same data. Useful when both views have identical+structure (i.e. the only difference is that whether some invariants are+enforced). For information on refinement types and the underlying concept, see+"Refined".++Say you're already sold on refinement types as a method to easily describe data+more precisely without complicating algorithms or comprising runtime+performance. You work with plain types internally, and refine only when you need+to. This means when working with records with refined types, you necessarily+duplicate the record: one for refined, one for unrefined.++Sometimes this is fine, because you change the data structure between refining+(e.g. you drop some indices that are generatable). Sometimes, it means you have+two records storing the same data, where one has some invariants enforced and+the other doesn't. In the former case, you should have one data type with+'Refined' fields, one without. This module focuses on the latter use case.++The 'WithRefine' newtype enables you to use the same type for both views by+wrapping refined types with a type-level switch that tracks whether the+predicate is currently enforced.++  * The type @t'WithRefine' ''Enforced' p a@ corresponds to @'Refined' p a@: a+    value of type @a@ with an enforced predicate @p@. Also available at+    @'Strong' p a@.+  * The type @t'WithRefine' ''Unenforced' p a@ corresponds to... @a@. It's a+    value of type @a@ tagged with predicate @p@, but the predicate remains+    unenforced. Also available at @'Weak' p a@.++Now internally, you write your code to only transform @'Weak' p a@ values. When,+say, serializing between an external system, you 'enforce' the predicate,+upgrading to a @'Strong' p a@. The upshot compared to plain refined:++  * No need to duplicate types when working with refined types.+  * Your internal code must be aware of your refined types. This can be good and+    bad: more wrapping, but also more type information.++Runtime impact should be the same as refined, pretty much nothing.+-}++module Refined.WithRefine+  (+  -- * 'WithRefine' types+    WithRefine, unWithRefine+  , withRefine+  , PredicateStatus(..)+  , Strong, Weak++  -- * Enforcing+  , enforce+  , enforceFail++  -- * Unenforcing+  , unenforce++  -- * Coercing between Refined+  , enforcedToRefined+  , refinedToEnforced++  -- * Unsafe enforcing+  , reallyUnsafeEnforce++  -- * Other definitions+  , WithRefineRep+  ) where++import Refined+import Refined.Unsafe+import Data.Proxy+import Control.DeepSeq ( NFData )+import Data.Hashable ( Hashable )+import GHC.Generics ( Generic )+import Data.Aeson+import Control.Exception++-- | A wrapper over a type @a@ with a predicate @p@, and a type-level "switch"+--   indicating whether the predicate is enforced or not.+--+-- @t'WithRefine' ''Enforced' p a@ is equivalent to 'Refined p a', while+-- @t'WithRefine' ''Unenforced' p a@ is equivalent to @a@. This newtype lets you+-- use the same term-level constructor for both. One could then combine multiple+-- t'WithRefine'-wrapped fields into a single record and parameterize over the+-- predicate status to essentially enable "weak" and "strong" views of the+-- record, while conveniently using the same value-level representation.+newtype WithRefine (ps :: PredicateStatus) p a+  = WithRefine {+      -- | Extracts any predicate-wrapped value. Works regardless of whether the+      --   predicate was enforced or not.+      unWithRefine :: a+  } deriving       (Hashable, NFData, Eq, Ord) via a+    deriving stock (Generic, Show, Foldable)++deriving stock instance Functor     (WithRefine 'Unenforced p)+deriving stock instance Traversable (WithRefine 'Unenforced p)++instance ToJSON   a => ToJSON   (WithRefine ps          p a) where+    toJSON     = toJSON     . unWithRefine+    toEncoding = toEncoding . unWithRefine++-- | Use the underlying type's instance.+instance FromJSON a => FromJSON (WithRefine 'Unenforced p a) where+    parseJSON = fmap withRefine . parseJSON++-- | Use the unenforced type's instance, and wrap the enforcing error into+--   Aeson's 'MonadFail'.+instance (FromJSON a, Predicate p a) => FromJSON (WithRefine 'Enforced p a) where+    parseJSON a = parseJSON a >>= enforceFail++-- | I don't really understand this. I naively use the same role annotation as+--   'Refined'. GHC user's guide page:+--   https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/roles.html+type role WithRefine nominal nominal nominal++-- | Wrap a value with any unenforced predicate. This is like tagging your value+--   with the note "this value needs to be checked using the given predicate".+withRefine :: a -> WithRefine 'Unenforced p a+withRefine = WithRefine++-- | Is the associated predicate currently enforced or not?+data PredicateStatus+  = Enforced   -- ^ value is read-only+  | Unenforced -- ^ value is read-write++-- | Synonym for a wrapped type with an enforced predicate.+type Strong p a = WithRefine 'Enforced   p a++-- | Synonym for a wrapped type with an unenforced predicate.+type Weak   p a = WithRefine 'Unenforced p a++-- | Enforce a wrapped value's predicate at runtime.+enforce+    :: forall p a. Predicate p a+    => WithRefine 'Unenforced p a+    -> Either RefineException (WithRefine 'Enforced p a)+enforce wrua =+    maybe (Right (WithRefine a)) Left (validate (Proxy @p) a)+  where a = unWithRefine wrua++-- | Enforce a wrapped value's predicate at runtime, calling 'fail' if the value+--   does not satisfy the predicate.+enforceFail+    :: (Predicate p a, MonadFail m)+    => WithRefine 'Unenforced p a+    -> m (WithRefine 'Enforced p a)+enforceFail wrua = case enforce wrua of+                    Left  e    -> fail $ displayException e+                    Right wrea -> pure wrea++-- | Stop enforcing a wrapped value's predicate.+unenforce :: WithRefine 'Enforced p a -> WithRefine 'Unenforced p a+unenforce = withRefine . unWithRefine++-- | If you have a @t'WithRefine' ''Enforced'@ value, you can obtain a matching+--   'Refined'.+enforcedToRefined :: WithRefine 'Enforced p a -> Refined p a+enforcedToRefined = reallyUnsafeRefine . unWithRefine++-- | If you have a 'Refined' value, you can obtain a matching @t'WithRefine'+--   ''Enforced'@.+refinedToEnforced :: Refined p a -> WithRefine 'Enforced p a+refinedToEnforced = reallyUnsafeEnforce . unrefine++-- | Construct an enforced type, completely ignoring any refinements!+--+-- You should only use this if you can prove that the refinement holds. (We need+-- it internally to coerce between 'Refined'.)+reallyUnsafeEnforce :: a -> WithRefine 'Enforced p a+reallyUnsafeEnforce = WithRefine++-- | Not very useful, but clarifies the meaning of enforced and unenforced+--   refinements.+type WithRefineRep :: forall p a r. PredicateStatus -> p -> a -> r+type family WithRefineRep ps p a where+    WithRefineRep 'Enforced   p a = Refined p a+    WithRefineRep 'Unenforced _ a = a