Safe Haskell | None |
---|---|
Language | Haskell2010 |
Simple refinement type with only one type and a predicate
Synopsis
- data Refined (opts :: OptT) p a
- unRefined :: forall k (opts :: OptT) (p :: k) a. Refined opts p a -> a
- type RefinedC opts p a = (OptTC opts, PP p a ~ Bool, P p a)
- newRefined :: forall opts p a. RefinedC opts p a => a -> Either String (Refined opts p a)
- newRefinedM :: forall opts p a m. (MonadEval m, RefinedC opts p a) => a -> m ((String, (String, String)), Maybe (Refined opts p a))
- newtype RefinedT m a = RefinedT {
- unRefinedT :: ExceptT String (WriterT [String] m) a
- prtRefinedIO :: forall opts p a. RefinedC opts p a => a -> IO (Either BoolP (Refined opts p a))
- prtRefinedTIO :: (MonadIO m, Show a) => RefinedT m a -> m ()
- withRefinedT :: forall opts p m a b. (Monad m, RefinedC opts p a) => a -> (Refined opts p a -> RefinedT m b) -> RefinedT m b
- withRefinedTIO :: forall opts p m a b. (MonadIO m, RefinedC opts p a) => a -> (Refined opts p a -> RefinedT m b) -> RefinedT m b
- newRefinedT :: forall m opts p a. (RefinedC opts p a, Monad m) => a -> RefinedT m (Refined opts p a)
- newRefinedTIO :: forall opts p a m. (RefinedC opts p a, MonadIO m) => a -> RefinedT m (Refined opts p a)
- genRefined :: forall opts p a. RefinedC opts p a => Gen a -> Gen (Refined opts p a)
- convertRefinedT :: forall m opts p a p1 a1. (RefinedC opts p1 a1, Monad m) => (a -> a1) -> RefinedT m (Refined opts p a) -> RefinedT m (Refined opts p1 a1)
- unRavelT :: RefinedT m a -> m (Either String a, [String])
- rapply :: forall m opts p a. (RefinedC opts p a, Monad m) => (a -> a -> a) -> RefinedT m (Refined opts p a) -> RefinedT m (Refined opts p a) -> RefinedT m (Refined opts p a)
- rapply0 :: forall opts p a m. (RefinedC opts p a, Monad m) => (a -> a -> a) -> a -> a -> RefinedT m (Refined opts p a)
- rapplyLift :: forall m opts p a. (RefinedC opts p a, Monad m) => (a -> a -> a) -> Refined opts p a -> Refined opts p a -> RefinedT m (Refined opts p a)
- unsafeRefined :: forall opts p a. a -> Refined opts p a
- unsafeRefined' :: forall opts p a. (RefinedC opts p a, HasCallStack) => a -> Refined opts p a
- type family ReplaceOptT (o :: OptT) t where ...
- type family AppendOptT (o :: OptT) t where ...
Refined
data Refined (opts :: OptT) p a Source #
a simple refinement type that ensures the predicate 'p' holds for the type 'a'
>>>
prtRefinedIO @'OZ @(Between 10 14 Id) 13
Right (Refined 13)
>>>
prtRefinedIO @'OZ @(Between 10 14 Id) 99
Left FalseP
>>>
prtRefinedIO @'OZ @(Last Id >> Len == 4) ["one","two","three","four"]
Right (Refined ["one","two","three","four"])
>>>
prtRefinedIO @'OZ @(Re "^\\d{1,3}\\.\\d{1,3}\\.\\d{1,3}\\.\\d{1,3}$" Id) "141.213.1.99"
Right (Refined "141.213.1.99")
>>>
prtRefinedIO @'OZ @(Re "^\\d{1,3}\\.\\d{1,3}\\.\\d{1,3}\\.\\d{1,3}$" Id) "141.213.1"
Left FalseP
>>>
prtRefinedIO @'OZ @(Map (ReadP Int Id) (Resplit "\\." Id) >> Guard (PrintF "bad length: found %d" Len) (Len == 4) >> 'True) "141.213.1"
Left (FailP "bad length: found 3")
>>>
prtRefinedIO @'OZ @(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) "141.213.1.444"
Left (FailP "octet 3 out of range 444")
>>>
prtRefinedIO @'OZ @(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) "141.213.1x34.444"
Left (FailP "ReadP Int (1x34)")
>>>
prtRefinedIO @'OZ @(Map ('[Id] >> ReadP Int Id) Id >> Luhn Id) "12344"
Right (Refined "12344")
>>>
prtRefinedIO @'OZ @(Map ('[Id] >> ReadP Int Id) Id >> Luhn Id) "12340"
Left FalseP
>>>
prtRefinedIO @'OZ @(Any (Prime Id) Id) [11,13,17,18]
Right (Refined [11,13,17,18])
>>>
prtRefinedIO @'OZ @(All (Prime Id) Id) [11,13,17,18]
Left FalseP
>>>
prtRefinedIO @'OZ @(Snd Id !! Fst Id >> Len > 5) (2,["abc","defghij","xyzxyazsfd"])
Right (Refined (2,["abc","defghij","xyzxyazsfd"]))
>>>
prtRefinedIO @'OZ @(Snd Id !! Fst Id >> Len > 5) (27,["abc","defghij","xyzxyazsfd"])
Left (FailP "(!!) index not found")
>>>
prtRefinedIO @'OZ @(Snd Id !! Fst Id >> Len <= 5) (2,["abc","defghij","xyzxyazsfd"])
Left FalseP
Instances
Eq a => Eq (Refined opts p a) Source # | |
(RefinedC opts p a, Read a) => Read (Refined opts p a) Source # |
|
Show a => Show (Refined opts p a) Source # | |
RefinedC opts p String => IsString (Refined opts p String) Source # | |
Defined in Predicate.Refined fromString :: String -> Refined opts p String # | |
Generic (Refined opts p a) Source # | |
Lift a => Lift (Refined opts p a) Source # | |
(Arbitrary a, RefinedC opts p a, Show a) => Arbitrary (Refined opts p a) Source # | |
(RefinedC opts p a, Hashable a) => Hashable (Refined opts p a) Source # | |
Defined in Predicate.Refined | |
ToJSON a => ToJSON (Refined opts p a) Source # | |
Defined in Predicate.Refined | |
(RefinedC opts p a, FromJSON a) => FromJSON (Refined opts p a) Source # |
|
(RefinedC opts p a, Binary a) => Binary (Refined opts p a) Source # |
|
type Rep (Refined opts p a) Source # | |
Defined in Predicate.Refined |
unRefined :: forall k (opts :: OptT) (p :: k) a. Refined opts p a -> a Source #
extract the value from Refined
type RefinedC opts p a = (OptTC opts, PP p a ~ Bool, P p a) Source #
the constraints that Refined
must adhere to
newRefined :: forall opts p a. RefinedC opts p a => a -> Either String (Refined opts p a) Source #
returns a Refined
value if 'a' is valid for the predicate 'p'
>>>
newRefined @'OL @(ReadP Int Id > 99) "123"
Right (Refined "123")
>>>
newRefined @'OL @(ReadP Int Id > 99) "12"
Left "FalseT (12 > 99)"
newRefinedM :: forall opts p a m. (MonadEval m, RefinedC opts p a) => a -> m ((String, (String, String)), Maybe (Refined opts p a)) Source #
effect wrapper for the refinement value
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 opts p a. RefinedC opts p a => a -> IO (Either BoolP (Refined opts p a)) Source #
same as newRefined
but prints the results
create methods
withRefinedT :: forall opts p m a b. (Monad m, RefinedC opts p a) => a -> (Refined opts 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 opts p m a b. (MonadIO m, RefinedC opts p a) => a -> (Refined opts p a -> RefinedT m b) -> RefinedT m b Source #
IO version of withRefinedT
newRefinedT :: forall m opts p a. (RefinedC opts p a, Monad m) => a -> RefinedT m (Refined opts p a) Source #
newRefinedTIO :: forall opts p a m. (RefinedC opts p a, MonadIO m) => a -> RefinedT m (Refined opts p a) Source #
IO version of newRefinedT
QuickCheck method
manipulate RefinedT values
convertRefinedT :: forall m opts p a p1 a1. (RefinedC opts p1 a1, Monad m) => (a -> a1) -> RefinedT m (Refined opts p a) -> RefinedT m (Refined opts 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 opts p a. (RefinedC opts p a, Monad m) => (a -> a -> a) -> RefinedT m (Refined opts p a) -> RefinedT m (Refined opts p a) -> RefinedT m (Refined opts p a) Source #
binary operation applied to two RefinedT
values
rapply0 :: forall opts p a m. (RefinedC opts p a, Monad m) => (a -> a -> a) -> a -> a -> RefinedT m (Refined opts p a) Source #
takes two values and lifts them into RefinedT
and then applies the binary operation
rapplyLift :: forall m opts p a. (RefinedC opts p a, Monad m) => (a -> a -> a) -> Refined opts p a -> Refined opts p a -> RefinedT m (Refined opts p a) Source #
unsafe create methods
unsafeRefined :: forall opts p a. a -> Refined opts p a Source #
create an unsafe Refined
value without running the predicate
unsafeRefined' :: forall opts p a. (RefinedC opts p a, HasCallStack) => a -> Refined opts p a Source #
create an unsafe Refined
value and also run the predicate
type family ReplaceOptT (o :: OptT) t where ... Source #
ReplaceOptT o (Refined _ p a) = Refined o p a |
type family AppendOptT (o :: OptT) t where ... Source #
AppendOptT o (Refined o' p a) = Refined (o' :# o) p a |