Typed Clojure Errors

Question

I'm implementing core.typed annotations in my project. The following code works fine:

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

(t/ann foo [String String -> String])
(defn foo [x y]
  (str x y))

(t/ann works [String String -> String])
(defn works [x y]
  (t/let [z :- (t/Vec String), (shuffle [x y])
          a :- String, (nth z 0)
          b :- String, (nth z 1)]
    (foo a b)))

If I alter the function definition slightly, I get a couple different errors:

(t/ann fails-1 [String String -> String])
(defn fails-1 [x y]
  (t/let [z :- (t/Vec String), (shuffle [x y])
          ; Fails because (t/Vec String) is not included
          ; in the domain of first or second
          a :- String, (first z)
          b :- String, (second z)]
    (foo a b)))

(t/ann fails-2 [String String -> String])
(defn fails-2 [x y]
  (t/let [[a b] :- (t/Vec String), (shuffle [x y])]
    ; Fails because a and b are of type (t/U nil String)
    (foo a b)))

From a type perspective, I would have expected these 3 examples to be more or less equivalent. Specifically I assumed:

• (t/Vec String) would be in the domain of both nth and first
• The range of (shuffle [x y]) won't include nil when x and y are of type String

Is this a limitation of core.typed, or do I have a fundamental misunderstanding?

Answer 1

The main thing to understand here is now nth works, and specifically how destructuring uses nth.

nth type

(∀ [x y]
   (λ [(∪ (∩ Sequential (Seqable x)) (Indexed x)) AnyInteger → x]
      [(∪ nil (∩ Sequential (Seqable x)) (Indexed x)) AnyInteger y → (∪ x y)]
      [(∪ nil (∩ Sequential (Seqable x)) (Indexed x)) AnyInteger → (∪ nil x)]))

Without a default value nth will throw an exception if passed a collection and an index outside its bounds. Typed Clojure does not try to prevent this exception.

(t/cf (t/fn [a :- (t/ASeq t/Int)] :- t/Int (nth a 0)))
;=> [(t/IFn [(t/ASeq t/Int) -> (t/U Integer Long BigInt BigInteger Short Byte)]) {:then tt, :else ff}]

With a default value, the default value is always part of the result type.

(t/cf (t/fn [a :- (t/ASeq t/Int)] :- (t/U nil t/Int) (nth a 0 nil)))
=> [(t/IFn [(t/ASeq t/Int) -> (t/U nil Integer Long BigInt BigInteger Short Byte)]) {:then tt, :else ff}]

Vector destructuring expands to an nth with default of nil.

Also notice that the return type of shuffle has no length information. Sometimes heterogeneous data structures destructure more accurately than their homogeneous counterparts.