core-typed

Prashant 2024-04-18T09:36:00.263529Z

I am stuck at trying to set bounds using ann-datatype . I think I am missing something really basic. Some help would be greatly appreciated.

(ann-datatype [[x :variance :covariant :< t/Num]] SomeData [count :- x])
(deftype SomeData [count])

;; =>
Type Error (NO_SOURCE_FILE) 
Type Error (:<NO LINE>) Type function argument number 1 (x) has kind (t/Type :< t/Num) but given x with missing bounds

in: ((t/TFn [[x :variance :covariant :< t/Num]] (SomeData x)) x)
Execution error (ExceptionInfo) at clojure.core.typed.errors/print-errors! (errors.cljc:299).
Type Checker: Found 1 error

2024-04-18T15:53:47.408499Z

It's a bug.

Prashant 2024-04-18T16:05:10.461249Z

Oh! Should I log an issue at Github? I tried to get this to work using t/Match but it didn't work either e.g.

(defalias NumOrError (t/TFn [[y :variance :invariant]]
                            (t/Match y
                                     t/Num :-> t/Num
                                     (t/Not t/Num) :-> t/TCError)))

(t/ann-datatype [x] SomeData [count :- (NumOrError x)])
(deftype SomeData [count])

(SomeData. 10)
and (t/check-ns-clj) reported errors:
Polymorphic function (new SomeData 10) could not be applied to arguments:
Polymorphic Variables:
	x

Domains:
	(fp.typed.monads/NumOrError x)

Arguments:
	(t/Val 10)

Ranges:
	(SomeData x)

in:
(new SomeData 10)

Execution error (ExceptionInfo) at clojure.core.typed.errors/print-errors! (errors.cljc:299).
Type Checker: Found 1 error

2024-04-18T16:06:43.096929Z

Yeah please put those examples. There's a scoping issue somewhere.

👍 1
2024-04-18T16:07:35.099309Z

You could try this: (ann-datatype [[x :variance :covariant]] SomeData [count :- (t/I x t/Num)])

👍 1
Prashant 2024-04-18T16:14:08.649649Z

I was trying to create a simple Result type akin to Rust but couldn't get it to work.

(t/ann-protocol [[M :variance :contravariant]]
  IResult
  then (t/All
         [a b]
         [(M a) [a :-> (t/U a b)] :-> (M (t/U a b))]))

(defprotocol IResult
  (then [this f]))

(t/ann-datatype [e] Err [err :- e] :extends [(IResult Err)])
(deftype Err [err]
  IResult
  (then [this _]
    this))

(ann-datatype [v] Ok [value :- v] :extends [(IResult Ok)])
(deftype Ok [value]
  IResult
  (then [_ f]
    (try
      (let [res (f value)]
        (cond
          (satisfies? IResult res) res
          (instance? Exception res) (Err. res)
          :else (Ok. res)))
      (catch Exception e
        (Err. e)))))
(t/chec-ns-clj) would always report following errors:
Type Error 
Type mismatch:

Expected: 	(Err (t/U b a))

Actual: 	(t/I (Err e) (Err a))

in:
`this`

Execution error (ExceptionInfo) at clojure.core.typed.errors/print-errors! (errors.cljc:299).
Type Checker: Found 1 error
Could this also be related to the same issue?

Prashant 2024-04-18T16:15:51.688749Z

I was also wondering if there's a cooler way to create a Result type using t/Match 😄

2024-04-18T16:32:59.187149Z

That looks like a type simplification issue. Maybe make Error's type param covariant?

2024-04-18T16:34:59.214429Z

IResult's param looks invariant to me.

2024-04-18T16:35:34.124409Z

But I struggle to combine object orientation with variance. Why is it contravariant?

2024-04-18T16:42:15.110689Z

Or rather, it's a subtyping issue. (Err (U a b)) is unrelated to (Err a) if Err is invariant.

Prashant 2024-04-18T16:42:28.176209Z

Thanks! for the tip

