I haven't implemented the generators yet for this, but another interesting example:

(is (= ["should be distinct: 3 provided 2 times"
          "should be sorted: index 1 has 3 but expected 2"]
         (me/humanize (m/explain
                        [:sequential {:sorted true
                                      :distinct true} :any]
                        [1 3 3 2]))))

To give some idea of the improved generator expressivity, this is another way of writing the schema in the OP:

(is (= 740 (mg/generate [:int {:and [[:not [:<= 739]]
                                       [:not [:>= 741]]]}])))

How's that different from min and max properties?

For other types that's pretty neat

superficially, min/max is inclusive (<=/>=). But on a fundamental level, this is no different than properties. This is a propositional logic where the atomic propositions are things like min/max/sorted/distinct/</>.

It would be trivial to add </> support in the same way as min/max, but I think this abstracts over that entire idea.

Which means it has algebra, neat

I thought you would enjoy 🙂

btw, if you're doing strings, it's worth it to add some caregory predicates, such as alpha, alnum, numeric, etc

oh yeah, and there's already generators for that. that would work nicely.

Exactly, and it can be implemented efficiently using https://docs.oracle.com/javase/8/docs/api/java/lang/Character.html predicates

Then just for fun you could add :re and we could get rid of regex schemas which aren't comparable because java regexes don't have value semantics (boo)

oh, and test.chuck has a re string generator.

is there a generator for :re?

It uses test.chuck if it's on the class path

And sorry to make more work for you but don't forget time schemas

elaborate your ideas

I want to really test this abstraction.

I mean these, I worked really hard on that sh*t would be a shame if they don't get to enjoy the new constraints features https://github.com/metosin/malli/blob/master/src/malli/experimental/time.cljc

ah, and which constraints are you thinking?

like before/after?

Yes. They already support min and max, so mostly make sure they aren't left out of the party

Nice. are min/max inclusive here?

I think so

Check line 30

and there's no generators currently hooked up?

There are. Getting them right was a pain

Here https://github.com/metosin/malli/blob/master/src/malli/experimental/time/generator.cljc

nice. yes I've been there.

This propositional logic might get us out of :fn guard hell. pretending we don't have nat-int? for a second, this could be the schema for nth:

[:=> {:refine [v i]
      [:and
       [:<= 0 i]
       [:< i [:count v]]]}
 [:cat :vector :int]
 :any]

I have no idea what implications that has but just an idea that popped up.

This is starting to look like a where clause in datomic 🙂

Though it loses some information, the return type isn't any, it's a function of the vector index

right, but I'm still working on polymorphic schemas 🙂

If I'm unabashedly wishfully thinking:

(m/all [x]
       [:=> {:and (m/refine [v i]
                            [:and
                             [:<= 0 i]
                             [:< i [:count v]]])}
        [:cat [:vector x] :int]
        x])

That doesn't handle a heterogeneous vector, right? Still, I'd buy it

might be more like:

(m/all [x :*, n :- nat-int?]
       [:=> 
        [:cat [:tuple [:.. x]] [:= n]]
        [:..nth x n]])

where [:..] is regex that expands at "instantiation time" of the all.

[:inst ::nth [:cat :a :b :c] 2] =>

[:=> [:cat [:tuple :a :b :c] [:= 2]] :c]

