Does it seem useful to add a new kwarg to fspec to allow a function spec to provide one or more constraints on or invariants of the function across distinct invocations in order to provide for constraints such as commutativity. I am working on this, but thought good to check if anyone else thinks is useful.
The new kwarg, possibly :alg given that this allows expression of the algebraic properties of the function, would take a map, with key being a naming keyword and value being a predicate (typically needing a let).
Looking somewhat like this for a few binary operators:
(s/fdef add
:args (s/cat :x int? :y int?)
:ret int?
:alg { :comm
(let [f (:f %)
x (-> % args :x)
y (-> % args :x)]
(= ((f x y) (f y x))
:assoc
(let [f (:f %)
x (-> % args :x)
y (-> % args :x)
z (-> % args :x)]
(= (f (f x y) z) (f x (f y z)))
:ident
(let [f (:f %)
x (-> % args :x)]
(= (f x 0) x))})
(s/fdef mul
:args (s/cat :x int? :y int?)
:ret int?
:alg { :comm
(let [f (:f %)
x (-> % args :x)
y (-> % args :x)]
(= ((f x y) (f y x))
:assoc
(let [f (:f %)
x (-> % args :x)
y (-> % args :x)
z (-> % args :x)]
(= (f (f x y) z) (f x (f y z)))
:ident
(let [f (:f %)
x (-> % args :x)]
(= (f x 0) x))
:super
(let [f (:f %)
x (-> % args :x)]
(= (f x 0) 0))})
(s/fdef max
:args (s/cat :x int? :y int?)
:ret int?
:alg { :comm
(let [f (:f %)
x (-> % args :x)
y (-> % args :x)]
(= ((f x y) (f y x))
:assoc
(let [f (:f %)
x (-> % args :x)
y (-> % args :x)
z (-> % args :x)]
(= (f (f x y) z) (f x (f y z)))
:idem
(let [f (:f %)
x (-> % args :x)]
(= (f x x) x)})
:ident, :super and :idem above could obvs be done with :fn, but seems handy to put together once one gets :comm and :assoc in place.
This may give rise to question of how to similarly handle constraints on or invariants of sets of related functions, although probably less commonly useful. However that may suggest that actually this would be better done as separate from the fspec in a separate spec - ?
