core.typed 未在 repl 中报告类型错误

Question

这是从 core.typed github repo 中获取的示例的一部分：

(ns typedclj.rps-async
  (:require [clojure.core.typed :as t]
            [clojure.core.async :as a]
            [clojure.core.typed.async :as ta]))

(t/defalias Move
  "A legal move in rock-paper-scissors"
  (t/U ':rock ':paper ':scissors))

(t/defalias PlayerName
  "A player's name in rock-paper-scissors"
  t/Str)

(t/defalias PlayerMove
  "A move in rock-paper-scissors. A Tuple of player name and move"
  '[PlayerName Move])

(t/defalias RPSResult
  "The result of a rock-paper-scissors match.
  A 3 place vector of the two player moves, and the winner"
  '[PlayerMove PlayerMove PlayerName])

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Implementation
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(t/ann MOVES (t/Vec Move))
(def MOVES [:rock :paper :scissors])

(t/ann BEATS (t/Map Move Move))
(def BEATS {:rock :scissors, :paper :rock, :scissors :paper})
(def BEATS {:a :b})

请注意，在最后一行中，我将 BEATS 重新定义为 {:a :b}，这与它的类型注释冲突，但是当我在 repl 中对此进行评估时，不会引发错误。我期待一个错误，因为据说最新版本的 core.typed 能够在运行时报告类型错误。

这是整个 project.clj 文件：

            (defproject typedclj "0.1.0-SNAPSHOT"
                        :description "FIXME: write description"
                        :url "http://example.com/FIXME"
                        :license {:name "Eclipse Public License"
                                  :url  "http://www.eclipse.org/legal/epl-v10.html"}
                        :dependencies [[org.clojure/clojure "1.6.0"]
                                       [org.clojure/core.async "0.1.346.0-17112a-alpha" :exclusions [org.clojure/tools.analyzer.jvm]]
                                       [org.clojure/core.typed "0.2.92"]
                                       [clj-http "1.1.2"]
                                       [http-kit "2.1.18"]
                                       ]
                        :repl-options {:nrepl-middleware [clojure.core.typed.repl/wrap-clj-repl]}
                        :main ^:skip-aot typedclj.core
                        :target-path "target/%s"
                        :profiles {:uberjar {:aot :all}})

---

使用 core.typed 0.3.0-alpha2 可以很好地捕捉到这种类型错误：

Type Error (/private/var/folders/5d/44ctbbln4dsflgzxph1dm8wr0000gn/T/form-init3488589171262628870.clj:36:12) Type mismatch:

Expected:   typedclj.rps-async/Move

Actual:     (t/Val :b)
in: :b


Type Error (/Users/kaiyin/personal_config_bin_files/workspace/typedclj/src/typedclj/rps_async.clj:36:12) Type mismatch:

Expected:   (t/Map typedclj.rps-async/Move typedclj.rps-async/Move)

Actual:     (t/HMap :mandatory {:a typedclj.rps-async/Move} :complete? true)
in: {:a :b}

Answer 1

您需要明确选择加入隐式类型检查。像这样更改您的 ns 表单：

(ns ^:core.typed typedclj.rps-async
   ...)

Answer 2

是的，当您明确要求它这样做时，它会在运行时报告错误。这与静态类型语言略有不同，其中类型错误会阻止程序成功构建——这里只是一个可选的“健全性检查”。

类型检查与编译是分开的，必须显式运行

使用clojure.core.typed/check-ns 键入检查当前命名空间。 这可以在 REPL 中完成。

注意：像ann 这样的全局注解只有在 命名空间当前使用check-ns 检查，或包装在cf 中。 REPL 中的原始ann 无效。全局注释应该是 顶级表单或在（可能嵌套的）顶级do 内。

——clojure.typed Quick Guide

在 REPL 中，您应该将表达式包装在 cf 中，以便从给定的代码中推断出类型并打印出来。 （参见this blog post）如果您想对源文件中定义的命名空间中的代码进行类型检查，请使用check-ns 对整个命名空间进行类型检查。