Fork me on GitHub
#core-typed
<
2020-02-14
>
ambrosebs14:02:46

@zilti anything I can help with?

zilti14:02:21

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?

ambrosebs14:02:45

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

ambrosebs15:02:07

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

ambrosebs15:02:14

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

zilti15:02:29

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

ambrosebs15:02:13

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

zilti15:02:31

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

ambrosebs15:02:47

yea.. one sec

zilti15:02:53

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

ambrosebs15:02:11

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

zilti15:02:40

Ooh yes, that works 🙂

ambrosebs15:02:54

except use IFn

ambrosebs15:02:04

sorry, woefully out of date

zilti15:02:05

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

zilti15:02:00

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]])

ambrosebs15:02:28

is that with t/defn ?

zilti15:02:35

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

zilti15:02:54

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

zilti15:02:56

That error btw happened when I tried checking with cf

ambrosebs15:02:02

needs an ann

ambrosebs15:02:23

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

ambrosebs15:02:43

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

ambrosebs15:02:04

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

ambrosebs15:02:37

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

ambrosebs15:02:54

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

zilti15:02:56

Sounds about right

ambrosebs15:02:14

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

ambrosebs15:02:34

which was a killer for performance

ambrosebs15:02:04

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

zilti15:02:08

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

ambrosebs15:02:26

tell that to all the users that ran away

zilti15:02:06

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

zilti15:02:18

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

ambrosebs15:02:24

that was one issue, that's gone now

ambrosebs15:02:44

that allowed transitive deps to be checked less often

ambrosebs15:02:57

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

ambrosebs15:02:23

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

ambrosebs15:02:35

and just literally checking one file is really compelling to me

ambrosebs15:02:44

and just trusting all annotations outside the ns

ambrosebs15:02:19

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

zilti15:02:39

True, yes

zilti15:02:00

Then again that makes it less type-safe ^^

ambrosebs15:02:35

yea it's a tradeoff

ambrosebs15:02:58

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

ambrosebs15:02:06

see: first 5 years of core.tyepd

zilti15:02:13

Yea, I remember

zilti15:02:01

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

ambrosebs15:02:25

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 ^

ambrosebs15:02:14

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

ambrosebs15:02:18

:no-check everything

ambrosebs15:02:22

just a nightmare

zilti15:02:50

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

ambrosebs15:02:19

t/tc-ignore all spec forms imo 🙂

ambrosebs15:02:33

should work wrapping any number of top-level forms

ambrosebs15:02:50

you can only give garbage annotations anyway

zilti15:02:06

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

ambrosebs15:02:14

oh what did you give?

zilti15:02:45

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

zilti15:02:56

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

zilti15:02:20

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?

ambrosebs15:02:58

what does s/register return?

ambrosebs15:02:20

(stepping back for a sec)

zilti15:02:32

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

zilti15:02:57

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

ambrosebs15:02:58

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.

zilti15:02:24

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

ambrosebs15:02:42

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

ambrosebs15:02:50

but back to your original q...

zilti15:02:26

Yea but what if k could be half a dozen types

ambrosebs15:02:17

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

ambrosebs15:02:31

good question

zilti15:02:42

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

ambrosebs15:02:39

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

ambrosebs15:02:03

erm, assuming K/S are type variables

zilti15:02:42

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?

zilti15:02:14

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

ambrosebs15:02:49

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

ambrosebs16:02:35

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

ambrosebs16:02:41

which is not a subtype of Sym

ambrosebs16:02:47

so that would be disallowed

ambrosebs16:02:19

it's a good question, still thinking

zilti16:02:26

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

ambrosebs16:02:34

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

ambrosebs16:02:44

so we're on the same page

zilti16:02:10

Hmm right, yes

zilti16:02:40

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

ambrosebs16:02:58

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

ambrosebs16:02:14

core.typed has to basically choose a type for a

ambrosebs16:02:34

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

ambrosebs16:02:50

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

ambrosebs16:02:30

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

ambrosebs16:02:46

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

zilti16:02:59

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

zilti16:02:19

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

ambrosebs16:02:58

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

zilti16:02:19

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

whilo19:02:21

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