refined
Refinement types with static and runtime checking
https://github.com/nikita-volkov/refined
LTS Haskell 23.1: | 0.8.2 |
Stackage Nightly 2024-12-21: | 0.8.2 |
Latest on Hackage: | 0.8.2 |
MIT licensed by Nikita Volkov
Maintained by chessai
This version can be pinned in stack with:
refined-0.8.2@sha256:dbd995788d9be0c045764d1fb2137c5e64b56a1721c785c0bb2018fdc84f2ad3,2365
Module documentation for 0.8.2
Depends on 11 packages(full list with versions):
Used by 3 packages in nightly-2024-12-21(full list with versions):
refined
In type theory, a refinement type is a type endowed with a predicate which is assumed to hold for any element of the refined type.
This library allows one to capture the idea of a refinement type
using the Refined
type. A Refined
p
x
wraps a value
of type x
, ensuring that it satisfies a type-level predicate p
.
A simple introduction to this library can be found here: http://nikita-volkov.github.io/refined/
Changes
Changelog
All notable changes to this project will be documented in this file.
The format is based on Keep a Changelog and this project adheres to the Haskell Package Versioning Policy.
[0.8.1] - 2023-04-05
Added
Weaken
instances forSizeGreaterThan
,SizeLessThan
.weakenAndLeft
,weakenAndRight
,weakenOrLeft
,weakenOrRight
type inference helper functions.
Changed
- bump
base
: “< 4.18” -> “< 4.19” - bump
mtl
: “< 2.3” -> “< 2.4” - bump
template-haskell
: “< 2.20” -> “< 2.21”
[0.8] - 2022-10-09
Changed
- on GHC >=9, make
refineTH
andrefineTH_
work in any monad(Quote m, MonadFail m)
. - bump
base
: “< 4.17” -> “< 4.18” - bump
template-haskell
: “< 2.19” -> “< 2.20” - bump
aeson
: “< 2.1” -> “< 2.2”
[0.7] - 2022-07-01
Changed
- make
Refined
predicate typep
kind polymorphic (p :: Type
->p :: k
)
[0.6.3] - 2022-01-14
Added
Hashable
instance forRefined
FromJSONKey
instance forRefined
ToJSONKey
instance forRefined
shrink
forRefined
’sArbitrary
instance.refineEither
function
Changed
- improved efficiency of
strengthen
- bump multiple dependency upper bounds
[0.6.2] - 2021-01-31
Changed
strengthen
no longer returns anEither
, since the proof that it should always succeed is in its constraints.- correct
success
documentation
[0.6.1] - 2020-08-02
Changed
- upper bound on QuickCheck: <2.14 -> <2.15
[0.6] - 2020-07-21
Changed
validate
now takes aProxy
as its first argument.- All uses of prettyprinter are now just
Text
Removed
- Refined.These module
- Dependency on
prettyprinter
Fixed
- bug in
sized
internal helper that caused formatting issues in sized predicate errors
[0.5.1] - 2020-07-14
Changed
refineTH_
is now implemented in terms ofrefineTH
- Fix pretty-printing of
RefineException
s during compile-time
[0.5] - 2020-07-11
Added
- sized Predicate instances for
Text
- sized Predicate instances for strict and lazy
ByteString
- INLINABLE pragmas on
refine_
reifyPredicate
NFData
instance forRefined
- RefineSomeException constructor. Enables recovering specific validation exceptions. Thanks to @haroldcarr for adding this.
- RefineXorException constructor.
Empty
andNotEmpty
predicates.NaN
andInfinite
predicates for floating-point numbers.- @since pragmas to EVERYTHING.
Changed
- lower bound on mtl to 2.2.2 due to use of liftEither. Thanks to @k0ral for reporting this
- Generalize sized predicates
- Allow newer template-haskell (< 0.16 ==> < 0.17)
- Allow newer aeson (< 1.5 ==> < 1.6) Thanks to @locallycompact for this change.
Removed
Refined.Internal
module Thanks to @nikita-volkov for pushing me to do this.- Orphan modules Thanks to @symbiont-sam-halliday for pointing out the silliness of these modules.
RefineT
. It was a needless abstraction that just made the library harder to learn and use, providing little benefit overMaybe RefineException
. Thanks to @nikita-volkov for helping me see the light.
Deprecated
- Refined.These module in favour of Data.These from these-skinny
[0.4.4] - 2019-10-18
Added
refine_
refineTH_
- test suite: unit tests for compiling.
Changed
- Allow newer
template-haskell
andQuickCheck
.
[0.4.2.3] - 2019-09-17
Added
reifyPredicate
Fixed
Arbitrary
instance forRefined
should now always terminate. Thanks to @symbiont-joseph-kachmar for reporting this.
[0.4.2.2] - 2019-07-19
Added
exceptRefine
,strengthen
, andstrengthenM
[0.4.2.1] - 2019-05-31
Fixed
- Documentation fix for
DivisibleBy
Changed
- Re-export
DivisibleBy
,Even
, andOdd
from moduleRefined
. - Re-export all constructors from module
Refined
.
[0.4.2] - 2019-05-30
Removed
- Re-removed dependency of
these
package.
Added
Even
,Odd
, andDivisibleBy
predicates.- doctests for all predicates.
Changed
- Make all predicates unary data constructors, instead of nullary, and export those newly added constructors.
[0.4.1] - 2019-04-15
Fixed
- Serious regression where
Not p
~p
. Thanks to @k0ral who reported this.
[0.4] - 2019-03-18
Added
- ‘NegativeFromTo’, a Predicate that ensures a numeric value is within a range [a,b], where a < 0 and b >= a. Thanks to github.com/futtetennista for this change.
Changed
RefinedNotException
now has a child (it should have had one in v2. This was an oversight.)displayRefineException
no longer uses tabs, instead 2 spaces.- make implementation of
displayRefineException
more clear via formatting.
[0.3.0.0] - 2018-09-26
Added
- Internal module, and Unsafe modules, making sure to take care w.r.t. the scope of coercions related to the use of the ‘Refined’ constructor.
- ‘IdPred’ predicate, predicate that never fails.
- Generic instances for all predicates.
reallyUnsafeRefine
,reallyUnsafeUnderlyingRefined
,reallyUnsafeAllUnderlyingRefined
, functions that allow one to use ‘Coercion’s to manually prove things about ‘Refined’ values.
Changed
- Type role of Refined from ‘phantom Representational’ to ‘nominal nominal’.
With the old type role, one can use
coerce
to proveQ x
given anyP x
. The second parameter should also be nominal because of interactions with something likeGreaterThan
andData.Ord.Down
. Thanks to David Feuer for pointing this out. - Change docs to point users to ‘Refined.Unsafe’ module instead of recommending ‘Unsafe.Coerce.unsafeCoerce’.
- ‘Ascending’ and ‘Descending’ predicates now use ‘Foldable’ instead of ‘IsList’.
- Lowered the lower bound on ‘exceptions’; it was too strict for the support window.
Removed
- Dependency of the ‘these’ package. It brings in some very
heavy transitive dependencies, even though the datatype
in
refined
is used to the most minimal extent. This is a breaking change because this change is exposed to the end user via ‘RefineAndException’. It is exported from a module called ‘Refined.These’. Users wishing to interact with such exceptions can either just use the datatype constituting a minimal API there, or depend on the ‘these’ package.
[0.2.3.0] - 2018-06-01
Added
- back in the ‘Foldable’ instance for ‘Refined’. It is safe.
[0.2.2.0] - 2018-05-31
Removed
- Unsafe typeclass instances that could break the ‘Refined’ invariant. These should not have been added.
[0.2.1.0] - 2018-05-31
Removed
- Unsafe typeclass instances that could break the ‘Refined’ invariant. These should not have been added.
[0.2.0.0] - 2018-05-30
Changed
- Radical rewrite of the library, centred around ‘RefineException’ and the ‘RefineT’ monad transformer. ‘validate’ now has the type signature validate :: (Predicate p x, Monad m) => p -> x -> RefineT m ()
Added
- More predicates