This page is not created by, affiliated with, or supported by Slack Technologies, Inc.
- # announcements (3)
- # asami (4)
- # babashka (79)
- # babashka-sci-dev (47)
- # beginners (97)
- # biff (12)
- # calva (7)
- # clj-commons (3)
- # clj-kondo (22)
- # clj-on-windows (13)
- # cljdoc (31)
- # cljfx (2)
- # cljs-dev (1)
- # clojure (85)
- # clojure-austin (4)
- # clojure-dev (12)
- # clojure-europe (15)
- # clojure-italy (8)
- # clojure-nl (4)
- # clojure-uk (4)
- # community-development (19)
- # conjure (3)
- # core-typed (40)
- # cursive (9)
- # datahike (21)
- # datomic (1)
- # emacs (7)
- # exercism (2)
- # graalvm (20)
- # graphql (1)
- # honeysql (16)
- # jobs (1)
- # malli (2)
- # off-topic (3)
- # pathom (28)
- # pedestal (3)
- # polylith (7)
- # reitit (14)
- # releases (1)
- # remote-jobs (1)
- # rewrite-clj (4)
- # shadow-cljs (21)
- # sql (21)
- # testing (8)
- # tools-deps (23)
- # vscode (8)
- # xtdb (38)
https://github.com/typedclojure/typedclojure/commit/0f222f73cc85d74ccd73bb3d9701a05da902ad03, can now check such higher-order function definitions:
Before, could not infer the type of
(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])
How far is typed's implementation from being used as an inline pass in a compiler?
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 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
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
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
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
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
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
Nope, haven't tackled that yet. Actually it's unclear if it'll straightjacket the rest of the type checker, we'll see.