usage of conj in core.typed

Question

The following code snippet in core.typed

(defn conj-num [coll x]
  (conj coll (byte x)))

(t/cf (t/ann conj-num (t/IFn [(t/ASeq t/Any) t/Any -> (t/ASeq t/Num)])))

(t/cf (reduce conj-num [] (range 10)))

fails with the message

Type Error...
Polymorphic function reduce could not be applied to arguments: 
Polymorphic Variables:  a   c

Domains:    [a c -> (t/U a (Reduced a))] a (t/Option (Seqable c))

Arguments:  [(t/ASeq t/Any) t/Any -> (t/ASeq t/Num)] (t/HVec []) (t/ASeq t/AnyInteger)

Ranges:     a


in: (reduce conj-num [] (range 10))


ExceptionInfo Type Checker: Found 1 error  clojure.core/ex-info (core.clj:4403)

The reducing fn accepts an ASeq of Any and another argument of type Any and returns a sequence of numbers. I have expected that the result of the type checker was (t/ASeq t/Num) rather than an error. Any idea what I am doing wrong here?

Thank you.

Edit

Thanks for the responses. I was able to figure out the problem now. It wasn't clear how to interpret the error message given by core.typed, but now it really makes sense.

I read the error message above now as follows

Polymorphic Variables:
    a
    c

-> this are the variables of the reduce function. you can determine it's signature (or type) with (t/cf reduce). It will show you 3 arities, but the following message specifies which arity was chosen and why it didn't match.

Domains:
    [a c -> (t/U a (Reduced a))] a (t/Option (Seqable c))

Core.typed also gives us ranges. I read them as the variables that couldn't be matched.

Ranges:
    a

So we have to focus on a. Core.typed seems happy about b.

The following message is about the actual type being matched (the type of our arguments are matched against the type defined by the reduce fn).

Arguments:
    [(t/HVec [t/Num]) t/Any -> (t/HVec [t/Num])] (t/HVec []) (t/ASeq t/Num)

We match it by hand

[(t/HVec [t/Num ]) t/Any -> (t/HVec [t/Num])] (t/HVec []) (t/ASeq t/Num)
  --------------  -----    ----------------   --------   ------------
    a               b      (t/U a (Reduced a)    a       (t/Option ...)

The following is now evident

• a must be of type (t/HVec [t/Num]) because of the first occurence AND also (t/HVec []) because of the second occurence of a. Since it can't be both of them, core.typed correctly fails.
• the type (t/U a (Reduced a)) matches any a or a reduced a. I don't understand what Reduced a means (maybe it has to do with transducers?), but t/U just means it can match either or. So in our case it's just a itself.

What is missing in this example is to make sure that the type a has to match on both side, for instance:

;; a is still a vector
(def a [])

;; we give the type (t/HVec [t/Num]) to a. This makes it *more* compatible with our conj-num fn.

(t/cf (t/ann a (t/HVec [t/Num])))

;; core.typed is happy now ;)
(t/cf (reduce conj-num a (range 10)))

It's ofc not satisfying to hack about a. The problem is that conj-num is just not defined in a helpful way. It is very rigid. It basically doesn't allow the accumulator to be just a vector. Here's the final type:

(t/cf (t/ann conj-num
            (t/IFn [(t/U (t/HVec [])
                         (t/HVec [t/Num])) t/Num -> (t/HVec [t/Num])])))

;; great. we can now use [] as input.
(t/cf (reduce conj-num [] (range 10)))

This signature now works because the first argument a can now be either an empty vector (t/HVec []) or a vector of nums (t/HVec [t/Num]) which is exactly what conj-num returns. So all good now. It just seems that learning core.typed really is about learning how to read these error message. But it seems less hard now. Thanks for your answer, it helped me analyze the message and find a fix for it.

Answer 1

That's very probably because the type checking engine cannot match the type variable a.

Look:

Domains: [a c -> (t/U a (Reduced a))] a (t/Option (Seqable c))

Arguments: [(t/ASeq t/Any) t/Any -> (t/ASeq t/Num)] (t/HVec []) (t/ASeq t/AnyInteger)

Ranges: a

"c" is t/Any, that's done. Now for "a", on the left side of -> "a" is (t/Aseq t/Any) and on the right side (t/U a (Reduced a)) is (t/ASeq t/Num). It doesn't match. I would advise to change conj-num type to:

[(t/ASeq t/Num) t/Any -> (t/ASeq t/Num)]

Answer 2

The ordering of your commands means that your function conj-num is not being checked.

I recommend instead checking this in a file.

(ns typed.test
  (:require [clojure.core.typed :as t]))

(t/ann conj-num (t/IFn [(t/ASeq t/Any) t/Any -> (t/ASeq t/Num)]))
(defn conj-num [coll x]
  (conj coll (byte x)))

(reduce conj-num [] (range 10))

The definition of conj-num does not correspond to the annotation, so should throw a type error.