Clojurians Log v2

answered @zilti over here if anyone wants to know https://clojurians.slack.com/archives/C03S1KBA2/p1581690839174800

@zilti anything I can help with?

Actually I am writing annotations right now ^^ Just like when I tried it a few years ago. And yes, I have two questions... 1. How do I define a subtype just for one declaration? Like [a Any -> a] where a is a subtype of let's say (U Kw Sym) only in that one definition? 2. core.typed just told me to add type hints to a Java constructor call. Making the argument be annotated seems to not suffice, is that on purpose, or not implemented yet?

1. let me look up the syntax xD 2. turn on (set! **warn-on-reflection** true) and fix reflection warnings. it should stop complaining

(All [[a :< (U Kw Sym)]] [a Any -> a])

try that

its a kwargs syntax, :< defines super constraint, :> subtype constraint

Okay, yes, I wasn't really sure how to express it anymore

btw which core.typed jar/s are you using?

And one more to vararg functions. I have a function (fn [& selectors] ...) and the annotation [& (Vec Selector) -> [State -> State]] is apparently wrong

yea.. one sec

I am using org.clojure/core.typed.checker.jvm {:mvn/version "0.7.2"}

try [(Vec Selector) * -> [State -> State]]

cool!

Ooh yes, that works 🙂

there's a & syntax for kwargs. some docs here https://github.com/clojure/core.typed/wiki/Types#rest-parameters

except use IFn

sorry, woefully out of date

Yea, that is the one I ran into, but I don't need kwargs in this case

Also, fyi: this will fail with an "Unannotated var: set-key" error: (defn set-key [key :- Kw modificator-fn [State -> Any]] :- [State -> State] ...) But it works when annotating it separately like this: (ann set-key [Kw [State -> Any] -> [State -> State]])

is that with t/defn ?

Yes. Actually I did a :as t :refer :all and tried both defn and t/defn. Seems to be a bit inconsistent though, so I am just using ann for now. If I find time I'll try to find out how it breaks

All other functions in the namespace after that one had the same problem

That error btw happened when I tried checking with cf

oh yea lol t/defn doesn't add a global annotation https://github.com/clojure/core.typed/blob/master/core/runtime.jvm/src/main/clojure/clojure/core/typed/macros.clj#L275

needs an ann

that's by design, so it's pretty useless now

(core.typed used to infer a def's type based on its initial value)

that's one of the design points that's up in the air atm

I see

fwiw, it's about the situation when you use set-key from another namespace

ann just updates the global environment, so you just need to eval the namespace

Sounds about right

t/defn needs to actually type check the var => transitively type check everything

which was a killer for performance

obviously also a good idea in many situations, but you didn't have the option to choose with t/defn 's behavior

But isn't the point about static type checking that it is allowed to have sorta bad performance?

haha

tell that to all the users that ran away

Hmm

I guess a problem was that core.typed threw away all the info between each invocation?

Of course, caching and validating that would be a huge undertaking on its own

that was one issue, that's gone now

that allowed transitive deps to be checked less often

but it didn't allow transitive deps to be omitted from checking altogether

I think the worry that core.typed is going to try and "check the world" is legit

and just literally checking one file is really compelling to me

and just trusting all annotations outside the ns

eliminates many-minute waits for initial check-ns's that don't really do anything, and can be delegated to CI

True, yes

Then again that makes it less type-safe ^^

yea it's a tradeoff

I tried uber-typesafe and I couldnt' pull it off with usable perf

see: first 5 years of core.tyepd

Yea, I remember

haha

And it was bleeding into all dependencies. "Oh, you want to use obscure-ns/whatever? Please add an annotation for half the ns", which is something you just can't pull off with an optional type system

if you care, should be easy to make you're own wrapper for t/defn that also emits an ann by reusing the machinery around the link above ^

yea

yea, and also "oh, you use this ns? let me try and type check it too!"

:no-check everything

just a nightmare

I mean even now I had to add annotations for two clojure.alpha.spec functions because I have s/def in my code

t/tc-ignore all spec forms imo 🙂

should work wrapping any number of top-level forms

you can only give garbage annotations anyway

I was being a little perfectionist and gave somewhat useful annotations 😛

oh what did you give?

(ann s/register (All [[a :< (U Kw Sym)]] [a Any -> a]))

ahhh yes ok

I also had to do (ann str/includes? [String String -> Bool])

hehe

Now, am I right that in the s/register example above, a can be Kw on the argument side and Sym on the return side in this case, and I'd need to make two annotations in a Union to cover that it returns Kw when given Kw?

what does s/register return?

at runtime

(stepping back for a sec)

It literally returns the argument again at the end. It is (defn register [k s] ... k)

I guess what I am thinking about are generics? Like in Java where you'd write "K register(K k, S s)"

ah. I would annotate it [(U Kw Sym) Any -> (U Kw Sym)] you only need the type variable if you're going to type-check code that uses s/register and cares exactly which keyword/sym you return.

Yes, I know I am being hypothetical here ^^ Just wondering.

you can also do (IFn [Kw Any -> Kw] [Sym Any -> Sym] [(U Kw Sym) Any -> (U Kw Sym)]) if you want to maintain the dependency between first arg and return

but back to your original q...

Yea but what if k could be half a dozen types

ok so your case is wondering whether (ann-form (s/register :a ...) Sym) would type check using that annotation

good question

I am basically wondering if there is a generics-like functionality in core.typed

K register(K k, S s) is (All [K S] [K S -> K])

erm, assuming K/S are type variables

Ah. So basically, my annotation is already correct in that sense, (ann s/register (All [[a :< (U Kw Sym)]] [a Any -> a])) does imply that if argument a is of type Kw the return type will also be Kw?

(or, of course, that the return type is a hypothetical subtype of Kw)

well, I'm not sure. the type information for a flows in from the type of the first argument and the expected type of the return. which is why I'm not sure if (ann-form (s/register :a ...) Sym) would be allowed

but I guess a would need to be (U ':a Sym)

which is not a subtype of Sym

so that would be disallowed

it's a good question, still thinking

I mean, in Java it would be clear - K register (K k, S s) guarantees that the return type K is the same or a subtype of the argument K, so when I give a string, I am guaranteed that the function will return a string or a subtype of string

the equivalent in java fwiw is (forget the syntax) <K super (U Kw Sym)> K register (K k, S s)

so we're on the same page

Hmm right, yes

And there I wouldn't know either if that would guarante the returned value to be of (sub)type of the argument given

ok. I think you're right. ((t/inst s/register Kw) ...) is guaranteed to return a keyword

core.typed has to basically choose a type for a

and you can only choose once, and a is simply substituted for the chosen type

I was lost in details about which type core.typed chooses

like, (s/register (ann-form :a (U Sym Kw)) ...) returns (U Sym Kw)

sorry, haven't thought about this stuff in a while

Ahh. Good, yes, that is what I was hoping for

great

It has been a long time that I spent time thinking about types, I gotta admit

😛

g2g nice chatting about types again! I get emailed about messages in this channel and I usually respond within 24hrs, or try the core.typed google group

Okay, see you! And thanks for your time and work!

cheers!

@ambrosebs hey! nice that you continue working on core.typed!

do you plan to port https://docs.racket-lang.org/turnstile/index.html to clojure?