[discussion] Catch contradictory predicates when declaring refined type

[kachayev]

That's a kinda tricky thing to do...

From "obvious" steps we can take:

1. Mark types & predicates as :seq, :num and :string and converge the predicates tree to the most "common" one. In case of mismatch show the error

2. For ordering predicates, we can do basic checks with :num types using simple rules to deal with intervals

3. Anything else...?

A few example of what I want to "catch":

(r/refined s/Str (r/Greater 0))
(r/refined [s/Str] (r/First (r/Greater 0)))
(r/And (r/Greater 0) r/NonEmpty))
(r/refined (r/refined [s/Str] r/NonEmpty) (r/Greater 0))
(r/refined (r/NonEmptyListOf s/Str) (r/First (r/Greater 0)))

More on "dependent types":

(r/And (r/Greater 0) (r/Less 0)) ;; (r/Equal 0)
(r/And (r/Greater 0) (r/Less -1)) ;; error
(r/Or (r/Greater 0) (r/Greater 10)) ;; (r/Greater 0)
(r/refined NonEmptyStr NonEmpty) ;; NonEmptyStr

Neat and very nice to have:

(r/refined [s/Str] (Less 0)) ;; error suggesting to use (On count (Less 0))
(r/refined [s/Str] (On count NonEmpty)) ;; error becuase `count` returns to numeric
(r/refined double (On count NonEmpty)) ;; error becuase `count` does not accept double

[gsnewmark]

(r/refined s/Num (r/StartsWith "1")) ; error

This one is probably too complex/specific (r/refined r/ASCIILetterChar (r/Includes "ї")) ; error

[kachayev]

@gsnewmark Even more specific

(r/refined (r/BoundedSizeStr 1 5) (r/Includes "thisiswaytoolong")) 

[kachayev]

I've started work on this here

There's an interesting question: should we always treat Equal as a numerical predicate? Or derive from the type of the value given? @gsnewmark @serzh Any thoughts on this?

[gsnewmark]

@kachayev why numerical? I prefer deriving it from the value, because nothing in it is specific to numbers.
We need something like this http://hackage.haskell.org/package/base-4.11.1.0/docs/Data-Eq.html 🙈 🙃

[kachayev]

@gsnewmark Because it's easier to reason about when it's predictable. We use = now, which might be not the best fit for your understanding of "equality". If we keep this straightforward using Less, Greater, Equal are of the same kind... it might help.

[gsnewmark]

🤷‍♀️ what if I want to check string for equality?

[gsnewmark]

Let's rename it to something like NumericEqual then

[serzh]

Will we create “Equal” predicate for every type? Im not sure it’s a good idea. Why it can’t be polymorphic? In case of checking for “impossible” predicate it doesn’t matter, you just need to check other preds are satisfied with this value (And (Equal 3) LowerCase) (LowerCase 3) ; => not satisfied

…

On Jun 27, 2018, at 19:52, Ivan Kryvoruchko ***@***.***> wrote: Let's rename it to something like NumericEqual then — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub, or mute the thread.

[kachayev]

You still have (s/eq _) and #(= _ %) or whatever. My concern is that Equal is positioned right now as a "companion" for Less, Greater, LessOrEqual, GreaterOrEqual. And for Less/Greater we except only numerical.

@serzh Deriving type from the value you're still able to catch (And (Equal 3) LowerCase) earlier.

[serzh]

In that case just renaming will be sufficient 👍

…

On Jun 27, 2018, at 20:20, Oleksii Kachaiev ***@***.***> wrote: You still have (s/eq _) and #(= _ %) or whatever. My concern is that Equal is positioned right now as a "companion" for Less, Greater, LessOrEqual, GreaterOrEqual. And for Less/Greater we except only numerical. @sergmarch Deriving type from the value you're still able catch (And (Equal 3) LowerCase) earlier. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub, or mute the thread.

[serzh]

@kachayev Can we have a separate exception for that type of error, instead of generic j.l.IllegalArgumentException?

[kachayev]

@serzh Why?

[serzh]

I have a use case where I want to analyze that two schemas don't have (or do have) something in common.

[kachayev]

😱

[kachayev]

For example? I didn't quite get that.

[serzh]

Well, never mind, I just understant that it has to be proven that to types does'nt have anything in common. I have some ideas on bidrectional programming, and I need this type of check to be sure that if is bidrectional