Refined.WithRefine

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.

Definitions generally order typevars predicate first and a last, to support visible type application (a is usually obvious to the compiler).

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

WithRefine types

data WithRefine (ps :: PredicateStatus) p a

A wrapper over a type a with a predicate p, and a type-level "switch" indicating whether the predicate is enforced or not.

WithRefine 'Enforced p a is equivalent to 'Refined p a', while 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 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.

Instances

Foldable (WithRefine ps p)

Defined in Refined.WithRefine

Methods

fold :: Monoid m => WithRefine ps p m -> m

foldMap :: Monoid m => (a -> m) -> WithRefine ps p a -> m

foldMap' :: Monoid m => (a -> m) -> WithRefine ps p a -> m

foldr :: (a -> b -> b) -> b -> WithRefine ps p a -> b

foldr' :: (a -> b -> b) -> b -> WithRefine ps p a -> b

foldl :: (b -> a -> b) -> b -> WithRefine ps p a -> b

foldl' :: (b -> a -> b) -> b -> WithRefine ps p a -> b

foldr1 :: (a -> a -> a) -> WithRefine ps p a -> a

foldl1 :: (a -> a -> a) -> WithRefine ps p a -> a

toList :: WithRefine ps p a -> [a]

null :: WithRefine ps p a -> Bool

length :: WithRefine ps p a -> Int

elem :: Eq a => a -> WithRefine ps p a -> Bool

maximum :: Ord a => WithRefine ps p a -> a

minimum :: Ord a => WithRefine ps p a -> a

sum :: Num a => WithRefine ps p a -> a

product :: Num a => WithRefine ps p a -> a

Traversable (WithRefine 'Unenforced p)

Defined in Refined.WithRefine

Methods

traverse :: Applicative f => (a -> f b) -> WithRefine 'Unenforced p a -> f (WithRefine 'Unenforced p b)

sequenceA :: Applicative f => WithRefine 'Unenforced p (f a) -> f (WithRefine 'Unenforced p a)

mapM :: Monad m => (a -> m b) -> WithRefine 'Unenforced p a -> m (WithRefine 'Unenforced p b)

sequence :: Monad m => WithRefine 'Unenforced p (m a) -> m (WithRefine 'Unenforced p a)

