Predicate.Refined1

Refinement type allowing the external type to differ from the internal type doesnt store the output value but runs on demand but has calculate each time and could fail later see Refined1

similar to Refined2 but also provides:
* quickCheck methods
* ability to combine refinement types
* a canonical output value using the 'fmt' parameter

Refined1

data Refined1 ip op fmt i

Refinement type that differentiates the input from output: similar to Refined3 but only creates the output value as needed.

• i is the input type
• ip converts i to PP ip i which is the internal type and stored in unRefined1
• op validates that internal type using PP op (PP ip i) ~ Bool
• fmt outputs the internal type PP fmt (PP ip i) ~ i (not stored anywhere but created on demand)
• PP fmt (PP ip i) should be valid as input for Refined1

Setting ip to Id and fmt to Id makes it equivalent to Refined: see RefinedEmulate

Setting the input type i to String resembles the corresponding Read/Show instances but with an additional predicate on the read value

• read a string using ip into an internal type and store in unRefined1
• validate unRefined1 using the predicate op
• show unRefined1 using fmt (does not store the formatted result unlike Refined3)

Although a common scenario is String as input, you are free to choose any input type you like

>>> prtEval1 @(ReadBase Int 16 Id) @(Lt 255) @(PrintF "%x" Id) oz "00fe"
Right (Refined1 {unRefined1 = 254})

>>> prtEval1 @(ReadBase Int 16 Id) @(Lt 253) @(PrintF "%x" Id) oz "00fe"
Left Step 2. False Boolean Check(op) | FalseP

>>> prtEval1 @(ReadBase Int 16 Id) @(Lt 255) @(PrintF "%x" Id) oz "00fg"
Left Step 1. Initial Conversion(ip) Failed | invalid base 16

>>> prtEval1 @(Map (ReadP Int Id) (Resplit "\\." Id)) @(Msg "length invalid:" (Len == 4)) @(PrintL 4 "%03d.%03d.%03d.%03d" Id) ol "198.162.3.1.5"
Left Step 2. False Boolean Check(op) | {length invalid:5 == 4}

