core.typed не сообщает об ошибке типа в repl

Вот часть примера, взятого из репозитория core.typed github:

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

person qed    schedule 22.05.2015    source источник


Ответы (2)


Вам необходимо явно согласиться на неявную проверку типов. Измените форму ns следующим образом:

(ns ^:core.typed typedclj.rps-async
   ...)
person Ambrose    schedule 23.05.2015
comment
Добавил, но это не имеет значения. - person qed; 23.05.2015
comment
Как вы оцениваете вещи? Вы используете IDE? Лейн РЕПЛ? - person Ambrose; 24.05.2015
comment
Спасибо, продолжаю тестировать курсивом. - person Ambrose; 24.05.2015
comment
Прохладный. С нетерпением жду вашего следующего выпуска. Продолжайте хорошую работу! :-) - person qed; 24.05.2015
comment
О, вы можете настроить (и я сделал) курсив для использования Leiningen nrepl, так что я подозреваю, что это не должно быть реальной проблемой здесь? - person qed; 24.05.2015
comment
Я думаю, что Cursive использует некоторые функции, которые я пока не поддерживаю. Можете ли вы проверить с обычным lein repl? requireing пространство имен должно вызвать ошибку типа. - person Ambrose; 24.05.2015
comment
Попробуйте core.typed 0.3.0-alpha2. - person Ambrose; 28.05.2015

Да, он сообщает об ошибках во время выполнения, когда вы явно просите его сделать это. Это немного отличается от статически типизированных языков, где ошибка типа препятствует успешной сборке программы, здесь это просто необязательная «проверка работоспособности».

Проверка типов выполняется отдельно от компиляции и должна запускаться явно

Используйте clojure.core.typed/check-ns для проверки текущего пространства имен. Это можно сделать в РЕПЛ.

Примечание. Глобальные аннотации, такие как ann, действительны только в том случае, если они находятся в пространстве имен, которое в настоящее время проверяется с помощью check-ns, или заключено в cf. raw ann в REPL не действует. Глобальные аннотации должны быть формами верхнего уровня или внутри (возможно, вложенных) верхнего уровня do.

clojure.typed Краткое руководство

В REPL вы должны заключать свои выражения в cf, чтобы типы выводились из заданного кода и распечатывались. (см. эту сообщение в блоге) Если вы хотите проверить тип кода из пространства имен, определенного в исходных файлах, используйте check-ns для проверки типа всего пространства имен.

person D-side    schedule 22.05.2015
comment
Это было верно до 0.2.92; OP тестирует новые функции. - person Ambrose; 23.05.2015
comment
@Ambrose - это документацию по этому которую трудно найти, или ее просто еще не существует? - person D-side; 23.05.2015
comment
В CHANGELOG.md есть некоторые документы, в противном случае их нет. Функция все еще WIP. - person Ambrose; 24.05.2015