Typechecking failure with HMaps, All & Any

[Josh Tilles]

I don't understand why the failing example doesn't typecheck. My thinking is: if (:example/foo m) returns anything other than nil, then the first signature would have been triggered.

Code:

(ns example

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

(t/ann failing-func (t/All [x]

                      (t/IFn ['{::foo x} -> x]

                             [t/Any -> nil])))

(defn failing-func [m]

  (::foo m))

(t/ann passing-func (t/All [x]

                      (t/IFn ['{::foo x} -> x]

                             [(t/HMap :absent-keys #{::foo}) -> nil])))

(defn passing-func [m]

  (::foo m))

Output of (t/check-ns 'example):

(t/check-ns 'example)

Start collecting example

Finished collecting example

Collected 1 namespaces in 70.703239 msecs

Not checking clojure.core.typed (does not depend on clojure.core.typed)

Start checking example

Checked example in 19.525299 msecs

Checked 2 namespaces  in 97.22153 msecs

Type Error (example.clj:8:3) Type mismatch:

Expected: nil

Actual: t/Any

in: (:example/foo m)

ExceptionInfo Type Checker: Found 1 error  clojure.core/ex-info (core.clj:4593)

[Ambrose Bonnaire-Sergeant]

This is expected, since each arity is checked by itself.

I don't know how well this works, but try:

(t/ann failing-func (t/All [m]

                      [m -> (t/Get x ::foo)]))

[Ambrose Bonnaire-Sergeant]

Rather

(t/ann failing-func (t/All [m]

                      [m -> (t/Get m ::foo)]))

[Josh Tilles]

Ah, okay: I had assumed that the second arity would somehow "know" that the first hadn't matched. In the future I'll keep in mind that they're all independent.

I like your proposed t/Get solution, but it fails for me:

Source code:

(ns example

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

(t/ann failing-func (t/All [x]

                      [x -> (t/Get x '::foo)]))

(defn failing-func [m]

  (::foo m))

Output of (t/check-ns 'example):

Start collecting example

Finished collecting example

Collected 1 namespaces in 57.654291 msecs

Not checking clojure.core.typed (does not depend on clojure.core.typed)

Start checking example

Checked example in 11.556961 msecs

Checked 2 namespaces  in 74.334535 msecs

Type Error (example.clj:8:3) Type mismatch:

Expected: (t/Get x (t/Val :example/foo))

Actual: t/Any

in: (:example/foo m)

ExceptionInfo Type Checker: Found 1 error  clojure.core/ex-info (core.clj:4593)

Maybe the failure is related to CTYP-262?

By the way, I also attempted to use t/Difference to approximate a solution, but apparently I'm misunderstanding its purpose and/or how to use it:

(t/ann failing-func (t/All [x]

                      (t/IFn ['{::foo x} -> x]

                             [(t/Difference t/Any '{::foo Object}) -> nil])))

the typechecker quickly fails with:

AssertionError Assert failed: (set? without)  clojure.core.typed.type-rep/DifferenceType-maker (type_rep.clj:829)

Thanks a ton, Ambrose!

--Josh

[Ambrose Bonnaire-Sergeant]

We're treading into experimental territory with Difference and Get.

It's usually better for the type checker if you provide positive types, rather than negation types.

I think your example in the OP with :absent-keys is the best approach atm.

Thanks,

Ambrose