Refined.Unsafe

This module exposes unsafe refinements. An unsafe refinement is one which either does not make the guarantee of totality in construction of the Refined value or does not perform a check of the refinement predicate. It is recommended only to use this when you can manually prove that the refinement predicate holds.

Refined

data Refined p x

A refinement type, which wraps a value of type x, ensuring that it satisfies a type-level predicate p.

Instances

Foldable (Refined p)

Defined in Refined.Internal

Methods

fold :: Monoid m => Refined p m -> m

foldMap :: Monoid m => (a -> m) -> Refined p a -> m

foldr :: (a -> b -> b) -> b -> Refined p a -> b

foldr' :: (a -> b -> b) -> b -> Refined p a -> b

foldl :: (b -> a -> b) -> b -> Refined p a -> b

foldl' :: (b -> a -> b) -> b -> Refined p a -> b

foldr1 :: (a -> a -> a) -> Refined p a -> a

foldl1 :: (a -> a -> a) -> Refined p a -> a

toList :: Refined p a -> [a]

null :: Refined p a -> Bool

length :: Refined p a -> Int

elem :: Eq a => a -> Refined p a -> Bool

maximum :: Ord a => Refined p a -> a

minimum :: Ord a => Refined p a -> a

sum :: Num a => Refined p a -> a

product :: Num a => Refined p a -> a

Eq x => Eq (Refined p x)

Defined in Refined.Internal

Methods

(==) :: Refined p x -> Refined p x -> Bool

(/=) :: Refined p x -> Refined p x -> Bool

Ord x => Ord (Refined p x)

Defined in Refined.Internal

Methods

compare :: Refined p x -> Refined p x -> Ordering

(<) :: Refined p x -> Refined p x -> Bool

(<=) :: Refined p x -> Refined p x -> Bool

(>) :: Refined p x -> Refined p x -> Bool

(>=) :: Refined p x -> Refined p x -> Bool

max :: Refined p x -> Refined p x -> Refined p x

min :: Refined p x -> Refined p x -> Refined p x

(Read x, Predicate p x) => Read (Refined p x)

This instance makes sure to check the refinement.

Defined in Refined.Internal

Methods

readsPrec :: Int -> ReadS (Refined p x)

readList :: ReadS [Refined p x]

readPrec :: ReadPrec (Refined p x)

readListPrec :: ReadPrec [Refined p x]

Show x => Show (Refined p x)

Defined in Refined.Internal

Methods

showsPrec :: Int -> Refined p x -> ShowS

show :: Refined p x -> String

showList :: [Refined p x] -> ShowS

Lift x => Lift (Refined p x)

Defined in Refined.Internal

Methods

lift :: Refined p x -> Q Exp

(Arbitrary a, Typeable a, Typeable p, Predicate p a) => Arbitrary (Refined p a)

Defined in Refined.Orphan.QuickCheck

Methods

arbitrary :: Gen (Refined p a)

shrink :: Refined p a -> [Refined p a]

(ToJSON a, Predicate p a) => ToJSON (Refined p a)

Defined in Refined.Orphan.Aeson

Methods

toJSON :: Refined p a -> Value

toEncoding :: Refined p a -> Encoding

toJSONList :: [Refined p a] -> Value

toEncodingList :: [Refined p a] -> Encoding

(FromJSON a, Predicate p a) => FromJSON (Refined p a)

Defined in Refined.Orphan.Aeson

Methods

parseJSON :: Value -> Parser (Refined p a)

parseJSONList :: Value -> Parser [Refined p a]

Creation

reallyUnsafeRefine :: x -> Refined p x

Constructs a Refined value, completely ignoring any refinements! Use this only when you can manually prove that the refinement holds.

unsafeRefine :: Predicate p x => x -> Refined p x

Constructs a Refined value at run-time, calling error if the value does not satisfy the predicate.

WARNING: this function is not total!

Coercion

reallyUnsafeUnderlyingRefined :: Coercion x (Refined p x)

A coercion between a type and any refinement of that type. See Data.Type.Coercion for functions manipulating coercions.

reallyUnsafeAllUnderlyingRefined :: ((forall x y p. Coercible x y => Coercible y (Refined p x)) => r) -> r

Reveal that x and Refined p x are Coercible for all x and p simultaneously.

Example

reallyUnsafePredEquiv :: Coercion (Refined p x) (Refined q x)
reallyUnsafePredEquiv = reallyUnsafeAllUnderlyingRefined Coercion

reallyUnsafePredEquiv :: Coercion (Refined p x) (Refined q x)

A coercion between two Refined types, magicking up the claim that one predicate is entirely equivalent to another.