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 :: k) x

A refinement type, which wraps a value of type x.

Since: 0.1.0.0

Instances

Lift x => Lift (Refined p x :: Type)

Since: 0.1.0.0

Defined in Refined.Unsafe.Type

Methods

lift :: Refined p x -> Q Exp

liftTyped :: Refined p x -> Q (TExp (Refined p x))

Foldable (Refined p)

Since: 0.2

Defined in Refined.Unsafe.Type

Methods

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

foldMap :: Monoid m => (a -> m) -> Refined p a -> 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)

Since: 0.1.0.0

Defined in Refined.Unsafe.Type

Methods

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

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

Ord x => Ord (Refined p x)

Since: 0.1.0.0

Defined in Refined.Unsafe.Type

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.

Since: 0.1.0.0

Defined in Refined

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)

Since: 0.1.0.0

Defined in Refined.Unsafe.Type

Methods

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

show :: Refined p x -> String

showList :: [Refined p x] -> ShowS

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

Since: 0.4

Defined in Refined

Methods

arbitrary :: Gen (Refined p a)

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

Hashable x => Hashable (Refined p x)

Since: 0.6.3

Defined in Refined.Unsafe.Type

Methods

hashWithSalt :: Int -> Refined p x -> Int

hash :: Refined p x -> Int

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

Since: 0.4

Defined in Refined

Methods

toJSON :: Refined p a -> Value

toEncoding :: Refined p a -> Encoding

toJSONList :: [Refined p a] -> Value

toEncodingList :: [Refined p a] -> Encoding

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

Since: 0.6.3

Defined in Refined

Methods

toJSONKey :: ToJSONKeyFunction (Refined p a)

toJSONKeyList :: ToJSONKeyFunction [Refined p a]

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

Since: 0.4

Defined in Refined

Methods

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

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

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

Defined in Refined

Methods

fromJSONKey :: FromJSONKeyFunction (Refined p a)

fromJSONKeyList :: FromJSONKeyFunction [Refined p a]

NFData x => NFData (Refined p x)

Since: 0.5

Defined in Refined.Unsafe.Type

Methods

rnf :: Refined p x -> ()

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.

Since: 0.3.0.0

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!

Since: 0.2.0.0

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.

Since: 0.3.0.0

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

Since: 0.3.0.0

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.

Since: 0.3.0.0