键入的 Clojure 错误答案

【问题标题】：Typed Clojure Errors键入的 Clojure 错误
【发布时间】：2014-08-03 18:45:41
【问题描述】：

我正在我的项目中实现core.typed 注释。以下代码工作正常：

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

如果我稍微改变函数定义，我会得到几个不同的错误：

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

从类型的角度来看，我预计这 3 个示例或多或少是等价的。具体来说，我假设：

(t/Vec String) 将在 nth 和 first 的域中
当x 和y 的类型为String 时，(shuffle [x y]) 的范围将不包括nil

这是 core.typed 的限制，还是我有根本的误解？

【问题讨论】：

标签： clojure clojure-core.typed

【解决方案1】：

这里要了解的主要内容是现在nth 的工作原理，特别是解构如何使用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)]))

如果没有默认值，nth 将在传递集合和超出其边界的索引时抛出异常。类型化 Clojure 不会尝试阻止此异常。

(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}]

使用默认值，默认值始终是结果类型的一部分。

(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}]

向量解构扩展为nth，默认为nil。

还要注意shuffle 的返回类型没有长度信息。有时异构数据结构比同质数据结构更准确地解构。

【讨论】：