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 :: Quote m => Refined p x -> m Exp

liftTyped :: forall (m :: Type -> Type). Quote m => Refined p x -> Code m (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

(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]

(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]

(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]

(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

NFData x => NFData (Refined p x)

Since: 0.5

Defined in Refined.Unsafe.Type

Methods

rnf :: Refined p x -> ()

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

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

data Refined1 (p :: k) f x

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

Lift (f a) => Lift (Refined1 p f a :: Type)

Defined in Refined.Unsafe.Type

Methods

lift :: Quote m => Refined1 p f a -> m Exp

liftTyped :: forall (m :: Type -> Type). Quote m => Refined1 p f a -> Code m (Refined1 p f a)

Foldable f => Foldable (Refined1 p f)

Defined in Refined.Unsafe.Type

Methods

fold :: Monoid m => Refined1 p f m -> m

foldMap :: Monoid m => (a -> m) -> Refined1 p f a -> m

foldMap' :: Monoid m => (a -> m) -> Refined1 p f a -> m

foldr :: (a -> b -> b) -> b -> Refined1 p f a -> b

foldr' :: (a -> b -> b) -> b -> Refined1 p f a -> b

foldl :: (b -> a -> b) -> b -> Refined1 p f a -> b

foldl' :: (b -> a -> b) -> b -> Refined1 p f a -> b

foldr1 :: (a -> a -> a) -> Refined1 p f a -> a

foldl1 :: (a -> a -> a) -> Refined1 p f a -> a

toList :: Refined1 p f a -> [a]

null :: Refined1 p f a -> Bool

length :: Refined1 p f a -> Int

elem :: Eq a => a -> Refined1 p f a -> Bool

maximum :: Ord a => Refined1 p f a -> a

minimum :: Ord a => Refined1 p f a -> a

sum :: Num a => Refined1 p f a -> a

product :: Num a => Refined1 p f a -> a

Traversable f => Traversable (Refined1 p f)

Defined in Refined.Unsafe.Type

Methods

traverse :: Applicative f0 => (a -> f0 b) -> Refined1 p f a -> f0 (Refined1 p f b)

sequenceA :: Applicative f0 => Refined1 p f (f0 a) -> f0 (Refined1 p f a)

mapM :: Monad m => (a -> m b) -> Refined1 p f a -> m (Refined1 p f b)

sequence :: Monad m => Refined1 p f (m a) -> m (Refined1 p f a)

Functor f => Functor (Refined1 p f)

Defined in Refined.Unsafe.Type

Methods

fmap :: (a -> b) -> Refined1 p f a -> Refined1 p f b

(<$) :: a -> Refined1 p f b -> Refined1 p f a

Show (f x) => Show (Refined1 p f x)

Defined in Refined.Unsafe.Type

Methods

showsPrec :: Int -> Refined1 p f x -> ShowS

show :: Refined1 p f x -> String

showList :: [Refined1 p f x] -> ShowS

NFData (f x) => NFData (Refined1 p f x)

Defined in Refined.Unsafe.Type

Methods

rnf :: Refined1 p f x -> ()

Eq (f x) => Eq (Refined1 p f x)

Defined in Refined.Unsafe.Type

Methods

(==) :: Refined1 p f x -> Refined1 p f x -> Bool

(/=) :: Refined1 p f x -> Refined1 p f x -> Bool

Ord (f x) => Ord (Refined1 p f x)

Defined in Refined.Unsafe.Type

Methods

compare :: Refined1 p f x -> Refined1 p f x -> Ordering

(<) :: Refined1 p f x -> Refined1 p f x -> Bool

(<=) :: Refined1 p f x -> Refined1 p f x -> Bool

(>) :: Refined1 p f x -> Refined1 p f x -> Bool

(>=) :: Refined1 p f x -> Refined1 p f x -> Bool

max :: Refined1 p f x -> Refined1 p f x -> Refined1 p f x

min :: Refined1 p f x -> Refined1 p f x -> Refined1 p f x

Hashable (f x) => Hashable (Refined1 p f x)

Defined in Refined.Unsafe.Type

Methods

hashWithSalt :: Int -> Refined1 p f x -> Int

hash :: Refined1 p f x -> Int

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

reallyUnsafeRefine1 :: f x -> Refined1 p f x

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