(ann-datatype [[e :variance :covariant]] Err [err :- e] :extends [(IResult Err)])
caused the Err type mismatch to pass. I was under the impression just specifying type variable e.g. [e] has implied :variance of :covariant I made IResult's param's type variable contravariant as then can take can be like [(Ok a) -> (Err b)]. Maybe it's wrong. I will try with invariant.

2024-04-18T16:42:43.830269Z

Invariant is the default.

2024-04-18T16:43:03.227129Z

Oh wait, I forgot I implemented variance inference.

2024-04-18T16:43:44.235549Z

But I guess it inferred invariant here?

Prashant 2024-04-18T16:44:32.294769Z

I do remember one of the type check messages yelling at me for setting wrong variance. I can't recall whether it was for a ann-protocol, a TFn or a ann-datatype

Prashant 2024-04-18T16:45:39.634119Z

I wonder if I can implement something simpler for Result type using t/Match ? something akin Rust's enum may be

2024-04-18T16:54:51.381779Z

Not sure. How would you implement this in vanilla clojure with just tagged maps? Might be an easier starting point for me to help.

👍 1
2024-04-18T16:55:04.012989Z

Or even with deftypes?

2024-04-18T16:56:07.157079Z

I guess that's what you sent me.

Prashant 2024-04-18T16:56:38.435039Z

Yeah, I am still struggling with the type simplification on the Ok deftype

2024-04-18T16:56:57.432499Z

Did you mark it covariant?

Prashant 2024-04-18T16:59:03.186649Z

Yes, I also simplified code quite a bit

(t/ann-protocol [[M :variance :invariant]]
  IResult
  then (t/All
         [a b]
         [(M a) [a :-> (t/U a b)] :-> (M (t/U a b))]))

(defprotocol IResult
  (then [this f]))

(ann-datatype [[e :variance :covariant]] Err [err :- e] :extends [(IResult Err)])
(deftype Err [err]
  IResult
  (then [this _]
    this))

(ann-datatype [[v :variance :covariant]] Ok [value :- v] :extends [(IResult Ok)])
(deftype Ok [value]
  IResult
  (then [_ f]
    (Ok. (f value))
;; Ideally this execution will be wrapped in try-catch block
))
Now the error is on
Function f could not be applied to arguments:

Domains:
	a

Arguments:
	v

Ranges:
	(t/U a b)

in:
(f value)

Execution error (ExceptionInfo) at clojure.core.typed.errors/print-errors! (errors.cljc:299).
Type Checker: Found 1 error

2024-04-18T17:03:28.226409Z

bit of a mind bender 🙂

2024-04-18T17:04:44.890049Z

maybe you need to manually instantiate f

Prashant 2024-04-18T17:05:27.022539Z

Dumb question. How would I do that?

2024-04-18T17:05:30.633669Z

((t/inst f v v) value) something like that, but intelligently chosen types

👍 1
2024-04-18T17:05:53.701069Z

it will at least give you a precise error message

Prashant 2024-04-18T17:07:10.441779Z

Just to contrast current deftype and protocol approach with t/Match

(defalias Ok (t/TFn [[x :< (t/Not Exception)]] x))
(defalias Err (t/TFn [[x :< Exception]] x))

(defalias Result (t/TFn [[x]]
                        (t/Match x
                                 Exception :-> (Err x)
                                 (t/Not Exception) :-> (Ok x))))

(ann then (t/All [x]
                 (t/IFn [(Err x) [x :-> x] :-> (Err x)]
                        [(Ok x) [x :-> x] :-> (Result x)]))) 

Prashant 2024-04-18T17:08:19.282709Z

This is something I thought just now, so may not work.

Prashant 2024-04-18T17:32:11.695559Z

I think I will take a break now. Spend some time with my toddler and unwind 🙂

❤️ 1
2024-04-18T18:31:58.306589Z

yeah this is heady stuff, also not that well supported. but I'm glad you're doing it.

❤️ 1