Clojurians Log v2

Hmm, so check-ns-clj fails with (defn foo [t] "abc"), but only after restarting the REPL?

yep

Oh, save the file?

mashing cmd + S does seem to make it work. Intellij saves when you switch tabs or give it that hint

but okay, that makes sense

so it type checks the file on disk, not the state in the repl

exactly. Did you eval the buffer instead of saving to disk?

yes i did. usually with IntelliJ I am not actively thinking about when the files are saved because they "just are"

but is it using the live repl state to do the type checking?

Type collection is live. eg., t/ann and m/=> is gathered from the REPL.

So is this some form of caching?

(how does it know the type when i haven't loaded it in?)

by loading the namespace in the REPL, you've evaluated m/=>. so t/check-ns-clj just retrieves it from malli.

Oh, now I get it.

Type checking works much like evaluation. except it's read -> macroexpand/type check -> eval for each form, left to right.

probably if m/=> occurred after defn it would fail

but in this case I haven't loaded the m/=> line

Here's what happens: 1. you create the tyt namespace. 2. you call t/check-ns-clj 3. now, the type checker basically calls (require 'tyt :reload), except just before evaluating each form, the form is type checked.

so (check-form '(m/=> ..)) is called before (check-form '(defn foo ..)), so the malli schema is registered just in time.

ooooh okay

does it still work if you switch the forms?

it does not fail with the error if i switch the forms

sideways question: Does this mean that typedclojure couldn't be embedded in cljkondo?

ah, so what's happening there is that if there's no expected type available, it will check as [Any -> Any] . and it succeeds.

(or be used in a similar way)

clj-kondo is very different, and I don't know if it's possible to combine the two. Typed Clojure relies on being able to really macroexpand your code, which is exactly what clj-kondo cannot.

it's more like eastwood.

Interestingly, clj-kondo and Typed Clojure are converging in other ways, since we're both making extensible rules for macros that we don't recognize. So maybe, Typed Clojure will know so many macros eventually that we can think of a graalvm offline version. But, I still don't really understand why you'd want that over importing a jar.

The flexibility you get is perfectly demonstrated by the malli integration you're playing with. You'd need extra steps to export the malli to a clj-kondo config to do this.

there is already that for malli

and it goes to the "clj-kondo type declaration" format

yes, that's what made me realize the pros/cons of each approach actually.

most of the motivation is (i think) around the editor experience, since requiring a running repl for feedback has been a barrier

I think the folks that make better use of it could make a more convincing pitch though

so "hooks" and the pseudo macro-expansion they provide wouldn't be enough for typed clojure?

IMO clj-kondo is perfect the way it is, I'm just commenting on what you'd lose by making Typed Clojure move to graalvm.

Theoretically it's enough.

But there are so few rules atm that we have to wait before seriously trying.

this is the no.1 question I get in the last few years 🙂 but Typed Clojure is 11 years old at this point, it's a totally different ball game on graalvm.

The best I could hope to contribute realistically is maybe help borkdude port some of Typed Clojure's type system features to clj-kondo.

at least in the short term.

It's about the same complexity as porting eastwood to graalvm. I haven't seen that suggested anywhere, which makes me think there are some misconceptions about Typed Clojure floating around 🙂

Yes, perhaps, but you trying it out gives me an incentive to finish it so thank you. 🙂

I bet I can knock out a good chunk of support by just copying the malli.clj-kondo namespace.

I would really like to know what the real challenges are in practice (you know, asides from :map not being implemented xD).

I have a feeling we'll need a way to embed malli syntax into Typed Clojure syntax. Say you have a big map defined in malli, and you need to override a type annotation, you'd want to be able to refer to the big malli map without rewriting the whole thing in typed clojure

(def MyMassiveMalliType [:cat ... ...])
(t/ann foo [(Malli MyMassiveMalliType) -> ...])

Basic :map works

is there a way to see what type was inferred based on a schema?

yeah, but it uses the old namespace. Try (clojure.core.typed/cf foo)

should be implicitly loaded by typed.clojure

is check-ns-clj what i should run to type check an entire project?

and does type checking extend into local/root dependencies?

(I'm gonna take the plunge and try to type check the monorepo)

check-ns-clj sources files in the same way as require. It just needs to be on the classpath in the normal place.

okay that went pretty quick - it skips checking namespaces that don't depend on clojure.core.typed

so i guess we would add a dummy require to turn it on ns by ns

(->> (all-ns)
     (filter #(string/starts-with? (str %) "lumanu"))
     (map (comp symbol str))
     (t/check-ns-clj))

Yeah that part is in flux. Before, that was important because check-ns checked all dependencies transitively. This is no longer the case, but the requirement is still there.

I was about to lift that requirement actually.

Yeah, the workflow is still not obvious to me after all these years. I just do

(deftest type-checking
  (is (check-ns-clj '[ns1 ns2 n3])))

I'm really leaning into a single file being the unit of type checking these days. Not a project, or a set of ns dependencies. Mainly for performance reasons.

One of the reasons users stopped using core.typed was that it forced you to check dependencies before doing anything else. Which was an agonizingly long time. This is no longer the case.

(ns ^:typecheck something.name)

(deftest type-check
  (is (->> (all-ns)
           (filter #(string/starts-with? (str %) "lumanu"))
           (filter #(:typecheck (meta %)))
           (t/check-ns-clj)))

ha nice

alright I gotta go. thanks @emccue, lmk how your experiments go!