Fork me on GitHub
ambrosebs02:04:29, 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 %)))
Before, could not infer the type of %.


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.

❤️ 1
Ben Sless04:04:46

How far is typed's implementation from being used as an inline pass in a compiler?

Ben Sless04:04:02

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.

wow 1

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.

🧠 1

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.

Ben Sless04:04:32

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

wow 1

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.

Ben Sless04:04:39

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.

Ben Sless04:04:41

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

Ben Sless04:04:01

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.

Ben Sless04:04:08

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

Ben Sless04:04:44

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


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

Ben Sless05:04:50

Cool. Thanks


analyze-outer == macroexpand1 on an AST node


otherwise, it's just tools.analyzer.

Ben Sless05:04:16

I'll try to enjoy it responsibly 🙂

😆 1
Ben Sless05:04:20

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

Ben Sless05:04:52

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