Safe Haskell	Safe-Inferred
Language	Haskell2010

Refined.Unsafe

Contents

Refined
- Creation
- Coercion

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

data Refined (p :: k) x
data Refined1 (p :: k) f x
reallyUnsafeRefine :: x -> Refined p x
reallyUnsafeRefine1 :: f x -> Refined1 p f x
unsafeRefine :: Predicate p x => x -> Refined p x
reallyUnsafeUnderlyingRefined :: Coercion x (Refined p x)
reallyUnsafeAllUnderlyingRefined :: ((forall x y p. Coercible x y => Coercible y (Refined p x)) => r) -> r
reallyUnsafePredEquiv :: Coercion (Refined p x) (Refined q x)

`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 :: Quote m => Refined p x -> m Exp Source # liftTyped :: forall (m :: Type -> Type). Quote m => Refined p x -> Code m (Refined p x) Source #
Foldable (Refined p) Source #	Since: 0.2
Instance details Defined in Refined.Unsafe.Type Methods fold :: Monoid m => Refined p m -> m Source # foldMap :: Monoid m => (a -> m) -> Refined p a -> m Source # foldMap' :: Monoid m => (a -> m) -> Refined p a -> m Source # foldr :: (a -> b -> b) -> b -> Refined p a -> b Source # foldr' :: (a -> b -> b) -> b -> Refined p a -> b Source # foldl :: (b -> a -> b) -> b -> Refined p a -> b Source # foldl' :: (b -> a -> b) -> b -> Refined p a -> b Source # foldr1 :: (a -> a -> a) -> Refined p a -> a Source # foldl1 :: (a -> a -> a) -> Refined p a -> a Source # toList :: Refined p a -> [a] Source # null :: Refined p a -> Bool Source # length :: Refined p a -> Int Source # elem :: Eq a => a -> Refined p a -> Bool Source # maximum :: Ord a => Refined p a -> a Source # minimum :: Ord a => Refined p a -> a Source # sum :: Num a => Refined p a -> a Source # product :: Num a => Refined p a -> a Source #
(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) Source # shrink :: Refined p a -> [Refined p a] Source #
(FromJSON a, Predicate p a) => FromJSON (Refined p a) Source #	Since: 0.4
Instance details Defined in Refined Methods parseJSON :: Value -> Parser (Refined p a) Source # parseJSONList :: Value -> Parser [Refined p a] Source #
(FromJSONKey a, Predicate p a) => FromJSONKey (Refined p a) Source #
Instance details Defined in Refined Methods fromJSONKey :: FromJSONKeyFunction (Refined p a) Source # fromJSONKeyList :: FromJSONKeyFunction [Refined p a] Source #
(ToJSON a, Predicate p a) => ToJSON (Refined p a) Source #	Since: 0.4
Instance details Defined in Refined Methods toJSON :: Refined p a -> Value Source # toEncoding :: Refined p a -> Encoding Source # toJSONList :: [Refined p a] -> Value Source # toEncodingList :: [Refined p a] -> Encoding Source #
(ToJSONKey a, Predicate p a) => ToJSONKey (Refined p a) Source #	Since: 0.6.3
Instance details Defined in Refined Methods toJSONKey :: ToJSONKeyFunction (Refined p a) Source # toJSONKeyList :: ToJSONKeyFunction [Refined p a] Source #
(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 Methods readsPrec :: Int -> ReadS (Refined p x) Source # readList :: ReadS [Refined p x] Source # readPrec :: ReadPrec (Refined p x) Source # readListPrec :: ReadPrec [Refined p x] Source #
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 Source # show :: Refined p x -> String Source # showList :: [Refined p x] -> ShowS Source #
NFData x => NFData (Refined p x) Source #	Since: 0.5
Instance details Defined in Refined.Unsafe.Type Methods rnf :: Refined p x -> () Source #
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 Source # (/=) :: Refined p x -> Refined p x -> Bool Source #
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 Source # (<) :: Refined p x -> Refined p x -> Bool Source # (<=) :: Refined p x -> Refined p x -> Bool Source # (>) :: Refined p x -> Refined p x -> Bool Source # (>=) :: Refined p x -> Refined p x -> Bool Source # max :: Refined p x -> Refined p x -> Refined p x Source # min :: Refined p x -> Refined p x -> Refined p x Source #
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 Source # hash :: Refined p x -> Int Source #

data Refined1 (p :: k) f x Source #

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

The predicate is applied over the functor f. Thus, we may safely recover various Functory instances, because no matter what you do to the values inside the functor, the predicate may not be invalidated.

Instances

Instances details

Lift (f a) => Lift (Refined1 p f a :: Type) Source #
Instance details Defined in Refined.Unsafe.Type Methods lift :: Quote m => Refined1 p f a -> m Exp Source # liftTyped :: forall (m :: Type -> Type). Quote m => Refined1 p f a -> Code m (Refined1 p f a) Source #
Foldable f => Foldable (Refined1 p f) Source #
Instance details Defined in Refined.Unsafe.Type Methods fold :: Monoid m => Refined1 p f m -> m Source # foldMap :: Monoid m => (a -> m) -> Refined1 p f a -> m Source # foldMap' :: Monoid m => (a -> m) -> Refined1 p f a -> m Source # foldr :: (a -> b -> b) -> b -> Refined1 p f a -> b Source # foldr' :: (a -> b -> b) -> b -> Refined1 p f a -> b Source # foldl :: (b -> a -> b) -> b -> Refined1 p f a -> b Source # foldl' :: (b -> a -> b) -> b -> Refined1 p f a -> b Source # foldr1 :: (a -> a -> a) -> Refined1 p f a -> a Source # foldl1 :: (a -> a -> a) -> Refined1 p f a -> a Source # toList :: Refined1 p f a -> [a] Source # null :: Refined1 p f a -> Bool Source # length :: Refined1 p f a -> Int Source # elem :: Eq a => a -> Refined1 p f a -> Bool Source # maximum :: Ord a => Refined1 p f a -> a Source # minimum :: Ord a => Refined1 p f a -> a Source # sum :: Num a => Refined1 p f a -> a Source # product :: Num a => Refined1 p f a -> a Source #
Traversable f => Traversable (Refined1 p f) Source #
Instance details Defined in Refined.Unsafe.Type Methods traverse :: Applicative f0 => (a -> f0 b) -> Refined1 p f a -> f0 (Refined1 p f b) Source # sequenceA :: Applicative f0 => Refined1 p f (f0 a) -> f0 (Refined1 p f a) Source # mapM :: Monad m => (a -> m b) -> Refined1 p f a -> m (Refined1 p f b) Source # sequence :: Monad m => Refined1 p f (m a) -> m (Refined1 p f a) Source #
Functor f => Functor (Refined1 p f) Source #
Instance details Defined in Refined.Unsafe.Type Methods fmap :: (a -> b) -> Refined1 p f a -> Refined1 p f b Source # (<$) :: a -> Refined1 p f b -> Refined1 p f a Source #
Show (f x) => Show (Refined1 p f x) Source #
Instance details Defined in Refined.Unsafe.Type Methods showsPrec :: Int -> Refined1 p f x -> ShowS Source # show :: Refined1 p f x -> String Source # showList :: [Refined1 p f x] -> ShowS Source #
NFData (f x) => NFData (Refined1 p f x) Source #
Instance details Defined in Refined.Unsafe.Type Methods rnf :: Refined1 p f x -> () Source #
Eq (f x) => Eq (Refined1 p f x) Source #
Instance details Defined in Refined.Unsafe.Type Methods (==) :: Refined1 p f x -> Refined1 p f x -> Bool Source # (/=) :: Refined1 p f x -> Refined1 p f x -> Bool Source #
Ord (f x) => Ord (Refined1 p f x) Source #
Instance details Defined in Refined.Unsafe.Type Methods compare :: Refined1 p f x -> Refined1 p f x -> Ordering Source # (<) :: Refined1 p f x -> Refined1 p f x -> Bool Source # (<=) :: Refined1 p f x -> Refined1 p f x -> Bool Source # (>) :: Refined1 p f x -> Refined1 p f x -> Bool Source # (>=) :: Refined1 p f x -> Refined1 p f x -> Bool Source # max :: Refined1 p f x -> Refined1 p f x -> Refined1 p f x Source # min :: Refined1 p f x -> Refined1 p f x -> Refined1 p f x Source #
Hashable (f x) => Hashable (Refined1 p f x) Source #
Instance details Defined in Refined.Unsafe.Type Methods hashWithSalt :: Int -> Refined1 p f x -> Int Source # hash :: Refined1 p f x -> Int Source #

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

reallyUnsafeRefine1 :: f x -> Refined1 p f x Source #

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