# refined

Refinement types with static and runtime checking

https://github.com/nikita-volkov/refined

Version on this page: | 0.8.1 |

LTS Haskell 22.23: | 0.8.2 |

Stackage Nightly 2024-05-26: | 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.1@sha256:68bde689caa49d5e45886e01ccefb581372a86f2b1bf9a61fd4d45657f2ab69f,2999`

#### Module documentation for 0.8.1

Depends on 11 packages

*(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 for`SizeGreaterThan`

,`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`

and`refineTH_`

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 type`p`

kind polymorphic (`p :: Type`

->`p :: k`

)

## [0.6.3] - 2022-01-14

### Added

`Hashable`

instance for`Refined`

`FromJSONKey`

instance for`Refined`

`ToJSONKey`

instance for`Refined`

`shrink`

for`Refined`

’s`Arbitrary`

instance.`refineEither`

function

### Changed

- improved efficiency of
`strengthen`

- bump multiple dependency upper bounds

## [0.6.2] - 2021-01-31

### Changed

`strengthen`

no longer returns an`Either`

, 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 a`Proxy`

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 of`refineTH`

- 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 for`Refined`

- RefineSomeException constructor. Enables recovering specific validation exceptions. Thanks to @haroldcarr for adding this.
- RefineXorException constructor.
`Empty`

and`NotEmpty`

predicates.`NaN`

and`Infinite`

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 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-haskell`

and`QuickCheck`

.

## [0.4.2.3] - 2019-09-17

### Added

`reifyPredicate`

### Fixed

`Arbitrary`

instance for`Refined`

should 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`

, and`Odd`

from module`Refined`

. - Re-export all constructors from module
`Refined`

.

## [0.4.2] - 2019-05-30

### Removed

- Re-removed dependency of
`these`

package.

### Added

`Even`

,`Odd`

, and`DivisibleBy`

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 prove`Q x`

given any`P x`

. The second parameter should also be nominal because of interactions with something like`GreaterThan`

and`Data.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