core.typed 中 conj 的用法

Question

下面的代码片段在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)))

消息失败

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)

reducing fn 接受一个 ASeq of Any 和另一个 Any 类型的参数和 returns 一个数字序列。我期望类型检查器的结果是 (t/ASeq t/Num) 而不是错误。知道我在这里做错了什么吗？

谢谢。

编辑

感谢您的回复。我现在能够找出问题所在。之前不清楚如何解释 core.typed 给出的错误信息，但现在它确实有意义了。

我现在阅读上面的错误信息如下

Polymorphic Variables:
    a
    c

-> 这是 reduce 函数的变量。您可以使用 (t/cf reduce) 确定它的签名（或类型）。它将向您显示 3 个参数，但以下消息指定了选择的参数及其不匹配的原因。

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

Core.typed 也给了我们范围。我把它们读作无法匹配的变量。

Ranges:
    a

所以我们要关注a。 Core.typed 似乎对 b 感到高兴。

以下消息是关于匹配的实际类型（我们的参数类型与 reduce fn 定义的类型相匹配）。

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

我们手工搭配

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

以下内容现在很明显

a 必须是 (t/HVec [t/Num]) 类型，因为第一次出现并且 (t/HVec []) 因为 a 的第二次出现。由于不能同时是它们，因此 core.typed 正确地失败了。
类型 (t/U a (Reduced a)) 匹配任何 a 或简化的 a。不明白Reduced a是什么意思（可能和transducers有关？），但是t/U只是表示可以匹配or。所以在我们的例子中，它只是 a 本身。

此示例中缺少的是确保类型 a 必须在两侧匹配，例如：

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

关于 a 的破解通常并不令人满意。问题是 conj-num 没有以有用的方式定义。它非常坚硬。它基本上不允许累加器只是一个向量。这是最终类型：

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

此签名现在有效，因为第一个参数 a 现在可以是空向量 (t/HVec []) 或 nums (t/HVec [t/Num]) 的向量，这正是 conj-num returns.所以现在一切都好。看起来学习 core.typed 真的是在学习如何阅读这些错误信息。不过现在好像没那么难了。感谢您的回答，它帮助我分析了消息并找到了修复方法。

Answer 1

这很可能是因为类型检查引擎无法匹配类型变量a。

看：

域：[a c -> (t/U a (Reduced a))] a (t/Option (Seqable c))

参数：[(t/ASeq t/Any) t/Any -> (t/ASeq t/Num)] (t/HVec []) ( t/ASeq t/Any整数)

范围：一个

"c"就是t/Any，搞定了。现在对于 "a"，在 -> "a" 的左侧是 (t/Aseq t/Any) 并且在右侧 (t/U a (Reduced a))是 (t/ASeq t/Num)。它不匹配。我建议将 conj-num 类型更改为：

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

Answer 2

你的命令顺序意味着你的功能 conj-num 没有被检查。

我建议改为在文件中检查。

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

conj-num的定义与注解不对应，应该抛出类型错误。

core.typed 中 conj 的用法

usage of conj in core.typed

clojure

clojure-core.typed