refined-0.7: Refinement types with static and runtime checking
Safe HaskellNone
LanguageHaskell2010

Refined.Unsafe

Description

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.

Synopsis

Refined

data Refined (p :: k) x Source #

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

Since: 0.1.0.0

Instances

Instances details
Lift x => Lift (Refined p x :: Type) Source #

Since: 0.1.0.0

Instance details

Defined in Refined.Unsafe.Type

Methods

lift :: Refined p x -> Q Exp #

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

Foldable (Refined p) Source #

Since: 0.2

Instance details

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) Source #

Since: 0.1.0.0

Instance details

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) Source #

Since: 0.1.0.0

Instance details

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) Source #

This instance makes sure to check the refinement.

Since: 0.1.0.0

Instance details

Defined in Refined

Show x => Show (Refined p x) Source #

Since: 0.1.0.0

Instance details

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) Source #

Since: 0.4

Instance details

Defined in Refined

Methods

arbitrary :: Gen (Refined p a) #

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

Hashable x => Hashable (Refined p x) Source #

Since: 0.6.3

Instance details

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) Source #

Since: 0.4

Instance details

Defined in Refined

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

Since: 0.6.3

Instance details

Defined in Refined

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

Since: 0.4

Instance details

Defined in Refined

(FromJSONKey a, Predicate p a) => FromJSONKey (Refined p a) Source # 
Instance details

Defined in Refined

NFData x => NFData (Refined p x) Source #

Since: 0.5

Instance details

Defined in Refined.Unsafe.Type

Methods

rnf :: Refined p x -> () #

Creation

reallyUnsafeRefine :: x -> Refined p x Source #

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 Source #

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) Source #

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 Source #

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) Source #

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

Since: 0.3.0.0