predicate-typed: a refinement type library

what this library provides:

1. a rich dsl for building refinement types eg regex expressions / arithmetic / datetime manipulation etc
2. visualisation of each step in the evaluation of an expression using a colorized tree
3. three types of Refinement types Refined/Refined2/Refined3
4. Template Haskell methods for creating the refinement types
5. Aeson (FromJSON ToJSON) instances
6. Read and Show instances
7. Binary instances
8. Hashable instances
9. IsString instances
10. Database encoders and decoders for refinement types (sqlhandler-odbc)

To run the examples you will need these settings (ghc>=8.6)

:set -XTypeApplications
:set -XDataKinds
:set -XPolyKinds
:set -XTemplateHaskell
:set -XNoStarIsType
:set -XTypeFamilies

Refined

*Refined2

Refined3

General information

• opts common display options for evaluating the typelevel expression

  • OZ no output:zero
  • OL one line:lite
  • OA ascii plus colors
  • OAN ascii without colors
  • OU unicode plus colors (for Windows: chcp 65001)

• Val is an ADT that holds the result of evaluating the type level expression

  • Val a : 'a' is any value
  • Fail String : indicates a failure with an error message

testing the dsl

• pu is a shortcut for run @OU (unicode with colors)
• pa is a shortcut for run @OA (ascii with colors)
• pl is a shortcut for run @OL (short one liner)
• pan is a shortcut for run @OAN (ascii without colors)

>pu @(Between 4 10 Id) 7
True 4 <= 7 <= 10
|
+- P Id 7
|
+- P '4
|
`- P '10
Val True

>pu @(Between 4 10 Id) 11
False 11 <= 10
|
+- P Id 11
|
+- P '4
|
`- P '10
Val False

>pu @(Between (4 % 7) (10 % 2) Id) 7
...
False (7 % 1 <= 5 % 1)
Val False

>pu @(Re "^[[:upper:]][[:lower:]]+") "Fred"
...
Val True

pu @(Re "^[[:upper:]][[:lower:]]+") "fred"
...
Val False

>pu @(Resplit "\\s+" >> GuardSimple (Len > 0 && All (Re "^[[:upper:]][[:lower:]]+"))) "Fred Abel Bart Jimmy"
...
Val ["Fred","Abel","Bart","Jimmy"]

>pu @(Resplit "\\s+" >> GuardSimple (Len > 0 && All (Re "^[[:upper:]][[:lower:]]+"))) "Fred Abel bart Jimmy"
...
Fail "(True && False | (All(4) i=2 (Re' [] (^[[:upper:]][[:lower:]]+) | bart)))"

>pu @(ReadP Day Id >> ToWeekDate Id >> Snd == "Monday") "2020-07-13"
...
Val True

>pu @(ReadP Day Id >> ToWeekDate Id >> Snd == "Monday") "2020-07-14"
...
False (>>) False | {"Tuesday" == "Monday"}
Val False

>pu @(ReadP Day Id >> ToWeekDate Id >> GuardSimple (Snd == "Monday")) "2020-07-13"
...
Val (1,"Monday")