Clojurians Log v2

@ben.sless here's how this one works:

(let [f (comp (fn [y] y)
              (fn [x] x))]
  (f 1))

1. (SymbolicClosure (fn [y] y))
2. (SymbolicClosure (fn [x] x))

1. (SymbolicClosure (fn [y] y)) <: [b :-> c]
2. (SymbolicClosure (fn [x] x)) <: [a :-> b]

1. (SymbolicClosure (fn [y] y)) <: [Nothing :-> ?]
2. (SymbolicClosure (fn [x] x)) <: [Nothing :-> ?]

1. (fn [y :- Nothing] y)) ====> [Nothing :-> Nothing]
2. (fn [x :- Nothing] x)) ====> [Nothing :-> Nothing]

1. (SymbolicClosure (fn [y] y)) <: [Nothing :-> ?]
2. (SymbolicClosure (fn [x] x)) <: [Int :-> ?]

1. (fn [y :- Nothing] y)) ====> [Nothing :-> Nothing]
2. (fn [x :- Int] x)) ====> [Int :-> Int]

1. (SymbolicClosure (fn [y] y)) <: [Int :-> ?]
2. (SymbolicClosure (fn [x] x)) <: [Int :-> ?]

1. (fn [y :- Int] y)) ====> [Int :-> Int]
2. (fn [x :- Int] x)) ====> [Int :-> Int]

[[Int :-> Int] [Int :-> Int] :-> [Int :-> Int]]

Yes, the function's code itself is embedded in its type.

To check something like this, the calls of f and g in comp have the source code available, and effectively a beta reduction happens.

(is-tc-e (let [comp (fn* [f g] (fn* [x] (f (g x))))
                 f (fn* [x] x)
                 g (fn* [y] y)]
             ((comp f g) 1))
           t/Int)

For get-in, I think that's more of a type-level problem. The best idea I've had so far is reify a Get type and then give get-in this type (but I haven't tried it yet):

(t/ann get-in (All [m ks] [m ks :-> (GetIn m ks]))

Though I'm fairly confident something like that will work. Here's the current type of assoc:

cc/assoc
(t/All [m k v c :..] (t/IFn [m k v (t/HSeq [c c] :repeat true) <... c :-> (t/Assoc m k v c :.. c)]
                            ;[m k v (t/HSeq [k v] :repeat true) <* :-> (t/Assoc m k v)]
                            [nil k v (t/HSeq [c c] :repeat true) <... c :-> (t/Assoc nil k v c :.. c)]
                            [nil k v (t/HSeq [k v] :repeat true) <* :-> (t/Map k v)]))

You basically push the problem into type simplification. You eventually get types like (Assoc {:a Int} :b Bool) then simplify them to {:a Int :b Bool} .

Similar for this hypothetical GetIn type. (GetIn {:a {:b Int}} [:a :b]) => Int

t/Get actually exists, it's just not used in any annotations yet since clojure.core/get is hardcoded into the type checker since that was the original implementation.

Eventually I think this will work instead:

(t/ann get (All [m k] [m k :-> (Get m k)]))

What directs my question is something which has been my white whale for a while, which is using inlining and simplification for optimization. So some symbolic manipulation could turn (get-in m [x y]) into (get (get m x) y). I'm wondering if this mechanism could be leveraged for it

I don't think so, but I went down the inlining path at some point with a different approach that I've mostly abandoned. I experimented with get-in also https://github.com/typedclojure/typedclojure/blob/37a86feb5adc2dcf925bfa5345cfdf33cf859736/typed/clj.runtime/src/clojure/core/typed/expand.clj#L508-L544

It mostly amounted to (the equivalent to) :inline rules that include improved static error messages in their expansion.

Yeah, but something I noticed with this, having very similar code in clj-fast https://github.com/bsless/clj-fast/blob/master/src/clj_fast/lens.clj#L8C1-L18C3 What I would have wanted is something to do that generically, i.e. it knows that calling seq on any collection returns a collection with same elements, and that calling if on a truthy value selects a branch. That way you can automatically inline get-in, not ad-hoc

Basically, I want partial evaluation and elimination of constructors

Yeah, Typed Clojure is capable of that kind of reasoning. And I think the answer is yes, the symbolic execution I've been using above can be used for inlining and optimization if enough bookkeeping is done. Right now, the symbolic execution is for local functions only, but that's only really for tractability. There's nothing really stopping grabbing the source code of get-in and letting it live in a type, it's just that right now it's done only for local functions.

The symbolic execution lives in "type land" and the inlining needs to get back to "expression land". That's the bookkeeping I mean.

And it's a mutually recursive process. Type checking can call subtyping, can call type checking etc.

So I think the devil is in the details. But in principle it sounds ok.

The trickiest detail is that the same piece of code could be checked multiple times at different types. e.g., assoc has 4-5 types. So the inlining has to agree with all the arities in some way.

Typed Racket probably deals with this better, since it inserts casts and things into type checked code. I've been mostly uninterested in this kind of thing in Typed Clojure, but I try and not destroy the possibility of doing it in the future. (Typed Clojure can already insert casts, but it gets weird once you have multiple arities).

Looks like Typed Clojure just gives up if it needs to check the same piece of code twice https://github.com/typedclojure/typedclojure/blob/37a86feb5adc2dcf925bfa5345cfdf33cf859736/typed/clj.checker/src/typed/cljc/checker/check/fn_methods.clj#L301-L309

I'm guessing Typed Racket also does the same in this case. I can't think of a good strategy. I think with most user-land code, you'll only check code at a single type, which is I image is the entry point for most inlining optimization, so it gives me some hope.