are schemas expressive enough for macros?

yes. Similar to s/defn. The argument checks are the same as it, and the return value checks express what the result of the execution will look like, not the result of the macro expansion. That would help when using macros.

> return value checks express what the result of the execution will look like, not the result of the macro expansion. are you describing s/defmacro or s/defn?

s/defmacro ; I assume that

that's cool. I've tried similar things but I want to hear more about your ideas. Do you have an example macro that returns anything other than Any?

(defmacro adding-all [& args]
  `(+ ~@(map inc args)))
;;=> #'argparse.core/adding-all

(macroexpand
 '(adding-all 1 2 3))
;;=> (clojure.core/+ 2 3 4)

(s/defmacro adding-all :- s/Int
  [& args :- [s/Int]]
  `(+ ~@(map inc args)))

How would the result be checked?

That's right. I can't check, but I was assuming I would use it in a static analysis. If this macro is used where s/Str is expected it will be able to produce errors.

would the arguments be unchecked too?

no, I can check,, I see, macro just get symbol instead of its value.

Oh I see. I don't think many macros are this statically known.

most take expressions as arguments too, which would be Any.

Hmm. Might be a little difficult. I'll give it some more thought.

when I tried this I ended up with typing rules. for example for if:

;; Env |- e1 : T1
;; Env |- e2 : T2
;; Env |- e3 : T3
;; --------------------------------
;; Env |- (if e1 e2 e3) : (U T2 T3)

;; Env       |- e1 : T1
;; Env, x:T2 |- e2 : T2
;; --------------------------------
;; Env |- (let [x e1] e2) : T2

are you aware of how spec treats macros?

I see. maybe we should have generic type before this?

yes exactly

here's my experiment for if that returns the then branch (spec)

(s/def ::logical-true (s/and s/any? boolean))
(s/def ::logical-false #{false nil})

;; Env |- e1 : logical-true
;; Env |- e2 : T2
;; --------------------------------
;; Env |- (if e1 e2 e3) : T2
(s/def ::if-true-simple
  (t/all :binder (t/binder
                   :e1 (t/bind-tv :kind (t/prog-spec
                                          :type ::logical-true))
                   :t2 (t/bind-tv :kind t/any-spec)
                   :e2 (t/bind-tv :kind (t/prog-spec
                                          :type (t/tv :t2)))
                   :e3 (t/bind-tv :kind (t/prog-spec)))
         :body
         (t/macro-spec
           :args (s/cat :test (t/tv :e1)
                        :then (t/tv :e2)
                        :else (s/? (t/tv :e3)))
           :prog (t/prog-spec
                   :type (t/tv :t2)))))

Thanks, for clarification. What is the t here?

t is a type (or a schema). but there's a lot going on here, any particular part you'd like to know more about?

I reused the names from the typing rule in the spec, that might help. I can also just explain the whole thing if you'd like.

Sounds good. I'm still a newbie to Clojure, though, so I'll get used to it first. And I'll come back here again next time.