Clojurians Log v2
core-typed
https://github.com/typedclojure/typedclojure/commit/0f222f73cc85d74ccd73bb3d9701a05da902ad03, can now check such higher-order function definitions:
(ann takes-hof [[[t/Int :-> t/Int] :-> t/Int] :-> t/Int])
(defn takes-hof [f] (f #(inc %)))%.Real-world function this helped check with just a top-level annotation:
(t/defalias ParserK [t/Any Pos (t/Seqable t/Any) :-> t/Any])
(t/defalias ParserTramp [t/Any t/Any Pos (t/Coll t/Any) ParserK :-> t/Any])
(t/ann re/fmap-parser [[t/Any :-> t/Any] ParserTramp :-> ParserTramp])I think Typed Clojure found a bug in malli's impl, that's always fun.
How far is typed's implementation from being used as an inline pass in a compiler?
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
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
analyze-outer-root == macroexpand
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