Safe Haskell | None |
---|---|
Language | Haskell2010 |
Simple refinement type with only one type and a predicate
Synopsis
- data Refined p a
- type RefinedC p a = (PP p a ~ Bool, P p a)
- newRefined :: forall p a m. (MonadEval m, RefinedC p a) => POpts -> a -> m ((BoolP, (String, String)), Maybe (Refined p a))
- newtype RefinedT m a = RefinedT {
- unRefinedT :: ExceptT String (WriterT [String] m) a
- prtRefinedIO :: forall p a. RefinedC p a => POpts -> a -> IO (Either BoolP (Refined p a))
- prtRefinedTIO :: (MonadIO m, Show a) => RefinedT m a -> m ()
- prtRefinedT :: (MonadIO m, Show a) => RefinedT Identity a -> m ()
- withRefinedT :: forall p m a b. (Monad m, RefinedC p a) => POpts -> a -> (Refined p a -> RefinedT m b) -> RefinedT m b
- withRefinedTIO :: forall p m a b. (MonadIO m, RefinedC p a) => POpts -> a -> (Refined p a -> RefinedT m b) -> RefinedT m b
- newRefinedT :: forall p a m. (RefinedC p a, Monad m) => POpts -> a -> RefinedT m (Refined p a)
- newRefinedTIO :: forall p a m. (RefinedC p a, MonadIO m) => POpts -> a -> RefinedT m (Refined p a)
- arbRefined :: forall p a. (Arbitrary a, RefinedC p a) => POpts -> Gen (Refined p a)
- convertRefinedT :: forall m p p1 a a1. (RefinedC p1 a1, Monad m) => POpts -> (a -> a1) -> RefinedT m (Refined p a) -> RefinedT m (Refined p1 a1)
- unRavelT :: RefinedT m a -> m (Either String a, [String])
- unRavelTIO :: RefinedT IO a -> IO (Either String a, [String])
- rapply :: forall m p a. (RefinedC p a, Monad m) => POpts -> (a -> a -> a) -> RefinedT m (Refined p a) -> RefinedT m (Refined p a) -> RefinedT m (Refined p a)
- rapply0 :: forall p a m. (RefinedC p a, Monad m) => POpts -> (a -> a -> a) -> a -> a -> RefinedT m (Refined p a)
- rapply1 :: forall m p a. (RefinedC p a, Monad m) => POpts -> (a -> a -> a) -> Refined p a -> Refined p a -> RefinedT m (Refined p a)
- unsafeRefined :: forall p a. a -> Refined p a
- unsafeRefined' :: forall p a. RefinedC p a => POpts -> a -> Refined p a
Refined
a simple refinement type that ensures the predicate 'p' holds for the type 'a'
>>>
prtRefinedIO @(Between 10 14 Id) oz 13
Right (Refined {unRefined = 13})
>>>
prtRefinedIO @(Between 10 14 Id) oz 99
Left FalseP
>>>
prtRefinedIO @(Last Id >> Len == 4) oz ["one","two","three","four"]
Right (Refined {unRefined = ["one","two","three","four"]})
>>>
prtRefinedIO @(Re "^\\d{1,3}\\.\\d{1,3}\\.\\d{1,3}\\.\\d{1,3}$" Id) oz "141.213.1.99"
Right (Refined {unRefined = "141.213.1.99"})
>>>
prtRefinedIO @(Re "^\\d{1,3}\\.\\d{1,3}\\.\\d{1,3}\\.\\d{1,3}$" Id) oz "141.213.1"
Left FalseP
>>>
prtRefinedIO @(Map (ReadP Int Id) (Resplit "\\." Id) >> Guard (PrintF "bad length: found %d" Len) (Len == 4) >> 'True) oz "141.213.1"
Left (FailP "bad length: found 3")
>>>
prtRefinedIO @(Map (ReadP Int Id) (Resplit "\\." Id) >> Guard (PrintF "bad length: found %d" Len) (Len == 4) >> GuardsN (PrintT "octet %d out of range %d" Id) 4 (Between 0 255 Id) >> 'True) oz "141.213.1.444"
Left (FailP "octet 3 out of range 444")
>>>
prtRefinedIO @(Map (ReadP Int Id) (Resplit "\\." Id) >> Guard (PrintF "bad length: found %d" Len) (Len == 4) >> GuardsN (PrintT "octet %d out of range %d" Id) 4 (Between 0 255 Id) >> 'True) oz "141.213.1x34.444"
Left (FailP "ReadP Int (1x34)")
>>>
prtRefinedIO @(Map ('[Id] >> ReadP Int Id) Id >> Luhn Id) oz "12344"
Right (Refined {unRefined = "12344"})
>>>
prtRefinedIO @(Map ('[Id] >> ReadP Int Id) Id >> Luhn Id) oz "12340"
Left FalseP
>>>
prtRefinedIO @(Any (Prime Id) Id) oz [11,13,17,18]
Right (Refined {unRefined = [11,13,17,18]})
>>>
prtRefinedIO @(All (Prime Id) Id) oz [11,13,17,18]
Left FalseP
>>>
prtRefinedIO @(Snd Id !! Fst Id >> Len > 5) oz (2,["abc","defghij","xyzxyazsfd"])
Right (Refined {unRefined = (2,["abc","defghij","xyzxyazsfd"])})
>>>
prtRefinedIO @(Snd Id !! Fst Id >> Len > 5) oz (27,["abc","defghij","xyzxyazsfd"])
Left (FailP "(!!) index not found")
>>>
prtRefinedIO @(Snd Id !! Fst Id >> Len <= 5) oz (2,["abc","defghij","xyzxyazsfd"])
Left FalseP
Instances
Eq a => Eq (Refined p a) Source # | |
(RefinedC p a, Read a) => Read (Refined p a) Source # |
|
Show a => Show (Refined p a) Source # | |
RefinedC p String => IsString (Refined p String) Source # | |
Defined in Predicate.Refined fromString :: String -> Refined p String # | |
Generic (Refined p a) Source # | |
Lift a => Lift (Refined p a) Source # | |
(RefinedC p a, Hashable a) => Hashable (Refined p a) Source # | |
Defined in Predicate.Refined | |
ToJSON a => ToJSON (Refined p a) Source # | |
Defined in Predicate.Refined | |
(RefinedC p a, FromJSON a) => FromJSON (Refined p a) Source # |
|
(RefinedC p a, Binary a) => Binary (Refined p a) Source # |
|
type Rep (Refined p a) Source # | |
Defined in Predicate.Refined |
newRefined :: forall p a m. (MonadEval m, RefinedC p a) => POpts -> a -> m ((BoolP, (String, String)), Maybe (Refined p a)) Source #
returns a Refined
value if 'a' is valid for the predicate 'p'
Instances
MonadTrans RefinedT Source # | |
Defined in Predicate.Refined | |
Monad m => MonadError String (RefinedT m) Source # | |
Defined in Predicate.Refined throwError :: String -> RefinedT m a # catchError :: RefinedT m a -> (String -> RefinedT m a) -> RefinedT m a # | |
Monad m => Monad (RefinedT m) Source # | |
Functor m => Functor (RefinedT m) Source # | |
Monad m => Applicative (RefinedT m) Source # | |
MonadIO m => MonadIO (RefinedT m) Source # | |
Defined in Predicate.Refined | |
MonadCont m => MonadCont (RefinedT m) Source # | |
Monad m => MonadWriter [String] (RefinedT m) Source # | |
(Show1 m, Show a) => Show (RefinedT m a) Source # | |
print methods
prtRefinedIO :: forall p a. RefinedC p a => POpts -> a -> IO (Either BoolP (Refined p a)) Source #
same as newRefined
but prints the results
create methods
withRefinedT :: forall p m a b. (Monad m, RefinedC p a) => POpts -> a -> (Refined p a -> RefinedT m b) -> RefinedT m b Source #
invokes the callback with the Refined
value if 'a' is valid for the predicate 'p'
withRefinedTIO :: forall p m a b. (MonadIO m, RefinedC p a) => POpts -> a -> (Refined p a -> RefinedT m b) -> RefinedT m b Source #
newRefinedT :: forall p a m. (RefinedC p a, Monad m) => POpts -> a -> RefinedT m (Refined p a) Source #
newRefinedTIO :: forall p a m. (RefinedC p a, MonadIO m) => POpts -> a -> RefinedT m (Refined p a) Source #
QuickCheck method
manipulate RefinedT values
convertRefinedT :: forall m p p1 a a1. (RefinedC p1 a1, Monad m) => POpts -> (a -> a1) -> RefinedT m (Refined p a) -> RefinedT m (Refined p1 a1) Source #
attempts to lift a refinement type to another refinement type by way of transformation function you can control both the predicate and the type
rapply :: forall m p a. (RefinedC p a, Monad m) => POpts -> (a -> a -> a) -> RefinedT m (Refined p a) -> RefinedT m (Refined p a) -> RefinedT m (Refined p a) Source #
binary operation applied to two RefinedT
values
rapply0 :: forall p a m. (RefinedC p a, Monad m) => POpts -> (a -> a -> a) -> a -> a -> RefinedT m (Refined p a) Source #
takes two values and lifts them into RefinedT
and then applies the binary operation
rapply1 :: forall m p a. (RefinedC p a, Monad m) => POpts -> (a -> a -> a) -> Refined p a -> Refined p a -> RefinedT m (Refined p a) Source #
unsafe create methods
unsafeRefined :: forall p a. a -> Refined p a Source #
a way to unsafely create a Refined
value