Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Refined.WithRefine
Description
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
corresponds toWithRefine
'Enforced
p a
: a value of typeRefined
p aa
with an enforced predicatep
. Also available at
.Strong
p a - The type
corresponds to...WithRefine
'Unenforced
p aa
. It's a value of typea
tagged with predicatep
, but the predicate remains unenforced. Also available at
.Weak
p a
Now internally, you write your code to only transform
values. When,
say, serializing between an external system, you Weak
p aenforce
the predicate,
upgrading to a
. The upshot compared to plain refined:Strong
p a
- 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.
Synopsis
- data WithRefine (ps :: PredicateStatus) p a
- withRefine :: forall p a. a -> WithRefine 'Unenforced p a
- withoutRefine :: WithRefine ps p a -> a
- data PredicateStatus
- type Strong p a = WithRefine 'Enforced p a
- type Weak p a = WithRefine 'Unenforced p a
- enforce :: forall p a. Predicate p a => WithRefine 'Unenforced p a -> Either RefineException (WithRefine 'Enforced p a)
- enforceFail :: forall p m a. (Predicate p a, MonadFail m) => WithRefine 'Unenforced p a -> m (WithRefine 'Enforced p a)
- unenforce :: forall p a. WithRefine 'Enforced p a -> WithRefine 'Unenforced p a
- enforcedToRefined :: forall p a. WithRefine 'Enforced p a -> Refined p a
- refinedToEnforced :: forall p a. Refined p a -> WithRefine 'Enforced p a
- reallyUnsafeEnforce :: forall p a. a -> WithRefine 'Enforced p a
- unsafeWithRefine :: forall ps p a. a -> WithRefine ps p a
- type family WithRefineRep ps p a where ...
WithRefine
types
data WithRefine (ps :: PredicateStatus) p a Source #
A wrapper over a type a
with a predicate p
, and a type-level "switch"
indicating whether the predicate is enforced or not.
is equivalent to 'Refined p a', while
WithRefine
'Enforced
p a
is equivalent to WithRefine
'Unenforced
p aa
. 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
withRefine :: forall p a. a -> WithRefine 'Unenforced p a Source #
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 Source #
Strips the predicate from a any wrapped value (enforced or not).
data PredicateStatus Source #
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 Source #
Synonym for a wrapped type with an enforced predicate.
type Weak p a = WithRefine 'Unenforced p a Source #
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) Source #
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) Source #
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 Source #
Stop enforcing a wrapped value's predicate.
Coercing between Refined
enforcedToRefined :: forall p a. WithRefine 'Enforced p a -> Refined p a Source #
If you have a
value, you can obtain a matching
WithRefine
'Enforced
Refined
.
refinedToEnforced :: forall p a. Refined p a -> WithRefine 'Enforced p a Source #
If you have a Refined
value, you can obtain a matching
.WithRefine
'Enforced
Unsafe enforcing
reallyUnsafeEnforce :: forall p a. a -> WithRefine 'Enforced p a Source #
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 Source #
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 ... Source #
Not very useful, but clarifies the meaning of enforced and unenforced refinements.
Equations
WithRefineRep 'Enforced p a = Refined p a | |
WithRefineRep 'Unenforced _ a = a |