Refined Extras

Description

refined-extras provides extra functionality for the refined package. This functionality can be broken into several categories.

Polymorphism

Allows us to write functions that are polymorphic in the predicate constraints they require, e.g.,

safeDiv :: Implies p NonZero => Int -> Refined p Int -> Int

Predicates

Predefined predicates.

Unsafe

Unsafe functions for when we know something holds but cannot prove it to the type system, e.g.,

let m = $$(refineTH 7) :: Refined Positive Int
    n = $$(refineTH 8) :: Refined Positive Int
 in unsafeLiftR2 (+) m n -- Refined Positive Int

Utils

Various convenience utilities.

The entrypoint is Refined.Extras, which reexports everything.