Clojurians Log v2

More noob noise for you if you're interested: 1. Are you suggesting to call cljs.c/type from inside core.typed on forms statically? Doesn't that only work "at runtime", as that's when the object whose constructor you're interested in exists?

What I'm speculating about is how to type check something like this:

(def my-specially-tagged-val ^{:type ::my-specially-tagged-val} {:foo 1 :bar 2})
(defn process-thing [thing :- t/Any]
  (case (type thing)
    ::my-specially-tagged-val (+ (:foo thing) (:bar thing))))

How can we know that (:foo thing) is an int when we type check (+ ...)?

Idea: Have a registry that maps :type values to their types.

(t/register-metadata-type ::my-specially-tagged-val '{:foo t/Int, :bar t/Int})

And once we learn, for example (= ::my-specially-tagged-val (type thing)), we update the type environment with thing :- '{:foo t/Int, :bar t/Int}.

Typed Clojure uses an environment of propositions that contain knowledge of the current lexical scope. You can see propositions encoded in the types of predicate, eg., pos-int? learns the 0th arg is an int if it returns true: https://github.com/typedclojure/typedclojure/blob/main/typed/lib.clojure/src/typed/ann/clojure.cljc#L2037-L2044

You can extend this propositional logic to reason about "paths" into local variables. Currently, we can reason about the "Class" of a variable, see the type of clojure.core/class. https://github.com/typedclojure/typedclojure/blob/main/typed/lib.clojure/src/typed/ann/clojure.cljc#L1760-L1762

That enables inferring cool stuff like this:

(defn foo [a :- t/Any]
  (when (= Number (class a))
    (inc a)))

Now the idea here is to add a Type path element, so we can reason about clojure.core/type in the same way.

cc/type would look something like [t/Any -> t/Any :object {:id 0 :path [Type]}]

Unrelated to the polymorphic ts contextual typing stuff, I'm sure you've seen https://github.com/borkdude/speculative, and I wonder if your spec->types endeavor could help you bootstrap the community types repo thing

Yeah it would be interesting to know how useful raw specs are for type checking. For CRUD-style things, it's probably perfectly adequate.

Unfortunately that's exactly the kind of thing that's usually closed source, so it's harder to experiment.

something like https://github.com/lilactown/cascade or https://github.com/lilactown/pyramid might be fun to try and type

that being said, I did my time in the OCaml and TypeScript mines and came out a better programmer and not excited about writing more types for my libs

oh boy, cascade would be a good stress test of how first-class the typings of core ops are.

I'm guessing it would fail miserably 🙂

my experience typing similar libraries in ts like ramda makes me believe it's just a hard problem 😄

Hahaha speaking of typing rambda you guys will fucking go nuts over this: https://www.freecodecamp.org/news/typescript-curry-ramda-types-f747e99744ab/ Loops in the type annotation syntax??? Bananas --- Anyways, I love typing libraries so much, no clue why, so I'm down to type either @lilactown, though IDK what Cascade is

Nice, conditional union types has always had me jealous. I almost included something like it for my PhD thesis IIRC because I wanted the expressivity.

I'm currently playing around with a nutty idea to solve how to check (map (fn [x :- InferThisTypeAutomatically] ..) [..]). I think Flow lang can do this. I don't think TS can, I believe it infers x as any.

Looks like TS added support for this https://www.typescriptlang.org/docs/handbook/2/functions.html#inference

apparently called contextual typing https://www.typescriptlang.org/docs/handbook/type-inference.html#contextual-typing

An old spec detailing when contextual typing happens https://github.com/microsoft/TypeScript/blob/main/doc/spec-ARCHIVED.md#423-contextually-typed-expressions

In a typed function call, argument expressions are contextually typed by their corresponding parameter types. ? Seems vague about polymorphic function calls AFAICT.

If anyone knows where the code is that implements this I'd be interested.

Forgive my ignorance, what is it about graal that makes it so that it needs special consideration for core-typed? What does core-typed do that isn't "regular clojure 'user-space'-y code"? btw I'm very invested in core-typed (or until, as I joke, I stop working at a clj startup lol) in a personal agenda sense but also curious about it - and I'd love to contribute in some way or other someday, if that's something you're into

Good question, the problem is that clojure on graalvm cannot perform macroexpansion.

This (being able to macroexpand forms) was very fundamental to how Typed Clojure worked in its original design. In the last few years, we've added custom rules for particular macros.

So now the door is partially open to graalvm...if we can write enough rules!

@rayatrahman9 in terms of contributing, it might be fun and informative to try and type check one of your favourite libraries or programs (~500 LOC). As you go through, through it, leave yourself a bunch of comments about what sucks. Then you have a list of relevant features to add to Typed Clojure! That's exactly what I'm doing now with malli.

if you pick a popular library, we can take the annotations and rules you generate from the exercise and make that itself a contribution to Typed Clojure.

What do you think?

1. 😮 I did not know that about graalvm. What's the best resource to learn more about that? I'm new AF to clj in general, but it does seem that macros are a pretty big part of it, no? Curious about how that is developing. I was so floored when I first read about graal like years ago, been out of the loop! 2. I'm very open to your proposal, however, I'm probably the worst person to ask : a. I started clj programming like 5 months ago after joining my current org b. And primarily am working so far in the UI stack in cljs, which I understand is quite far from clj as far as progress/integration with most tooling goes, including typed , right? c. That being said, I'm very comfortable throwing my manager @lilactown under the bus here, i. as (I like to believe) he wants nothing more than to make me happy (with cljs tooling), ii. and is far more experienced 1. in the clj/s OSS community a. and the experiences with/expectations for/frustrations with them that developers have, 2. but also from his own libraries, like #helix, a. which I'm sure I can irritate him enough to eventually fully type annotate 3. and has also had experience with the gradually-typed static type annotation world of TS 3. Are you familiar with Typescript's DefinitelyTyped repository? a. If not, it's a community repo with auto build system set up by M$ for people to share hand-written type annotations for popular libraries whose maintainers don't want to or can't provide them themselves. b. It's an imperfect solution to an imperfect problem, but provides a halfway-decent opt-in way to essentially let people who need them obtain and contribute annotations Regarding making the annotations and rules generated from your proposed exercise contributions to Type Clojure, do you mean something like (3) above?

1. I don't know a lot about Graalvm except that babashka and clj-kondo use it, and they are both excellent tools. I donate to @borkdude so I don't have to know too much about graavlm xD 2. FYI Typed Clojure is both older than clj-kondo/malli/spec/schema and both less mature and more experimental. It effectively has no users AFAIK. Just to say, it might be a while, if ever, if it can be applied to your job. That said, I think it's extremely rewarding to work on, and it's really making strides lately. 3. Yes, my plan is just to shove annotations into the monorepo with Typed Clojure so I have everything in the same place. I'm basically proposing that you write annotations like you would in DefinitelyTyped for library "X", except you also call t/check-ns-clj on the actual library with those annotations (actually, not sure if this is the usual practice with DefinitelyTyped). Now you have annotations that have been self-checked, and some experience under your belt as to the rough edges to Typed Clojure and some idea of which things you think would be the biggest improvements.

How do I get the current ns, and what's the node->sexpr function called?

I'll add the current ns now

The node->sexpr function is called rewrite-clj.node/sexpr or you can use the internal version: clj-kondo.impl.rewrite-clj.node/sexpr

4d7bc522b512d773df4a395b6c515a84abb53bf3

Ok that looks good, thanks! wish me luck ;)