and the [:nth.. schema implicitly relates x and n?

there's a bunch of details I'm working out to get something like this, but I think we can look to type theory for inspiration on how to create an expressive specification language.

the main caveat is that you can't really instrument a polymorphic fn, so you'd need to compile a monomorphic one for instrumentation, and just use the polymorphic one for generation. Still working on how to do that. like, one detail here is that if you instantiate n to nat-int to generate the most general version of the schema for instrumentation purposes, you get [:= nat-int] as the second arg. Obviously not what you want. Perhaps n is really a spec here instead of a nat. Stuff like that.

Would be curious to know what this would look like starting from your observation that everything resembles datalog, but I don't know how to create verification system from that foundation so that's for someone else to explore 🙂

my formal training in type theory is leaking through exposing my biases/limitations. it's my one trick.

fleshed it out a bit, I think this should check length bounds for instrumentation and additionally generators of this schema will know how to generate good returns.

(m/all [x :*, n :< nat-int?]
       [:=> {:and (m/refine {{:keys [v i]} :args}
                            [:< i [:count v]])}
        [:catn
         [:v [:schema x]]
         [:i n]]
        [:..nth x n]])

[:inst ::nth [:cat :a :b :c] [:= 2]]
;=> [:=> {:and ..} [:cat [:schema [:cat :a :b :c]] [:= 2]] :c]
[:inst ::nth [:* :int] nat-int?]
;=> [:=> {:and ..} [:cat [:schema [:* :int]] nat-int?] :int]
;; for instrumentation:
[:inst ::nth [:* :any] nat-int?]
;=> [:=> {:and ..} [:cat [:schema [:* :any]] nat-int?] :any]

The trick is that [:..nth [:* :int] nat-int?] => :int and [:..nth [:cat :a :b] [:= 0]] => :a. And probably [:..nth [:cat :a :b] nat-int?]=>[:or :a :b].

Why aren't you speccing it like a map? I guess heterogeneous and homogeneous vectors could be specced differently

this was my only idea, what were you thinking?

Too tired to be coherent, but just however you'll describe a map if the vector is heterogeneous. A homogeneous vector could be defined like you have now. The definitions should overlap for homogeneous vector, too

I like where this is heading. It is much cleaner to have a :map with constraints in the properties versus having to nest it inside :and or :fn etc. The symmetry with the actual shape is maintained.

For instance, I have been working on some visualizations of schemas and it requires walking the schema tree and removing all the nodes that are really constraints since the`:maps` are the bits I am interested in.

Suggestion: use the format property like json schema does. Thinking forward to things like email, IP, etc

@UK0810AQ2 are you referring to the :format field in malli.json-schema? I don't follow.

For strings, instead of :alpha true, :format :alpha

A single key to look at

It's just sugar for an atomic proposition: {prop true} => {:and [[prop]]}. {:alpha true :numeric true :max 10} => {:and [[:alpha] [:numeric] [:max 10]]}

You can even do {:gen/alpha true, :alphanumeric true} to generate alpha in generators and alphanumeric in validators.

though I haven't implemented it, that's how I've set up the syntax.

I've only done the validator side atm. there [:gen/alpha] expands to the top proposition [:any] so it usually has no effect on the proposition during validation.

to give you an idea, these are the propositions I've supported for :string alone, along with their :gen version. they all use the {prop true} syntax:

:max :min :alphanumeric :non-alphanumeric :letters :non-letters :numeric :non-numeric :alpha :non-alpha :sorted :distinct :palindrome :trim :triml :trimr :trim-newline :blank :non-blank :escapes :includes

it's easily extensible

well, {:includes "foo"} and

{:escapes {\- "_MINUS_"}}

and min/max of course.

What threw me in a loop is that (and alpha numeric) is an empty set

The sugar is confusion imo

{:max 10 :or [[:alpha] [:numeric]]} rather

{:distinct true :sorted true :max 10} is a better example of a conjunction.

The rule is the same as always: {:min 10 :max 12} is a conjunction. we just have more atomic propositions now.

Yes, but the code for handling them would be annoying

{:format [:and :alpha :distinct]} is clearer for the reader and simpler to implement imo

It's uniform and simple to compile to a bunch of predicates

It's a dozen lines to desugar in a fully extensible way. Plus I want to save the keyword syntax for [:contains K] sugar like s/keys.

(defn -constraint-from-properties [properties constraint-opts options]
  (let [{:keys [flat-property-keys nested-property-keys]} (->constraint-opts constraint-opts)]
    (when-some [cs (-> []
                       (into (keep #(when-some [[_ v] (find properties %)]
                                      (into [%] v)))
                             nested-property-keys)
                       (into (keep #(when-some [[_ v] (find properties %)]
                                      (conj [%] v)))
                             flat-property-keys)
                       not-empty)]
      (if (= 1 (count cs))
        (first cs)
        (into [:and] cs)))))

[:and :x :y] instead of [:and [:contains :x] [:contains :y]].

At least for schemas that support contains?. Haven't decided whether to allow unwrapped keywords in other schemas yet.

Let's say I do allow unwrapped keyword in say :string . I think {:and [:alpha :distinct]} is clearer than {:format [:and :alpha :distinct]}.

mainly because "format" isn't a proposition.

It's unclear how far this concept can go, but I want the user to think property == proposition. And property map == conjunction.

yeah, format isn't a proposition, it's more like a predicate

earlier I renamed :and to things like :keyset :keys . I think once I saw the abstraction of everything is a proposition, the current philosophy started to make sense to me.

every single schema can support :and , and it will make sense.

I think :format for :string is similar to my thinking of :keyset constraints for :map. We can abstract over the concept of "thing is true for schema".

my thinking about it is tainted by how json schema does it

yeah and my thinking about properties was tainted by min/max. It was tailored for each schema in different ways and didn't seem like a coherent abstraction beyond syntax.

but that was my thinking too: a property is something tied to the schema type.

until like yesterday. so it's a new idea.

here's a good existing example of using true.

(mg/generate
  [:double {:gen/infinite? true, :gen/NaN? true}]
  {:seed 1})