I don't quite understand the behavior or clojure.core.typed/cf
as explained below.
I assume cf
is used to infer the type of a form
(t/cf (+ 1 2)) => Long
Now, this fails
(t/cf (/ 1 0)) => Error
This indicates to me that the sexpr was evaluated prior to be type checked. I had expected Long
.
When I define a custom function:
(t/ann my-fn [t/Any -> t/Num])
(defn my-fn [x]
(assert (number? x))
(println "CALLED")
x)
I can used this in the same expression again and it fails, indicating that the fn was indeed called.
(t/cf (/ 1 (my-fn 0)) => Error, because it evaluates my-fn. no type inference here??
However, then the following makes no sense to me.
(t/cf (range)) => (t/ASeq t/AnyInteger)
Why is in this case function range NOT evaluated, also if it did evaluate the expression, the following examples should return the same type:
(t/cf (->> (range 2) vec)) => (t/AVec (t/U Short Byte Integer BigInteger Long BigInt))
(t/cf [0 1]) => [(t/HVec [(t/Val 0) (t/Val 1)]) {:then tt, :else ff}]
But they return different types.
My gut feeling is that it has to do with constants, i.e. when I type check a form that contains t/Val's, then core.typed autoamtically evaluates it. This however doesn't explain why for certain functions it does not evaluate it. The 2
in (range 2)
is definitely a constant, so why this difference in behavior.
If the forms are evaluated before type checking then the following should have the same behavior
(t/cf (map inc (range 10))))
(t/cf (map #(inc %) (range 10))))
But core.typed
does indeed see a difference. The second example fails because the anonymous fn
receives a t/Any
by default and you cannot call inc
on it. So this means that core.typed
must do some analysis of the form plus it also evaluates it. I find this a bit confusing I confess, maybe someone can enlighten me.
Edit: A short summary
Why does the following relation seems to be true in some but not all cases?
(t/cf form) <=> (let [x form] (t/cf x))
core.typed
performs completely static type checking.
The compilation pipleline for cf
is read -> analyze -> type check -> eval
.
If there is a static type error, that is considered fatal.
Otherwise the evaluation will be performed.
(cf (/ 1 0))
throws a runtime error because (/ 1 0)
is a well-typed expression.
The reason evaluation is needed is related to the practicalities of analysing Clojure code — strange things happen if you analyze code then don’t evaluate it.