Fork me on GitHub
#core-typed
<
2023-08-20
>
ambrosebs14:08:14

Working through comp, this infers as (Val 1)

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

ambrosebs21:08:50

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

(let [f (comp (fn [y] y)
              (fn [x] x))]
  (f 1))
comp's type is: comp :- (All [a b c] [[b :-> c] [a :-> b] :-> [a :-> c]]) when we call comp, it's passed two argument (types):
1. (SymbolicClosure (fn [y] y))
2. (SymbolicClosure (fn [x] x))
So we need to solve:
1. (SymbolicClosure (fn [y] y)) <: [b :-> c]
2. (SymbolicClosure (fn [x] x)) <: [a :-> b]
We fix the most precise types for the type variables, but use a "wildcard" placeholder type in covariant occurrences.
1. (SymbolicClosure (fn [y] y)) <: [Nothing :-> ?]
2. (SymbolicClosure (fn [x] x)) <: [Nothing :-> ?]
Then the type checking can proceed.
1. (fn [y :- Nothing] y)) ====> [Nothing :-> Nothing]
2. (fn [x :- Nothing] x)) ====> [Nothing :-> Nothing]
So the type of the call to comp can be instantiated as [[Nothing :-> Nothing] [Nothing :-> Nothing] :-> [Nothing :-> Nothing]] . Since there's no expected type this is good enough for now. But (f 1) forces the return type to need to be [Int -> ?]. That gives us a type for the a type variable. So we can check again with more information:
1. (SymbolicClosure (fn [y] y)) <: [Nothing :-> ?]
2. (SymbolicClosure (fn [x] x)) <: [Int :-> ?]
Gives:
1. (fn [y :- Nothing] y)) ====> [Nothing :-> Nothing]
2. (fn [x :- Int] x)) ====> [Int :-> Int]
Now we have a type for b thanks to the inferred return of 2. So check again:
1. (SymbolicClosure (fn [y] y)) <: [Int :-> ?]
2. (SymbolicClosure (fn [x] x)) <: [Int :-> ?]
This gives us a new type for c .
1. (fn [y :- Int] y)) ====> [Int :-> Int]
2. (fn [x :- Int] x)) ====> [Int :-> Int]
We don't learn any more information after this, so we can instantiate comp to:
[[Int :-> Int] [Int :-> Int] :-> [Int :-> Int]]

Ben Sless18:08:09

This is pretty incredible, does it work by symbolic evaluation? What happens with code like get-in when the keys seq is statically known? (It just calls reduce with get)

ambrosebs20:08:44

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

😮 2
4
ambrosebs20:08:24

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)
To type check (g x) , g has type (SymbolicClosure {...local type env...} (fn* [y] y))

ambrosebs20:08:39

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]))

ambrosebs20:08:59

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)]))

ambrosebs20:08:45

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} .

ambrosebs20:08:25

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

ambrosebs20:08:41

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.

ambrosebs20:08:15

Eventually I think this will work instead:

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

Ben Sless04:08:27

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

ambrosebs13:08:10

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

ambrosebs13:08:33

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

Ben Sless13:08:07

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

Ben Sless13:08:17

Basically, I want partial evaluation and elimination of constructors

ambrosebs13:08:51

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.

ambrosebs13:08:31

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

ambrosebs13:08:23

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

ambrosebs13:08:42

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

ambrosebs14:08:00

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.

ambrosebs14:08:56

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).

ambrosebs15:08:54

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.

ambrosebs21:08:50

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

(let [f (comp (fn [y] y)
              (fn [x] x))]
  (f 1))
comp's type is: comp :- (All [a b c] [[b :-> c] [a :-> b] :-> [a :-> c]]) when we call comp, it's passed two argument (types):
1. (SymbolicClosure (fn [y] y))
2. (SymbolicClosure (fn [x] x))
So we need to solve:
1. (SymbolicClosure (fn [y] y)) <: [b :-> c]
2. (SymbolicClosure (fn [x] x)) <: [a :-> b]
We fix the most precise types for the type variables, but use a "wildcard" placeholder type in covariant occurrences.
1. (SymbolicClosure (fn [y] y)) <: [Nothing :-> ?]
2. (SymbolicClosure (fn [x] x)) <: [Nothing :-> ?]
Then the type checking can proceed.
1. (fn [y :- Nothing] y)) ====> [Nothing :-> Nothing]
2. (fn [x :- Nothing] x)) ====> [Nothing :-> Nothing]
So the type of the call to comp can be instantiated as [[Nothing :-> Nothing] [Nothing :-> Nothing] :-> [Nothing :-> Nothing]] . Since there's no expected type this is good enough for now. But (f 1) forces the return type to need to be [Int -> ?]. That gives us a type for the a type variable. So we can check again with more information:
1. (SymbolicClosure (fn [y] y)) <: [Nothing :-> ?]
2. (SymbolicClosure (fn [x] x)) <: [Int :-> ?]
Gives:
1. (fn [y :- Nothing] y)) ====> [Nothing :-> Nothing]
2. (fn [x :- Int] x)) ====> [Int :-> Int]
Now we have a type for b thanks to the inferred return of 2. So check again:
1. (SymbolicClosure (fn [y] y)) <: [Int :-> ?]
2. (SymbolicClosure (fn [x] x)) <: [Int :-> ?]
This gives us a new type for c .
1. (fn [y :- Int] y)) ====> [Int :-> Int]
2. (fn [x :- Int] x)) ====> [Int :-> Int]
We don't learn any more information after this, so we can instantiate comp to:
[[Int :-> Int] [Int :-> Int] :-> [Int :-> Int]]