Functor (WithRefine 'Unenforced p)

Defined in Refined.WithRefine

Methods

fmap :: (a -> b) -> WithRefine 'Unenforced p a -> WithRefine 'Unenforced p b

(<$) :: a -> WithRefine 'Unenforced p b -> WithRefine 'Unenforced p a

(FromJSON a, Predicate p a) => FromJSON (WithRefine 'Enforced p a)

Use the unenforced type's instance, and wrap the enforcing error into Aeson's MonadFail.

Defined in Refined.WithRefine

Methods

parseJSON :: Value -> Parser (WithRefine 'Enforced p a)

parseJSONList :: Value -> Parser [WithRefine 'Enforced p a]

FromJSON a => FromJSON (WithRefine 'Unenforced p a)

Use the underlying type's instance.

Defined in Refined.WithRefine

Methods

parseJSON :: Value -> Parser (WithRefine 'Unenforced p a)

parseJSONList :: Value -> Parser [WithRefine 'Unenforced p a]

ToJSON a => ToJSON (WithRefine ps p a)

Defined in Refined.WithRefine

Methods

toJSON :: WithRefine ps p a -> Value

toEncoding :: WithRefine ps p a -> Encoding

toJSONList :: [WithRefine ps p a] -> Value

toEncodingList :: [WithRefine ps p a] -> Encoding

Generic (WithRefine ps p a)

Defined in Refined.WithRefine

Associated Types

type Rep (WithRefine ps p a) :: Type -> Type

Methods

from :: WithRefine ps p a -> Rep (WithRefine ps p a) x

to :: Rep (WithRefine ps p a) x -> WithRefine ps p a

Show a => Show (WithRefine ps p a)

Defined in Refined.WithRefine

Methods

showsPrec :: Int -> WithRefine ps p a -> ShowS

show :: WithRefine ps p a -> String

showList :: [WithRefine ps p a] -> ShowS

NFData a => NFData (WithRefine ps p a)

Defined in Refined.WithRefine

Methods

rnf :: WithRefine ps p a -> ()

Eq a => Eq (WithRefine ps p a)

Defined in Refined.WithRefine

Methods

(==) :: WithRefine ps p a -> WithRefine ps p a -> Bool

(/=) :: WithRefine ps p a -> WithRefine ps p a -> Bool

Ord a => Ord (WithRefine ps p a)

Defined in Refined.WithRefine

Methods

compare :: WithRefine ps p a -> WithRefine ps p a -> Ordering

(<) :: WithRefine ps p a -> WithRefine ps p a -> Bool

(<=) :: WithRefine ps p a -> WithRefine ps p a -> Bool

(>) :: WithRefine ps p a -> WithRefine ps p a -> Bool

(>=) :: WithRefine ps p a -> WithRefine ps p a -> Bool

max :: WithRefine ps p a -> WithRefine ps p a -> WithRefine ps p a

min :: WithRefine ps p a -> WithRefine ps p a -> WithRefine ps p a

Hashable a => Hashable (WithRefine ps p a)

Defined in Refined.WithRefine

Methods

hashWithSalt :: Int -> WithRefine ps p a -> Int

hash :: WithRefine ps p a -> Int

type Rep (WithRefine ps p a)

Defined in Refined.WithRefine

type Rep (WithRefine ps p a) = D1 ('MetaData "WithRefine" "Refined.WithRefine" "refined-with-0.3.0-inplace" 'True) (C1 ('MetaCons "WithRefine" 'PrefixI 'True) (S1 ('MetaSel ('Just "withoutRefine") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))

withRefine :: forall p a. a -> WithRefine 'Unenforced p a

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

withoutRefine :: WithRefine ps p a -> a

Strips the predicate from a any wrapped value (enforced or not).

data PredicateStatus

Is the associated predicate currently enforced or not?

Constructors

Enforced

value is read-only

Unenforced

value is read-write

type Strong p a = WithRefine 'Enforced p a

Synonym for a wrapped type with an enforced predicate.

type Weak p a = WithRefine 'Unenforced p a

Synonym for a wrapped type with an unenforced predicate.

Enforcing

enforce :: forall p a. Predicate p a => WithRefine 'Unenforced p a -> Either RefineException (WithRefine 'Enforced p a)

Enforce a wrapped value's predicate at runtime.

enforceFail :: forall p m a. (Predicate p a, MonadFail m) => WithRefine 'Unenforced p a -> m (WithRefine 'Enforced p a)

Enforce a wrapped value's predicate at runtime, calling fail if the value does not satisfy the predicate.

Unenforcing

unenforce :: forall p a. WithRefine 'Enforced p a -> WithRefine 'Unenforced p a

Stop enforcing a wrapped value's predicate.

Coercing between Refined

enforcedToRefined :: forall p a. WithRefine 'Enforced p a -> Refined p a

If you have a WithRefine 'Enforced value, you can obtain a matching Refined.

refinedToEnforced :: forall p a. Refined p a -> WithRefine 'Enforced p a

If you have a Refined value, you can obtain a matching WithRefine 'Enforced.

Unsafe enforcing

reallyUnsafeEnforce :: forall p a. a -> WithRefine 'Enforced p a

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

Unsafe creation

unsafeWithRefine :: forall ps p a. a -> WithRefine ps p a

Wrap a value with any predicate, enforced or unenforced. This is useful for "no-op" refinements, potentially letting you to merge two instances into one, where you explicitly ignore the PredicateStatus (perhaps clearer).

You should only use this if you can prove that the refinement holds for all values of a.

Other definitions

type family WithRefineRep ps p a where ...

Not very useful, but clarifies the meaning of enforced and unenforced refinements.

Equations

WithRefineRep 'Enforced p a = Refined p a

WithRefineRep 'Unenforced _ a = a