rerefined-0.3.0: Refinement types, again
Safe HaskellSafe-Inferred
LanguageGHC2021

Rerefined.Refined

Description

Refined and Refined1 definitions for refined values.

Not intended for external use. For unsafe refining, use Unsafe.

Synopsis

Refined

newtype Refined p a Source #

a refined with predicate p.

Constructors

Refined a 

Instances

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

Defined in Rerefined.Refined

Methods

lift :: Quote m => Refined p a -> m Exp #

liftTyped :: forall (m :: Type -> Type). Quote m => Refined p a -> Code m (Refined p a) #

Show a => Show (Refined p a) Source # 
Instance details

Defined in Rerefined.Refined

Methods

showsPrec :: Int -> Refined p a -> ShowS #

show :: Refined p a -> String #

showList :: [Refined p a] -> ShowS #

unrefine :: Refined p a -> a Source #

Strip the refinement from a Refined.

This is kept as a separate function for prettier Show Refined output.

Refined1

newtype Refined1 p f a Source #

f a refined with predicate p.

We may derive legal Functor, Traversable instances for this as Refine1 guarantees that the predicate only applies to the functor structure. That is, you _may_ alter a Refined1 without re-asserting its predicate, provided your changes are made without altering the structure/shape of f (e.g. fmap, traverse).

Constructors

Refined1 (f a) 

Instances

Instances details
Lift (f a) => Lift (Refined1 p f a :: Type) Source # 
Instance details

Defined in Rerefined.Refined

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

Defined in Rerefined.Refined

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

Defined in Rerefined.Refined

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

Defined in Rerefined.Refined

Methods

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

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

Show (f a) => Show (Refined1 p f a) Source # 
Instance details

Defined in Rerefined.Refined

Methods

showsPrec :: Int -> Refined1 p f a -> ShowS #

show :: Refined1 p f a -> String #

showList :: [Refined1 p f a] -> ShowS #

unrefine1 :: Refined1 p f a -> f a Source #

Strip the refinement from a Refined1.

This is kept as a separate function for prettier Show Refined1 output.

squashRefined1 :: Refined1 p f a -> Refined p (f a) Source #

Squash a Refined1 into a Refined. Essentially forget the f.