Using polymorphic records

[Brendan Tobolaski]

Apologies in advance if this has a very obvious solution.

I'm trying to annotate Cats' Either monad. I think I have correct annotations for both of the records

(t/ann-record [[a :variance :covariant]]
   cats.monad.either.Left
   [v :- a])

(t/ann-record [[a :variance :covariant]]
   cats.monad.either.Right
   [v :- a])

My goal is make these usable like the build in types, i.e. I'd like to be able to annotate the constructors like this:

(t/ann cats.monad.either.left
   [a -> (cats.monad.either.Left a)])

(t/ann cats.monad.either.right
   [a -> (cats.monad.either.Right a)])

Obviously I'm missing something there as all I get is an unresolved var a. Maybe what I'm missing is a (t/All [a] ...) but I'm not really sure. Even if that is correct, I'm not sure what I need to do to allow me to annotate functions like this

(t/ann collect-successfull
   [(t/U (cats.monad.either.Left String)
         (cats.monad.either.Right (t/Vec String))) -> (t/Vec String)])

(t/ann try-read
   [String -> (t/U (cats.monad.either.Left String)
                   (cats.monad.either.Right (t/HMap ...)))])

I'm very much a beginner at this as you can probably tell. I've spent some time digging through the documentation and source code and I'm at a loss for how to do this. Any help would be greatly appreciated.

[Ambrose Bonnaire-Sergeant]

As you mention, you're missing `All` binders. The `a` that is scoped in `(All [a] ..)` is a type variable which is

picked based on the specific invocation.

eg. identity is (All [x] [x -> x]), and (identity 1) instantiates x to Num (or some subtype of it), thus becoming [Num -> Num].

The later annotations for collect-successfull and try-read look correct to me.

Thanks,

Ambrose

[Piotr Jarzemski]

Hi Brendan,

I recently created a small project with core.typed annotations for funcool.cats: 

https://github.com/kazuhiro/cats.typed

It's far from being a complete reference, however, maybe you'll find it useful.

Regards,

Piotr Jarzemski