luck :)

ah, now I have a potential list of type errors I want to pass back to clj-kondo to report on.

You can use clj-kondo.impl.findings/reg-finding! for this

(at this phase, when this goes public, we need to make everything impl a bit more neat)

Hmm, right now this won't work for you

Let me add something

Commit:

fe622fe37ff93c2edfdc22c30c4ac65bdcb9ef20

row col end-row end-col type message

And looky here, clj-kondo found a missing required key ;)

Gotta love that!

Could I get an atom that I can store local state in? Stuff like thread bindings for the current ns.

clj-kondo already has that local state

can't it just give you that?

oh thread bindings?

I guess that atom can just live in a closed over value of your hook?

Yes, that's what I was thinking. Either let me set my own state at the top level (say call my hook with zero args and assoc the result to :state) or give me an atom.

The former is probably most flexible.

I was thinking a few steps ahead -- I could close over the hook myself (and I'm doing that for the moment), but if the hook was configured in a .edn configuration somewhere, you'd just want to provide a symbol naming the hook I think.

The node contains the row/col as metadata

Thanks!

So you need to grab that before you convert it

Hmm how do I do that recursively?

That's a good question. In general you can't attach metadata to some values like numbers, etc so converting to a sexpr is lossy anyway. But you might be able to postwalk the thing at make a best attempt. Or only report the top level location for now. It's a tricky problem. This is why clj-kondo :analyze-call hooks operate directly on nodes so you can return more accurate locations to your messages

There's also a :macroexpand hook which operates on the s-expr but moves the messages to the outer node location

I'll try postwalk. I just want the equivalent to the tools.reader output.

This could maybe be done for the :macroexpand hook too to get better locations. The challenge there is also that the transformed s-expr is converted back into a rewrite-clj node

The Clojure reader has imo a good trade-off to only attach locations to seqs

Also I think another piece that I can't access is the current file name for *file*.

ok, we can pass that too

but should not be relevant probably, as the reg-finding! already takes care of this

PRs welcome against the clj-kondo core-typed-hook branch. I'm done programming for today :)

You can probably experiment with this in a local checkout.

sounds good, thanks very much!

Just one more thought: if you're more interested in getting the sexprs exactly like tools.reader gives them, maybe it makes more sense to place the hook elsewhere so you can parse the file yourself. I'm not exactly sure where you want to go with this hook.

Yeah I think you're right. Not exactly sure either, my eventual goal is to have something like clj-kondo native but running Typed Clojure. I was hoping this was a good first step, to share as much machinery as I can with clj-kondo. We'll see.

Makes sense, let's keep exploring

Hehe yes. I looked for a better place for the hook, but I ended up so far up the stack it seemed a little pointless 🙂

At the bottom of analyzer you have analyze-input which has the string of the file

you could just do your normal tools reader thing there

if the rewrite conversion doesn't pan out

but we could also make improvements to the rewrite-clj -> sexpr stuff too

Ah, I missed that. This is making me step back to what I think I want to reuse from clj-kondo: • symbol->var resolution, • info about Java classes/methods/fields • participate in existing editor feedback mechanisms

right, then probably top level exprs makes sense

Hmm let's say we wanted feedback from both clj-kondo and typed clojure, but as soon as it's ready. I'm guessing if both were computed by the same run! then both would have to finish before feedback right?

OK, we can change it to only pass top level forms, or pass a :top-level key so you can filter

I'll try the latter, thanks!

There's already a top-level thing floating around which you probably only need to pass to the hook

hmm do you mean the :top-level? in the ctx? I don't think the hook can access it

not yet no, but if we pass it, it can