Fork me on GitHub
#core-typed
<
2022-04-03
>
ambrosebs15:04:26

BTW I had an idea on how to support inference via cljs.core/type in the CLJS checker. How important is this function in CLJS? and are namespaced keywords usually used to identify a type?

rayat23:04:07

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?

ambrosebs23:04:22

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

ambrosebs23:04:53

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

1
ambrosebs23:04:23

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

ambrosebs23:04:01

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}.

ambrosebs00:04:41

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

today-i-learned 1
ambrosebs00:04:57

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

ambrosebs00:04:02

That enables inferring cool stuff like this:

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

ambrosebs00:04:48

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

ambrosebs00:04:28

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

1
ambrosebs15:04:25

Also thinking about how Typed Clojure might integrate with clj-kondo (JVM). If the checker can be hooked in every time clj-kondo thinks an expression needs linting, I think that should work.

šŸ˜® 1
ambrosebs15:04:01

that's probably the first step to thinking about Graalvm support--integrate via JVM first.

rayat23:04:36

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

ambrosebs23:04:41

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

ambrosebs23:04:21

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.

ambrosebs23:04:48

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

ambrosebs01:04:41

@U037TPXKBGS 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.

ambrosebs01:04:34

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.

ambrosebs01:04:55

What do you think?

rayat01:04:20

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

ambrosebs01:04:39

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.

šŸ˜† 1
1
lilactown16:04:13

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

šŸ‘ 1
ambrosebs17:04:47

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

ambrosebs17:04:11

I'm guessing it would fail miserably šŸ™‚

šŸ˜„ 1
lilactown17:04:22

my experience typing similar libraries in ts like ramda makes me believe it's just a hard problem šŸ˜„

rayat18:04:44

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 @U4YGF4NGM, though IDK what Cascade is

ambrosebs21:04:28

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.

ā¤ļø 1
ambrosebs22:04:57

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.

ambrosebs22:04:45

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

ambrosebs22:04:36

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

1
rayat21:04:27

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

šŸ‘ 1
ambrosebs23:04:56

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

ambrosebs23:04:47

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

borkdude15:04:03

@ambrosebs welcome to elaborate - I can help with both clj-kondo and graalvm

ā¤ļø 1
borkdude15:04:42

is core typed a static-analysis based type checker or a run-time checker?

ambrosebs15:04:55

static, like eastwood mostly

borkdude15:04:18

but it does expand macros etc first right?

ambrosebs15:04:00

Kind of, it's starting to look more like clj-kondo now. You can make custom rules for macros. But where clj-kondo gives up if it doesn't recognize the macro, Typed Clojure will expand.

ambrosebs15:04:20

So theoretically with enough rules, it should be compatible with graalvm.

borkdude15:04:30

clj-kondo has hooks to expand any macro, if you configure it correctly

ambrosebs15:04:53

Ah ok, news to me! It can use the definition of the macro?

borkdude15:04:45

Not exactly but you can often copy the macro definition literally to the config

ambrosebs15:04:31

Oh ok, we're talking about the same thing. Typed Clojure has hooks in the same way. But it also expands the macro from its definition if there is no hook.

ambrosebs15:04:39

Obviously not possible on graalvm

1
borkdude15:04:47

yes, that's why I was asking :)

borkdude15:04:23

but potentially that can be disabled for native compilation

borkdude15:04:31

or it could use SCI in native-mode, to try to eval

ambrosebs15:04:35

Yes. My thoughts are, let's try and integrate with clj-kondo JVM first. Try and teach clj-kondo about what Typed Clojure thinks a cache should contain (ie., when to relint a form/file). And hook into clj-kondo's linting at the form-level. ie., if clj-kondo thinks a form needs linting, it also passes it to Typed Clojure.

ambrosebs15:04:08

The former is not super important first up.

ambrosebs15:04:20

Cache integration can wait.

borkdude15:04:52

What would be interesting for clj-kondo is also directly be able to use typed clojure annotations for its own (super simple) type checker

ambrosebs15:04:10

I agree but there are are major perf implications.

borkdude15:04:33

E.g. it can lint the following: (assoc (keyword "dude") 1 2 ) as invalid, but it doesn't know the type of everything

ambrosebs15:04:34

I read through your design goals, it didn't seem to fit with Typed Clojure

ambrosebs15:04:05

I had exactly the same thought as you, I'm still mulling it over. Ignore my negative reaction for now, thinking out loud xD

borkdude15:04:15

@ambrosebs I've got a thing for clojure.spec here (super spartan, but conceptually it works): https://github.com/clj-kondo/inspector You run clojure.spec at runtime, it emits some type info on disk and clj-kondo can start using it for static analysis

1
borkdude15:04:26

A similar thing exists for malli

ambrosebs15:04:28

Yes, I saw the same thing in malli a few days ago. I was about to build one for Typed Clojure until I realized there's a large difference in expressibility. Typed Clojure types are very expressive, it's not obvious how to translate.

borkdude15:04:41

I wish there was one annotation format to rule them all, so then clj-kondo could just support it statically maybe

borkdude15:04:13

yes, you have to convert from super expressive to a lossy representation, but the cool thing is that you will get some linting for free, even though it's not perfect

ambrosebs15:04:40

It's an alien language.

borkdude15:04:12

don't worry about assoc, clj-kondo already has built-in types for that :)

ambrosebs15:04:25

hehe, ok what about polymorphism? map/identity?

borkdude15:04:39

not available right now

borkdude15:04:10

all that clj-kondo knows about map is that you get back a sequence

borkdude15:04:39

it's at the other end of the type spectrum: super mundane, but sometimes it catches a silly thing :)

