schema

conao3 2024-08-10T19:01:05.815639Z

I found there is no schema.core/defmacro . Is there anyone else who wants it?

2024-08-10T19:35:10.936579Z

are schemas expressive enough for macros?

conao3 2024-08-11T00:23:12.993189Z

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.

2024-08-11T02:22:20.568839Z

> 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?

conao3 2024-08-11T02:23:58.201609Z

s/defmacro ; I assume that

2024-08-11T02:27:07.836879Z

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?

conao3 2024-08-11T02:32:41.764659Z

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

(macroexpand
 '(adding-all 1 2 3))
;;=> (clojure.core/+ 2 3 4)
This is an illustrative example, but suppose we define such a macro. And this macro could be typed thus.
(s/defmacro adding-all :- s/Int
  [& args :- [s/Int]]
  `(+ ~@(map inc args)))

2024-08-11T02:33:21.250139Z

How would the result be checked?

conao3 2024-08-11T02:35:05.136549Z

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.

2024-08-11T02:35:42.294499Z

would the arguments be unchecked too?

conao3 2024-08-11T02:36:55.253549Z

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

2024-08-11T02:38:54.063419Z

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

2024-08-11T02:39:39.410549Z

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

conao3 2024-08-11T02:40:15.925909Z

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

2024-08-11T02:41:50.527739Z

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)
and let
;; Env       |- e1 : T1
;; Env, x:T2 |- e2 : T2
;; --------------------------------
;; Env |- (let [x e1] e2) : T2

2024-08-11T02:42:14.838529Z

are you aware of how spec treats macros?

conao3 2024-08-11T02:45:21.948999Z

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

2024-08-11T02:48:07.730749Z

yes exactly

👍 1
2024-08-11T02:49:17.115459Z

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

conao3 2024-08-11T02:50:53.621709Z

Thanks, for clarification. What is the t here?

2024-08-11T02:52:27.011299Z

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?

2024-08-11T02:55:12.747409Z

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.

conao3 2024-08-11T02:57:14.506439Z

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.

👍 1