Skip to content

Latest commit

 

History

History
127 lines (104 loc) · 2.78 KB

README.md

File metadata and controls

127 lines (104 loc) · 2.78 KB
Raw

predicate-typed: a refinement type library

Hackage

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