ambrosebs15:04:58

Yes, and that also plays into your perf goals (lint per character).

borkdude15:04:29

not sure if I understand that right

ambrosebs15:04:15

Type checking with polymorphic types is expensive. If you support polymorphic types in clj-kondo, you'll need to navigate that problem.

ambrosebs15:04:25

If you want quick response times from the linter.

ambrosebs15:04:42

So that's why I'm thinking, let's keep clj-kondo's type system. clj-kondo + Typed Clojure is almost another use case, it's going to be very slow.

borkdude15:04:32

ok. if you need any help with anything clj-kondo / graalvm, just poke me.

ambrosebs15:04:23

@borkdude is there a way to hook into clj-kondo's linting on a form-level (JVM, not graalvm)? Say, I just want to add an extra log printing the current form, or call my own linter on the form at the same time as clj-kondo. how might I do that?

borkdude15:04:08

@ambrosebs There is no generic hook for that, but for experimentation, we could add that in a branch and then see if that's useful

ambrosebs15:04:25

Yes please. All I need is the current namespace and the form.

borkdude15:04:06

clj-kondo lints on a file-by-file basis, so you would get every form from file. clj-kondo walks from in recursive descend fashion

borkdude15:04:48

forms are rewrite-clj nodes, but there are ways to coerce those into s-expressions

ambrosebs15:04:06

a rewrite-clj node sounds perfect.

borkdude15:04:31

clj-kondo runs with a fork of rewrite-clj: the nodes are the same, but all the whitespace has already been erased

šŸ‘ 1
ambrosebs15:04:44

Oh, is this pre or post reader conditional expansion? I might also need the current platform. Or, just separate hooks for clj/cljs.

ambrosebs15:04:17

Ok cool. Still need the platform to pick the right annotations.

borkdude15:04:24

yeah that's available

borkdude15:04:33

let's see where to best put this hook

šŸ˜ 1
borkdude15:04:07

OK, try commit 7c6a60fd1b0c3b168e5982afedbfa41c16b90519:

user=> (with-in-str "(+ 1 2 3)" (clj-kondo/run! {:lint ["-"] :core-typed-hook prn}))
{:node <list: (+ 1 2 3)>, :lang :clj}
{:node <token: 1>, :lang :clj}
{:node <token: 2>, :lang :clj}
{:node <token: 3>, :lang :clj}

šŸ‘ 1
ambrosebs15:04:59

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

borkdude15:04:29

I'll add the current ns now

šŸ‘ 1
borkdude15:04:59

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

šŸ‘ 1
borkdude15:04:59

4d7bc522b512d773df4a395b6c515a84abb53bf3

ambrosebs15:04:30

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

ambrosebs16:04:31

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

borkdude16:04:32

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

šŸ‘ 1
borkdude16:04:55

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

borkdude16:04:31

Hmm, right now this won't work for you

borkdude16:04:37

Let me add something

borkdude16:04:14

Commit:

fe622fe37ff93c2edfdc22c30c4ac65bdcb9ef20
There is a :reg-finding! key that contains a function that should be called with a map with keys:
row col end-row end-col type message
The location keys are on the metadata of the node. The :type should be configured in .clj-kondo/config.edn and contain a :level

borkdude16:04:02

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

ambrosebs16:04:29

Gotta love that!

ambrosebs16:04:14

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

borkdude16:04:54

clj-kondo already has that local state

borkdude16:04:04

can't it just give you that?

borkdude16:04:22

oh thread bindings?

borkdude16:04:05

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

ambrosebs17:04:28

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.

ambrosebs17:04:29

The former is probably most flexible.

ambrosebs17:04:23

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.

ambrosebs18:04:08

@borkdude do I need to register a new :type for reg-finding! to show up in the :findings entry?

borkdude18:04:42

yes, it needs to be in your config.edn

borkdude18:04:47

configured with a :level

šŸ‘ 1
ambrosebs20:04:40

@borkdude how do I get the rewrite-clj sexpr with line/col metadata? Using clj-kondo.impl.rewrite-clj.node/sexpr seems to give nil metadata.

borkdude20:04:12

The node contains the row/col as metadata

borkdude20:04:36

So you need to grab that before you convert it

ambrosebs20:04:14

Hmm how do I do that recursively?

borkdude20:04:39

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

borkdude20:04:20

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

ambrosebs20:04:52

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

borkdude20:04:08

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

borkdude20:04:40

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

šŸ‘ 1
ambrosebs20:04:33

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

borkdude20:04:54

ok, we can pass that too

šŸ‘ 1
borkdude20:04:10

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

borkdude20:04:58

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

borkdude20:04:10

You can probably experiment with this in a local checkout.

ambrosebs20:04:33

sounds good, thanks very much!

borkdude21:04:03

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.

ambrosebs22:04:02

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.

borkdude22:04:49

Makes sense, let's keep exploring

šŸ‘ 1
ambrosebs22:04:27

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 šŸ™‚

borkdude22:04:50

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

borkdude22:04:07

you could just do your normal tools reader thing there

borkdude22:04:25

if the rewrite conversion doesn't pan out

borkdude22:04:59

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

ambrosebs22:04:42

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

borkdude22:04:58

right, then probably top level exprs makes sense

ambrosebs22:04:40

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?

ambrosebs20:04:02

@borkdude I think the hook needs to be a little higher in the analyzer stack, Typed Clojure just needs the top-level forms, but where the hook is now seems pass the checker all the subforms too.

borkdude20:04:02

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

ambrosebs20:04:42

I'll try the latter, thanks!

borkdude20:04:15

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

ambrosebs20:04:08

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

borkdude20:04:20

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

šŸ‘ 1