>>> prtEval1 @(Map (ReadP Int Id) (Resplit "\\." Id)) @(Guard (PrintF "found length=%d" Len) (Len == 4) >> 'True) @(PrintL 4 "%03d.%03d.%03d.%03d" Id) oz "198.162.3.1.5"
Left Step 2. Failed Boolean Check(op) | found length=5

>>> prtEval1 @(Map (ReadP Int Id) (Resplit "\\." Id)) @(Guard (PrintF "found length=%d" Len) (Len == 4) >> 'True) @(PrintL 4 "%03d.%03d.%03d.%03d" Id) oz "198.162.3.1"
Right (Refined1 {unRefined1 = [198,162,3,1]})

>>> :m + Data.Time.Calendar.WeekDate
>>> prtEval1 @(MkDay >> 'Just Id) @(Guard "expected a Sunday" (Thd Id == 7) >> 'True) @(UnMkDay (Fst Id)) oz (2019,10,13)
Right (Refined1 {unRefined1 = (2019-10-13,41,7)})

>>> prtEval1 @(MkDay >> 'Just Id) @(Msg "expected a Sunday:" (Thd Id == 7)) @(UnMkDay (Fst Id)) ol (2019,10,12)
Left Step 2. False Boolean Check(op) | {expected a Sunday:6 == 7}

>>> prtEval1 @(MkDay' (Fst Id) (Snd Id) (Thd Id) >> 'Just Id) @(Guard "expected a Sunday" (Thd Id == 7) >> 'True) @(UnMkDay (Fst Id)) oz (2019,10,12)
Left Step 2. Failed Boolean Check(op) | expected a Sunday

>>> type T4 k = '(MkDay >> 'Just Id, Guard "expected a Sunday" (Thd Id == 7) >> 'True, UnMkDay (Fst Id), k)
>>> prtEval1P (Proxy @(T4 _)) oz (2019,10,12)
Left Step 2. Failed Boolean Check(op) | expected a Sunday

>>> prtEval1P (Proxy @(T4 _)) oz (2019,10,13)
Right (Refined1 {unRefined1 = (2019-10-13,41,7)})

Instances

(Eq i, Eq (PP ip i), Eq (PP fmt (PP ip i))) => Eq (Refined1 ip op fmt i)

Defined in Predicate.Refined1

Methods

(==) :: Refined1 ip op fmt i -> Refined1 ip op fmt i -> Bool

(/=) :: Refined1 ip op fmt i -> Refined1 ip op fmt i -> Bool

(Eq i, Show i, Eq (PP ip i), Show (PP ip i), Refined1C ip op fmt i, Read (PP ip i), Read (PP fmt (PP ip i))) => Read (Refined1 ip op fmt i)

Read instance for Refined1

>>> reads @(Refined1 (ReadBase Int 16 Id) (Between 0 255 Id) (ShowBase 16 Id) String) "Refined1 {unRefined1 = 254}"
[(Refined1 {unRefined1 = 254},"")]

>>> reads @(Refined1 (ReadBase Int 16 Id) (Between 0 255 Id) (ShowBase 16 Id) String) "Refined1 {unRefined1 = 300}"
[]

>>> reads @(Refined1 (ReadBase Int 16 Id) (Id < 0) (ShowBase 16 Id) String) "Refined1 {unRefined1 = -1234}"
[(Refined1 {unRefined1 = -1234},"")]

>>> reads @(Refined1 (Map (ReadP Int Id) (Resplit "\\." Id)) (Guard "len/=4" (Len == 4) >> 'True) (PrintL 4 "%d.%d.%d.%d" Id) String) "Refined1 {unRefined1 = [192,168,0,1]}"
[(Refined1 {unRefined1 = [192,168,0,1]},"")]

Defined in Predicate.Refined1

Methods

readsPrec :: Int -> ReadS (Refined1 ip op fmt i)

readList :: ReadS [Refined1 ip op fmt i]

readPrec :: ReadPrec (Refined1 ip op fmt i)

readListPrec :: ReadPrec [Refined1 ip op fmt i]

(Show i, Show (PP ip i), Show (PP fmt (PP ip i))) => Show (Refined1 ip op fmt i)

Defined in Predicate.Refined1

Methods

showsPrec :: Int -> Refined1 ip op fmt i -> ShowS

show :: Refined1 ip op fmt i -> String

showList :: [Refined1 ip op fmt i] -> ShowS

(Refined1C ip op fmt String, Show (PP ip String)) => IsString (Refined1 ip op fmt String)

Defined in Predicate.Refined1

Methods

fromString :: String -> Refined1 ip op fmt String

(Lift (PP ip i), Lift (PP fmt (PP ip i))) => Lift (Refined1 ip op fmt i)

Defined in Predicate.Refined1

Methods

lift :: Refined1 ip op fmt i -> Q Exp

(Refined1C ip op fmt i, Hashable (PP ip i)) => Hashable (Refined1 ip op fmt i)

Hashable instance for Refined1

Defined in Predicate.Refined1

Methods

hashWithSalt :: Int -> Refined1 ip op fmt i -> Int

hash :: Refined1 ip op fmt i -> Int

(Show (PP fmt (PP ip i)), ToJSON (PP fmt (PP ip i)), P fmt (PP ip i)) => ToJSON (Refined1 ip op fmt i)

ToJSON instance for Refined1

>>> import qualified Data.Aeson as A
>>> A.encode (unsafeRefined1 @(ReadBase Int 16 Id) @(Between 0 255 Id) @(ShowBase 16 Id) 254)
"\"fe\""

>>> A.encode (unsafeRefined1 @Id @'True @Id 123)
"123"

Defined in Predicate.Refined1

Methods

toJSON :: Refined1 ip op fmt i -> Value

toEncoding :: Refined1 ip op fmt i -> Encoding

toJSONList :: [Refined1 ip op fmt i] -> Value

toEncodingList :: [Refined1 ip op fmt i] -> Encoding

(Show (PP fmt (PP ip i)), Show (PP ip i), Refined1C ip op fmt i, FromJSON i) => FromJSON (Refined1 ip op fmt i)

FromJSON instance for Refined1

>>> import qualified Data.Aeson as A
>>> A.eitherDecode' @(Refined1 (ReadBase Int 16 Id) (Id > 10 && Id < 256) (ShowBase 16 Id) String) "\"00fe\""
Right (Refined1 {unRefined1 = 254})

>>> removeAnsi $ A.eitherDecode' @(Refined1 (ReadBase Int 16 Id) (Id > 10 && Id < 256) (ShowBase 16 Id) String) "\"00fe443a\""
Error in $: Refined1:Step 2. False Boolean Check(op) | {True && False | (16663610 < 256)}

*** Step 1. Success Initial Conversion(ip) [16663610] ***

P ReadBase(Int,16) 16663610 | "00fe443a"
|
`- P Id "00fe443a"

*** Step 2. False Boolean Check(op) ***

False True && False | (16663610 < 256)
|
+- True 16663610 > 10
|  |
|  +- P Id 16663610
|  |
|  `- P '10
|
`- False 16663610 < 256
   |
   +- P Id 16663610
   |
   `- P '256

Defined in Predicate.Refined1

Methods

parseJSON :: Value -> Parser (Refined1 ip op fmt i)

parseJSONList :: Value -> Parser [Refined1 ip op fmt i]

(Show (PP fmt (PP ip i)), Show (PP ip i), Refined1C ip op fmt i, Binary i) => Binary (Refined1 ip op fmt i)

Binary instance for Refined1

>>> import Control.Arrow ((+++))
>>> import Control.Lens
>>> import Data.Time
>>> type K1 = MakeR1 '(ReadP Day Id, 'True, ShowP Id, String)
>>> type K2 = MakeR1 '(ReadP Day Id, Between (ReadP Day "2019-05-30") (ReadP Day "2019-06-01") Id, ShowP Id, String)
>>> r = unsafeRefined1' oz "2019-04-23" :: K1
>>> removeAnsi $ (view _3 +++ view _3) $ B.decodeOrFail @K1 (B.encode r)
Refined1 {unRefined1 = 2019-04-23}

>>> removeAnsi $ (view _3 +++ view _3) $ B.decodeOrFail @K2 (B.encode r)
Refined1:Step 2. False Boolean Check(op) | {2019-05-30 <= 2019-04-23}

*** Step 1. Success Initial Conversion(ip) [2019-04-23] ***

P ReadP Day 2019-04-23
|
`- P Id "2019-04-23"

*** Step 2. False Boolean Check(op) ***

False 2019-05-30 <= 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.Refined1

Methods

put :: Refined1 ip op fmt i -> Put

get :: Get (Refined1 ip op fmt i)

putList :: [Refined1 ip op fmt i] -> Put

type Refined1C ip op fmt i = (P ip i, P op (PP ip i), PP op (PP ip i) ~ Bool, P fmt (PP ip i), PP fmt (PP ip i) ~ i)

Provides the constraints on Refined1

display results

prtEval1 :: forall ip op fmt i. (Refined1C ip op fmt i, Show (PP ip i), Show i) => POpts -> i -> Either Msg1 (Refined1 ip op fmt i)

same as prtEval1P but skips the proxy and allows you to set each parameter individually using type application

prtEval1P :: forall ip op fmt i proxy. (Refined1C ip op fmt i, Show (PP ip i), Show i) => proxy '(ip, op, fmt, i) -> POpts -> i -> Either Msg1 (Refined1 ip op fmt i)

create a Refined1 using a 4-tuple proxy and aggregate the results on failure

prtEval1PIO :: forall ip op fmt i proxy. (Refined1C ip op fmt i, Show (PP ip i), Show i) => proxy '(ip, op, fmt, i) -> POpts -> i -> IO (Either String (Refined1 ip op fmt i))

same as prtEval1P but runs in IO

prt1IO :: (Show a, Show b) => POpts -> (RResults1 a b, Maybe r) -> IO (Either String r)

prt1 :: (Show a, Show b) => POpts -> (RResults1 a b, Maybe r) -> Either Msg1 r

prt1Impl :: (Show a, Show b) => POpts -> RResults1 a b -> Msg1

data Msg1

Constructors

Msg1

Fields

• m1Desc :: !String
• m1Short :: !String
• m1Long :: !String

Instances

Eq Msg1

Defined in Predicate.Refined1

Methods

(==) :: Msg1 -> Msg1 -> Bool

(/=) :: Msg1 -> Msg1 -> Bool

Show Msg1

Defined in Predicate.Refined1

Methods

showsPrec :: Int -> Msg1 -> ShowS

show :: Msg1 -> String

showList :: [Msg1] -> ShowS

data RResults1 a b

An ADT that summarises the results of evaluating Refined1 representing all possible states

Constructors

RF !String !(Tree PE)

RTF !a !(Tree PE) !String !(Tree PE)

RTFalse !a (Tree PE) !(Tree PE)

RTTrueF !a (Tree PE) !(Tree PE) !String !(Tree PE)

RTTrueT !a (Tree PE) !(Tree PE) !b !(Tree PE)

Instances

(Show a, Show b) => Show (RResults1 a b)

Defined in Predicate.Refined1

Methods

showsPrec :: Int -> RResults1 a b -> ShowS

show :: RResults1 a b -> String

showList :: [RResults1 a b] -> ShowS

evaluation methods

eval1 :: forall ip op fmt i. Refined1C ip op fmt i => POpts -> i -> (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined1 ip op fmt i))

same as eval1P but can pass the parameters individually using type application

eval1P :: forall ip op fmt i proxy. Refined1C ip op fmt i => proxy '(ip, op, fmt, i) -> POpts -> i -> (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined1 ip op fmt i))

create a Refined1 value using a 4-tuple proxy (see mkProxy1)

use mkProxy1 to package all the types together as a 4-tuple

create a wrapped Refined1 value

newRefined1T :: forall m ip op fmt i. (Refined1C ip op fmt i, Monad m, Show (PP ip i), Show i) => POpts -> i -> RefinedT m (Refined1 ip op fmt i)

newRefined1TP :: forall m ip op fmt i proxy. (Refined1C ip op fmt i, Monad m, Show (PP ip i), Show i) => proxy '(ip, op, fmt, i) -> POpts -> i -> RefinedT m (Refined1 ip op fmt i)

create a wrapped Refined1 type

>>> prtRefinedTIO $ newRefined1TP (Proxy @'(MkDay >> Just Id, GuardSimple (Thd Id == 5) >> 'True, UnMkDay (Fst Id), (Int,Int,Int))) oz (2019,11,1)
Refined1 {unRefined1 = (2019-11-01,44,5)}

>>> prtRefinedTIO $ newRefined1TP (Proxy @'(MkDay >> Just Id, Thd Id == 5, UnMkDay (Fst Id), (Int,Int,Int))) ol (2019,11,2)
failure msg[Step 2. False Boolean Check(op) | {6 == 5}]

>>> prtRefinedTIO $ newRefined1TP (Proxy @'(MkDay >> Just Id, Msg "wrong day:" (Thd Id == 5), UnMkDay (Fst Id), (Int,Int,Int))) ol (2019,11,2)
failure msg[Step 2. False Boolean Check(op) | {wrong day:6 == 5}]

newRefined1TPIO :: forall m ip op fmt i proxy. (Refined1C ip op fmt i, MonadIO m, Show (PP ip i), Show i) => proxy '(ip, op, fmt, i) -> POpts -> i -> RefinedT m (Refined1 ip op fmt i)

withRefined1T :: forall ip op fmt i m b. (Monad m, Refined1C ip op fmt i, Show (PP ip i), Show i) => POpts -> i -> (Refined1 ip op fmt i -> RefinedT m b) -> RefinedT m b

create a Refined1 value using a continuation

This first example reads a hex string and makes sure it is between 100 and 200 and then reads a binary string and adds the values together

>>> :set -XPolyKinds
>>> b16 = Proxy @'(ReadBase Int 16 Id, Between 100 200 Id, ShowBase 16 Id, String)
>>> b2 = Proxy @'(ReadBase Int 2 Id, 'True, ShowBase 2 Id, String)
>>> prtRefinedTIO $ withRefined1TP b16 oz "a3" $ \x -> withRefined1TP b2 oz "1001110111" $ \y -> pure (unRefined1 x + unRefined1 y)
794

this example fails as the the hex value is out of range

>>> prtRefinedTIO $ withRefined1TP b16 o0 "a388" $ \x -> withRefined1TP b2 o0 "1001110111" $ \y -> pure (x,y)

*** Step 1. Success Initial Conversion(ip) [41864] ***

P ReadBase(Int,16) 41864 | "a388"
|
`- P Id "a388"

*** Step 2. False Boolean Check(op) ***

False 41864 <= 200
|
+- P Id 41864
|
+- P '100
|
`- P '200

failure msg[Step 2. False Boolean Check(op) | {41864 <= 200}]

withRefined1TIO :: forall ip op fmt i m b. (MonadIO m, Refined1C ip op fmt i, Show (PP ip i), Show i) => POpts -> i -> (Refined1 ip op fmt i -> RefinedT m b) -> RefinedT m b

withRefined1TP :: forall m ip op fmt i b proxy. (Monad m, Refined1C ip op fmt i, Show (PP ip i), Show i) => proxy '(ip, op, fmt, i) -> POpts -> i -> (Refined1 ip op fmt i -> RefinedT m b) -> RefinedT m b

proxy methods

mkProxy1 :: forall z ip op fmt i. z ~ '(ip, op, fmt, i) => Proxy '(ip, op, fmt, i)

creates a 4-tuple proxy (see withRefined1TP newRefined1TP eval1P prtEval1P)

use type application to set the 4-tuple or set the individual parameters directly

set the 4-tuple directly

>>> eg1 = mkProxy1 @'(ReadP Int Id, Gt 10, ShowP Id, String)
>>> prtEval1P eg1 ol "24"
Right (Refined1 {unRefined1 = 24})

skip the 4-tuple and set each parameter individually using type application

>>> eg2 = mkProxy1 @_ @(ReadP Int Id) @(Gt 10) @(ShowP Id)
>>> prtEval1P eg2 ol "24"
Right (Refined1 {unRefined1 = 24})

mkProxy1' :: forall z ip op fmt i. (z ~ '(ip, op, fmt, i), Refined1C ip op fmt i) => Proxy '(ip, op, fmt, i)

same as mkProxy1 but checks to make sure the proxy is consistent with the Refined1C constraint

type family MakeR1 p where ...

type family for converting from a 4-tuple '(ip,op,fmt,i) to a Refined1 type

Equations

MakeR1 '(ip, op, fmt, i) = Refined1 ip op fmt i

unsafe methods for creating Refined1

unsafeRefined1 :: forall ip op fmt i. PP ip i -> Refined1 ip op fmt i

directly load values into Refined1 without any checking

unsafeRefined1' :: forall ip op fmt i. (HasCallStack, Show i, Show (PP ip i), Refined1C ip op fmt i) => POpts -> i -> Refined1 ip op fmt i

directly load values into Refined1. It still checks to see that those values are valid

combine Refined1 values

convertRefined1TP :: forall m ip op fmt i ip1 op1 fmt1 i1. (Refined1C ip1 op1 fmt1 i1, Monad m, Show (PP ip i), PP ip i ~ PP ip1 i1, Show i1) => Proxy '(ip, op, fmt, i) -> Proxy '(ip1, op1, fmt1, i1) -> POpts -> RefinedT m (Refined1 ip op fmt i) -> RefinedT m (Refined1 ip1 op1 fmt1 i1)

attempts to cast a wrapped Refined1 to another Refined1 with different predicates

rapply1 :: forall m ip op fmt i. (Refined1C ip op fmt i, Monad m, Show (PP ip i), Show i) => POpts -> (PP ip i -> PP ip i -> PP ip i) -> RefinedT m (Refined1 ip op fmt i) -> RefinedT m (Refined1 ip op fmt i) -> RefinedT m (Refined1 ip op fmt i)

applies a binary operation to two wrapped Refined1 parameters

rapply1P :: forall m ip op fmt i proxy. (Refined1C ip op fmt i, Monad m, Show (PP ip i), Show i) => proxy '(ip, op, fmt, i) -> POpts -> (PP ip i -> PP ip i -> PP ip i) -> RefinedT m (Refined1 ip op fmt i) -> RefinedT m (Refined1 ip op fmt i) -> RefinedT m (Refined1 ip op fmt i)

same as rapply1 but uses a 4-tuple proxy instead

QuickCheck methods

arbRefined1 :: forall ip op fmt i. (Arbitrary (PP ip i), Refined1C ip op fmt i) => Proxy '(ip, op, fmt, i) -> Gen (Refined1 ip op fmt i)

arbRefined1With :: forall ip op fmt i. (Arbitrary (PP ip i), Refined1C ip op fmt i) => Proxy '(ip, op, fmt, i) -> (PP ip i -> PP ip i) -> Gen (Refined1 ip op fmt i)

uses arbitrary to generate the internal unRefined1 and then uses 'fmt' to fill create output value

emulate Refined1 using Refined

type RefinedEmulate p a = Refined1 Id p Id a

emulates Refined using Refined1 by setting the input conversion and output formatting as noops

eval1PX :: forall ip op fmt i proxy. Refined1C ip op fmt i => proxy '(ip, op, fmt, i) -> POpts -> i -> (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined op (PP ip i), PP fmt (PP ip i)))

similar to eval1P but it emulates Refined1 but using Refined

takes a 4-tuple proxy as input but outputs the Refined value and the result separately

• initial conversion using 'ip' and stores that in Refined
• runs the boolean predicate 'op' to make sure to validate the converted value from 1.
• runs 'fmt' against the converted value from 1.
• returns both the Refined and the output from 3.
• if any of the above steps fail the process stops it and dumps out RResults1

eval1X :: forall ip op fmt i. Refined1C ip op fmt i => POpts -> i -> (RResults1 (PP ip i) (PP fmt (PP ip i)), Maybe (Refined op (PP ip i), PP fmt (PP ip i)))

same as eval1PX but allows you to set the parameters individually using type application

extract from 4-tuple

type family T4_1 x where ...

used by Refined1 to extract 'ip' from a promoted 4-tuple

>>> pl @(T4_1 Predicate.Examples.Refined3.Ip4) "1.2.3.4"
Present [1,2,3,4] (Map [1,2,3,4] | ["1","2","3","4"])
PresentT [1,2,3,4]

Equations

T4_1 '(a, b, c, d) = a

type family T4_2 x where ...

used by Refined1 for extracting the boolean predicate 'op' from a promoted 4-tuple

>>> pl @(T4_2 Predicate.Examples.Refined3.Ip4) [141,213,308,4]
Error octet 2 out of range 0-255 found 308
FailT "octet 2 out of range 0-255 found 308"

>>> pl @(T4_2 Predicate.Examples.Refined3.Ip4) [141,213,308,4,8]
Error Guards:invalid length(5) expected 4
FailT "Guards:invalid length(5) expected 4"

Equations

T4_2 '(a, b, c, d) = b

type family T4_3 x where ...

used by Refined1 for extracting 'fmt' from a promoted 4-tuple

>>> pl @(T4_3 Predicate.Examples.Refined3.Ip4) [141,513,9,4]
Present "141.513.009.004" (PrintL(4) [141.513.009.004] | s=%03d.%03d.%03d.%03d)
PresentT "141.513.009.004"

Equations

T4_3 '(a, b, c, d) = c

type family T4_4 x where ...

used by Refined1 for extracting the input type 'i' from a promoted 4-tuple

Equations

T4_4 '(a, b, c, d) = d