core-typed 2024-04-02 | Slack Archive

I am stuck at annotating a deftype such that it does not allow nil values e.g.

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

(t/ann-datatype [w] NonNilDataClass [v :- w]) ;; May be I can apply :filters here?
(deftype NonNilDataClass [v])


(t/ann ->NonNilDataClass (t/All [w] [w :-> (NonNilDataClass w) :filters {:then (! nil 0) :else (is nil 0)}]))
(defn ->NonNilDataClass
  [v]
  (assert (nil? v) "nil supplied as value")
  (NonNilDataClass. v))

(t/check-ns-clj)

;Expected result with filter {:then (! nil v__#0), :else (is nil v__#0)}, got filter {:then tt, :else tt}
;
;
;in:
;(fn*
; ([v]
;  (do (assert (nil? v) "nil supplied as value") (NonNilDataClass. v))))
;
;
;
;Execution error (ExceptionInfo) at clojure.core.typed.errors/print-errors! (errors.cljc:299).
;Type Checker: Found 1 error

Prashant15:04:28

Got it working 😃

(t/defalias NonNil (t/TFn [x] (t/I x (t/Not nil))))

(t/ann-datatype [w] NonNilDataClass [v :- (NonNil w)])
(deftype NonNilDataClass [v])

with (NonNilDataClass. 10)

(t/check-ns-clj)
=> :ok

with (NonNilDataClass. nil)

(t/check-ns-clj)
=>
Type Error 
Polymorphic function (new NonNilDataClass nil) could not be applied to arguments:
Polymorphic Variables:
	w

Domains:
	(fr33m0nk.typed/NonNil w)

Arguments:
	nil

Ranges:
	(NonNilDataClass w)




in:
(new NonNilDataClass nil)
Type Checker: Found 1 error

Prashant15:04:02

Above also works with ->NonNilDataClass as expected

Prashant15:04:50

#Also sent to the channel

While I have solved my problem, I would love to know more about :filters and when to use them

ambrosebs16:04:50

Also possible: (t/I x Object)

👍 1

Prashant16:04:29

Totally forget I could use (t/I x Object) (`null pointer exceptions` should have reminded me of this 😅 ) PS: Is there any documentation for using :filters? Do they provide Type refinement? I can also look at examples and try making sense of it if this isn't documented.

ambrosebs17:04:11

I don't remember, but it implements "occurrence typing". Here's the original paper https://www2.ccs.neu.edu/racket/pubs/icfp10-thf.pdf

ambrosebs17:04:35

See section 2

ambrosebs17:04:51

yes, it's related to type refinement. my friend Andrew also extended it to refinement types for Typed Racket https://arxiv.org/pdf/1511.07033v1.pdf

Prashant17:04:07

Thanks Ambrose, much appreciated 👍

🎉 1

Prashant15:04:50

replied to a thread:I am stuck at annotating a deftype such that it does not allow nil values e.g. (require '[typed.clojure :as t]) (t/ann-datatype [w] NonNilDataClass [v :- w]) ;; May be I can apply :filters here? (deftype NonNilDataClass [v]) (t/ann ->NonNilDataClass (t/All [w] [w :-> (NonNilDataClass w) :filters {:then (! nil 0) :else (is nil 0)}])) (defn ->NonNilDataClass [v] (assert (nil? v) "nil supplied as value") (NonNilDataClass. v)) (t/check-ns-clj) ;Expected result with filter {:then (! nil v__#0), :else (is nil v__#0)}, got filter {:then tt, :else tt} ; ; ;in: ;(fn* ; ([v] ; (do (assert (nil? v) "nil supplied as value") (NonNilDataClass. v)))) ; ; ; ;Execution error (ExceptionInfo) at clojure.core.typed.errors/print-errors! (errors.cljc:299). ;Type Checker: Found 1 error

While I have solved my problem, I would love to know more about :filters and when to use them

2024-04-02

Channels