diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,4 @@ +## 0.1.0 (2022-04-22) +Initial release. + + * extracted from gtvm-hs diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,20 @@ +Copyright (c) 2022 Ben Orchard (@raehik) + +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. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/refined-with.cabal b/refined-with.cabal new file mode 100644 --- /dev/null +++ b/refined-with.cabal @@ -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 +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 diff --git a/src/Refined/WithRefine.hs b/src/Refined/WithRefine.hs new file mode 100644 --- /dev/null +++ b/src/Refined/WithRefine.hs @@ -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