Clojurians Log v2

Sorry for bouncing off all these ideas. I was thinking how to make core.typed convincing to use by default by getting additional features beyond correctness out of its usage (such as more flexible high performance dispatch, or automatic bindings for other languages). I did see these ideas applied while having worked mostly with Python, Julia and a bit of Rust lately. I also took a look at Zig, which I think is interesting.

My intuition tells me that this might make Clojurians engage more with core.typed, but I might be wrong. The correctness alone is already super cool ofc.

I've moved away from static optimization capabilities in preference of highly parallelizable and cachable linting.

that's where the Clojure community seems to be indicating it's heading

the principles of optional type systems have always resonated with me since hearing Gilad Bracha's opinions on the risks of relying (too much) on highly complex type systems for security and correctness guarantees.

but concretely, there's a large cost to restricting a clojure namespace to only work if you have an external tool.

bouncing some ideas back 😉

I also find Racket's optimization coach compelling. If Clojure supported selective inlining maybe an external tool could assert that you've inlined optimally?

no?

Basically it does local type inference in each function and whenever it hits a dispatch of another function it devirtualizes the call (if it knows all the argument types and can identify the implementation being called). If the function has a specialized implementation for the type signature that has not been compiled yet this is also compiled at that point.

It is fundamentally a local way of doing type inference such that the resulting code is fast because it gets rid of virtual dispatch and, if functions are implemented for concrete types with explicit memory sizes (as recommended), it also can allocate the memory and unbox numbers etc.

I am wondering if core-typed could provide a similar way to implement multiple dispatch on the basis of all the concrete types of the arguments (and not just the type of the first argument or arity alone).

Where you get warned if a concrete type signature is not implemented by core-typed at inference time, and if it is it could devirtualize the dispatch.

that makes sense. julia's multiple dispatch is basically the type based version of defmulti. it would not be enough to check though, it picks the defmethod based on the full types of the invocation and the closest defmethod implementation and then devirtualizes the call removing runtime dispatch. defmulti is very powerful, but also fairly slow, so this would give you a way to have flexible and fast dispatch if you type your functions well. i am not saying this needs to be implemented, but i think the clojure community should steal more new ideas and play with them.

i need to actually start using core.typed to be honest. i want to basically just use spec or something similar to express exactly the contraints (basically dependent types) that are on my mind and then maybe make them checkable if they are too general (ideally through an automatic form of relaxation into the type checker).

i think it is not ideal if i have to restrict the invariants because of what can be checked and not express them. but it is also not ideal if type checking doesn't work automatically anymore. to fill this gap this "relaxation" could work. where for instance even? would be relaxed to integer? , this will be a bit tricky with co- and contravariance how to relax, but most importantly somehow these relaxations would need to be specified. i do think we should have standardized types that are used as libraries, then this relaxation work for instance can be shared and also libraries would be proven to be compatible before you even pick them up. this is like ontologies in RDF or the semantic web. it is a lot of work to make that work in the large, but i think if it is possible to make it work in the small it could be fairly useful.