Isn't it close to type inference in terms of implementation and partial application?

Hmm well it takes and receives a mostly tools.analyzer format. If any compilers used that format it could be compatible.

It would be pretty easy to convert to a tools.analyzer version. There's just one extra op for an unexpanded form--you'd just expand it into the normal ops.

As to whether Typed Clojure's been designed that way, no. I've intentionally left evaluation of forms untouched to fulfill the promise of a truly optional type system.

Most of the inlining logic that Typed Clojure does never makes it way back to the AST.

It just passes things around in its type environment.

It actually leaves a lot of breathing room in terms of implementation. I can think a bit more out of the box. Kind of interesting too when you think about proving type soundness. Usually you have a source -> target lang translation, and prove the type system compiles from one to the other. That's not really the full story on some of the things I want to do with Typed Clojure.

I mean, I'm sure most type system impls fudge the details in practice compared to papers. Just something we realized a few years ago.

That we're sort of beating around the bush trying to make a source -> target language to prove soundness for a symbolic analysis idea.

Writing an inline pass on tools analyzer isn't hard, I did it myself. Same for constant propagation. The harder parts are: Partial application Escaped closures

Ah ok. Inlining passes don't really make sense in a lot of cases for Typed Clojure. e.g., some functions are checked multiple times, how to combine results?

There's literature in the intersection type community but I haven't used it in the impl.

It's not obvious to me how to combine Typed Clojure with a compiler and get a non-negligible improvement over just the compiler.

One thing comes to mind, dispatch to protocol or interface implementation at compile time over run time

Yes true. The attitude I've been taking is that's something that Typed Clojure could tell the user to annotate in their programs. Like Racket's optimization coach.

It's just so much extra baggage and complexity for a couple of implicit type hints.

But I was thinking more in line of if there are some internals which could be used even for untyped inline passes

Where type checking can be used to ensure correctness

No nothing like that. In terms of manipulating the AST, Typed Clojure does almost literally nothing.

The day I manage to properly inline get-in without ad-hoc code I'll know I got it

Any entry point if I want to familiarize myself with the implementation?

Ok, technically there's this beta-reduction pass you might be interested in. But it isn't used https://github.com/typedclojure/typedclojure/blob/main/typed/clj.analyzer/src/typed/clj/analyzer/passes/beta_reduce.clj

It was an experiment which trying to figure out how to write rules for macros.

Here's the recursive algorithm for checking an AST https://github.com/typedclojure/typedclojure/blob/c60d81587d203ab53b922a2dce4b98870c61ea1c/typed/clj.checker/src/typed/clj/checker/check.clj#L203

It uses a fork of tools.analyzer that has an :unanalyzed node. https://github.com/typedclojure/typedclojure/blob/main/typed/clj.analyzer/src/typed/clj/analyzer.clj https://github.com/typedclojure/typedclojure/blob/main/typed/cljc.analyzer/src/typed/cljc/analyzer.cljc

Here's a tiny type system in this analyzer. It's a great introduction https://github.com/typedclojure/typedclojure/blob/main/typed/clj.analyzer/test/typed_test/clj/analyzer/gilardi_test.clj

Cool. Thanks

analyze-outer == macroexpand1 on an AST node

otherwise, it's just tools.analyzer.

enjoy 🙂

I'll try to enjoy it responsibly 🙂

Another thing I think I asked on before is something like life time analysis which can be used to identify points between which a collection can be transient

Or even mutable if you can guarantee it does not escape

Nope, haven't tackled that yet. Actually it's unclear if it'll straightjacket the rest of the type checker, we'll see.

It'll probably be fine in practice, if I ever figure out how to do it.

This channel is riveting