Predicate.Refined

Simple refinement type with only one type and a predicate

Refined

data Refined (opts :: OptT) p a

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 FalseT

>>> 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 FalseT

>>> prtRefinedIO @OZ @(Map (ReadP Int Id) (Resplit "\\." Id) >> Guard (PrintF "bad length: found %d" Len) (Len == 4) >> 'True) "141.213.1"
Left (FailT "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 (FailT "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 (FailT "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 FalseT

>>> 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 FalseT

>>> 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 (FailT "(!!) index not found")

>>> prtRefinedIO @OZ @(Snd Id !! Fst Id >> Len <= 5) (2,["abc","defghij","xyzxyazsfd"])
Left FalseT

Instances

Eq a => Eq (Refined opts p a)

Defined in Predicate.Refined

Methods

(==) :: Refined opts p a -> Refined opts p a -> Bool

(/=) :: Refined opts p a -> Refined opts p a -> Bool

(RefinedC opts p a, Read a) => Read (Refined opts p a)

Read instance for Refined

>>> reads @(Refined OZ (Between 0 255 Id) Int) "Refined 254"
[(Refined 254,"")]

>>> reads @(Refined OZ (Between 0 255 Id) Int) "Refined 300"
[]

>>> reads @(Refined OZ 'True Int) "Refined (-123)xyz"
[(Refined (-123),"xyz")]

Defined in Predicate.Refined

Methods

readsPrec :: Int -> ReadS (Refined opts p a)

readList :: ReadS [Refined opts p a]

readPrec :: ReadPrec (Refined opts p a)

readListPrec :: ReadPrec [Refined opts p a]

Show a => Show (Refined opts p a)

Defined in Predicate.Refined

Methods

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

show :: Refined opts p a -> String

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

RefinedC opts p String => IsString (Refined opts p String)

IsString instance for Refined

>>> pureTryTest $ fromString @(Refined OL (ReadP Int Id >> Id > 244) String) "523"
Right (Refined "523")

>>> pureTryTest $ fromString @(Refined OL (ReadP Int Id >> Id > 244) String) "52"
Left ()

Defined in Predicate.Refined

Methods

fromString :: String -> Refined opts p String

Generic (Refined opts p a)

Defined in Predicate.Refined

Associated Types

type Rep (Refined opts p a) :: Type -> Type

Methods

from :: Refined opts p a -> Rep (Refined opts p a) x

to :: Rep (Refined opts p a) x -> Refined opts p a

Lift a => Lift (Refined opts p a)

Defined in Predicate.Refined

Methods

lift :: Refined opts p a -> Q Exp

(Arbitrary a, RefinedC opts p a, Show a) => Arbitrary (Refined opts p a)

Arbitrary instance for Refined

>>> xs <- generate (vectorOf 10 (arbitrary @(Refined OU (Id /= 0) Int)))
>>> all ((/=0) . unRefined) xs
True

>>> xs <- generate (vectorOf 10 (arbitrary @(Refined OU (Prime Id) Int)))
>>> all (isPrime . unRefined) xs
True

Defined in Predicate.Refined

Methods

arbitrary :: Gen (Refined opts p a)

shrink :: Refined opts p a -> [Refined opts p a]

(RefinedC opts p a, Hashable a) => Hashable (Refined opts p a)

Hashable instance for Refined

Defined in Predicate.Refined

Methods

hashWithSalt :: Int -> Refined opts p a -> Int

hash :: Refined opts p a -> Int

ToJSON a => ToJSON (Refined opts p a)

ToJSON instance for Refined

Defined in Predicate.Refined

Methods

toJSON :: Refined opts p a -> Value

toEncoding :: Refined opts p a -> Encoding

toJSONList :: [Refined opts p a] -> Value

toEncodingList :: [Refined opts p a] -> Encoding

(RefinedC opts p a, FromJSON a) => FromJSON (Refined opts p a)

FromJSON instance for Refined

>>> :set -XOverloadedStrings
>>> import qualified Data.Aeson as A
>>> A.eitherDecode' @(Refined OZ (Between 10 14 Id) Int) "13"
Right (Refined 13)

>>> removeAnsi $ A.eitherDecode' @(Refined OAN (Between 10 14 Id) Int) "16"
Error in $: Refined(FromJSON:parseJSON):FalseT (16 <= 14)
False 16 <= 14
|
+- P Id 16
|
+- P '10
|
`- P '14

Defined in Predicate.Refined

Methods

parseJSON :: Value -> Parser (Refined opts p a)

parseJSONList :: Value -> Parser [Refined opts p a]

(RefinedC opts p a, Binary a) => Binary (Refined opts p a)

Binary instance for Refined

>>> import Data.Time
>>> import Control.Lens
>>> import Control.Arrow ((+++))
>>> type K1 = Refined OZ (ReadP Day Id >> 'True) String
>>> type K2 = Refined OAN (Between (ReadP Day "2019-05-30") (ReadP Day "2019-06-01") (ReadP Day Id)) String
>>> r = unsafeRefined' @OZ "2019-04-23" :: K1
>>> removeAnsi $ (view _3 +++ view _3) $ B.decodeOrFail @K1 (B.encode r)
Refined "2019-04-23"

>>> removeAnsi $ (view _3 +++ view _3) $ B.decodeOrFail @K2 (B.encode r)
Refined(Binary:get):FalseT (2019-05-30 <= 2019-04-23)
False 2019-05-30 <= 2019-04-23
|
+- P ReadP Day 2019-04-23
|  |
|  `- P Id "2019-04-23"
|
+- P ReadP Day 2019-05-30
|  |
|  `- P '"2019-05-30"
|
`- P ReadP Day 2019-06-01
   |
   `- P '"2019-06-01"

Defined in Predicate.Refined

Methods

put :: Refined opts p a -> Put

get :: Get (Refined opts p a)

putList :: [Refined opts p a] -> Put

type Rep (Refined opts p a)

Defined in Predicate.Refined

type Rep (Refined opts p a) = D1 (MetaData "Refined" "Predicate.Refined" "predicate-typed-0.7.2.0-LsjUtDgKRIuJtCd3aFXA1x" True) (C1 (MetaCons "Refined" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a)))

unRefined :: forall k (opts :: OptT) (p :: k) a. Refined opts p a -> a

extract the value from Refined

type RefinedC opts p a = (OptTC opts, PP p a ~ Bool, P p a)

the constraints that Refined must adhere to

newtype RefinedT m a

effect wrapper for the refinement value

Constructors

RefinedT

Fields

• unRefinedT :: ExceptT String (WriterT [String] m) a

Instances

MonadTrans RefinedT

Defined in Predicate.Refined

Methods

lift :: Monad m => m a -> RefinedT m a

Monad m => MonadError String (RefinedT m)

Defined in Predicate.Refined

Methods

throwError :: String -> RefinedT m a

catchError :: RefinedT m a -> (String -> RefinedT m a) -> RefinedT m a

Monad m => Monad (RefinedT m)

Defined in Predicate.Refined

Methods

(>>=) :: RefinedT m a -> (a -> RefinedT m b) -> RefinedT m b

(>>) :: RefinedT m a -> RefinedT m b -> RefinedT m b

return :: a -> RefinedT m a

fail :: String -> RefinedT m a

Functor m => Functor (RefinedT m)

Defined in Predicate.Refined

Methods

fmap :: (a -> b) -> RefinedT m a -> RefinedT m b

(<$) :: a -> RefinedT m b -> RefinedT m a

Monad m => Applicative (RefinedT m)

Defined in Predicate.Refined

Methods

pure :: a -> RefinedT m a

(<*>) :: RefinedT m (a -> b) -> RefinedT m a -> RefinedT m b

liftA2 :: (a -> b -> c) -> RefinedT m a -> RefinedT m b -> RefinedT m c

(*>) :: RefinedT m a -> RefinedT m b -> RefinedT m b

(<*) :: RefinedT m a -> RefinedT m b -> RefinedT m a

MonadIO m => MonadIO (RefinedT m)

Defined in Predicate.Refined

Methods

liftIO :: IO a -> RefinedT m a

MonadCont m => MonadCont (RefinedT m)

Defined in Predicate.Refined

Methods

callCC :: ((a -> RefinedT m b) -> RefinedT m a) -> RefinedT m a

Monad m => MonadWriter [String] (RefinedT m)

Defined in Predicate.Refined

Methods

writer :: (a, [String]) -> RefinedT m a

tell :: [String] -> RefinedT m ()

listen :: RefinedT m a -> RefinedT m (a, [String])

pass :: RefinedT m (a, [String] -> [String]) -> RefinedT m a

(Show1 m, Show a) => Show (RefinedT m a)

Defined in Predicate.Refined

Methods

showsPrec :: Int -> RefinedT m a -> ShowS

show :: RefinedT m a -> String

showList :: [RefinedT m a] -> ShowS

print methods

prtRefinedIO :: forall opts p a. RefinedC opts p a => a -> IO (Either (BoolT Bool) (Refined opts p a))

same as newRefined but prints the results

prtRefinedTIO :: (MonadIO m, Show a) => RefinedT m a -> m ()

create methods

newRefined :: forall opts p a. RefinedC opts p a => a -> Either String (Refined opts p a)

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))

withRefinedT :: forall opts p m a b. (Monad m, RefinedC opts p a) => a -> (Refined opts p a -> RefinedT m b) -> RefinedT m b

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

IO version of withRefinedT

newRefinedT :: forall m opts p a. (RefinedC opts p a, Monad m) => a -> RefinedT m (Refined opts p a)

returns a wrapper RefinedT around a possible Refined value if 'a' is valid for the predicate 'p'

newRefinedTIO :: forall opts p a m. (RefinedC opts p a, MonadIO m) => a -> RefinedT m (Refined opts p a)

IO version of newRefinedT

QuickCheck method

genRefined :: forall opts p a. RefinedC opts p a => Gen a -> Gen (Refined opts p a)

create Refined generator using a generator to restrict the values

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)

attempts to lift a refinement type to another refinement type by way of transformation function you can control both the predicate and the type

unRavelT :: RefinedT m a -> m (Either String a, [String])

unwrap the RefinedT value

rapply :: forall m opts p a opts1 z. (z ~ (opts :# opts1), OptTC opts1, RefinedC opts p a, Monad m) => (a -> a -> a) -> RefinedT m (Refined opts p a) -> RefinedT m (Refined opts1 p a) -> RefinedT m (Refined z p a)

binary operation applied to two RefinedT values

>>> x = newRefinedT @_ @OAN @(Between 4 12 Id) 4
>>> y = newRefinedT @_ @OAN @(Between 4 12 Id) 5
>>> prtRefinedTIO (rapply (+) x y)
=== a ===
True 4 <= 4 <= 12
|
+- P Id 4
|
+- P '4
|
`- P '12

=== b ===
True 4 <= 5 <= 12
|
+- P Id 5
|
+- P '4
|
`- P '12

=== a `op` b ===
True 4 <= 9 <= 12
|
+- P Id 9
|
+- P '4
|
`- P '12

Refined 9

>>> x = newRefinedT @_ @OAN @(Prime Id || Id < 3) 3
>>> y = newRefinedT @_ @OAN @(Prime Id || Id < 3) 5
>>> prtRefinedTIO (rapply (+) x y)
=== a ===
True True || False
|
+- True Prime
|  |
|  `- P Id 3
|
`- False 3 < 3
   |
   +- P Id 3
   |
   `- P '3

=== b ===
True True || False
|
+- True Prime
|  |
|  `- P Id 5
|
`- False 5 < 3
   |
   +- P Id 5
   |
   `- P '3

=== a `op` b ===
False False || False | (Prime) || (8 < 3)
|
+- False Prime
|  |
|  `- P Id 8
|
`- False 8 < 3
   |
   +- P Id 8
   |
   `- P '3

failure msg[FalseT]

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)

same as rapply except we already have valid Refined values as input

unsafe create methods

unsafeRefined :: forall opts p a. a -> Refined opts p a

create an unsafe Refined value without running the predicate

unsafeRefined' :: forall opts p a. (RefinedC opts p a, HasCallStack) => a -> Refined opts p a

create an unsafe Refined value and also run the predicate

type family ReplaceOptT (o :: OptT) t where ...

Equations

ReplaceOptT o (Refined _ p a) = Refined o p a

type family AppendOptT (o :: OptT) t where ...

Equations

AppendOptT o (Refined o' p a) = Refined (o' :# o) p a