refined
Refinement types with static and runtime checking
https://github.com/nikita-volkov/refined
| LTS Haskell 24.17: | 0.8.2 | 
| Stackage Nightly 2025-10-31: | 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,2365Module documentation for 0.8.2
Depends on 11 packages(full list with versions):
Used by 5 packages in nightly-2025-10-31(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
- Weakeninstances for- SizeGreaterThan,- SizeLessThan.
- weakenAndLeft,- weakenAndRight,- weakenOrLeft,- weakenOrRighttype 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 refineTHandrefineTH_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 Refinedpredicate typepkind polymorphic (p :: Type->p :: k)
[0.6.3] - 2022-01-14
Added
- Hashableinstance for- Refined
- FromJSONKeyinstance for- Refined
- ToJSONKeyinstance for- Refined
- shrinkfor- Refined’s- Arbitraryinstance.
- refineEitherfunction
Changed
- improved efficiency of strengthen
- bump multiple dependency upper bounds
[0.6.2] - 2021-01-31
Changed
- strengthenno longer returns an- Either, since the proof that it should always succeed is in its constraints.
- correct successdocumentation
[0.6.1] - 2020-08-02
Changed
- upper bound on QuickCheck: <2.14 -> <2.15
[0.6] - 2020-07-21
Changed
- validatenow takes a- Proxyas its first argument.
- All uses of prettyprinter are now just Text
Removed
- Refined.These module
- Dependency on prettyprinter
Fixed
- bug in sizedinternal helper that caused formatting issues in sized predicate errors
[0.5.1] - 2020-07-14
Changed
- refineTH_is now implemented in terms of- refineTH
- Fix pretty-printing of RefineExceptions 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
- NFDatainstance for- Refined
- RefineSomeException constructor. Enables recovering specific validation exceptions. Thanks to @haroldcarr for adding this.
- RefineXorException constructor.
- Emptyand- NotEmptypredicates.
- NaNand- Infinitepredicates 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.Internalmodule 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 over- Maybe 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-haskellandQuickCheck.
[0.4.2.3] - 2019-09-17
Added
- reifyPredicate
Fixed
- Arbitraryinstance for- Refinedshould now always terminate. Thanks to @symbiont-joseph-kachmar for reporting this.
[0.4.2.2] - 2019-07-19
Added
- exceptRefine,- strengthen, and- strengthenM
[0.4.2.1] - 2019-05-31
Fixed
- Documentation fix for DivisibleBy
Changed
- Re-export DivisibleBy,Even, andOddfrom moduleRefined.
- Re-export all constructors from module Refined.
[0.4.2] - 2019-05-30
Removed
- Re-removed dependency of thesepackage.
Added
- Even,- Odd, and- DivisibleBypredicates.
- 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
- RefinedNotExceptionnow has a child (it should have had one in v2. This was an oversight.)
- displayRefineExceptionno longer uses tabs, instead 2 spaces.
- make implementation of displayRefineExceptionmore 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 coerceto proveQ xgiven anyP x. The second parameter should also be nominal because of interactions with something likeGreaterThanandData.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 refinedis 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
