Fork me on GitHub
#core-typed
<
2022-04-08
>
ambrosebs01:04:04

@emccue I've exposed annotating Java classes to users. There's a new macro called typed.clojure.jvm/override-class. No docs, but I've moved all the base env to use it, https://github.com/typedclojure/typedclojure/blob/6119fc4d766d16f68b61e7f885ce8822fb16254c/typed/lib.clojure/src/typed/ann/clojure/jvm.clj#L29.

1
👀 1
emccue00:04:49

Hmm, so variance of generics for java classes is/can be different from the variance you'd see in java

ambrosebs02:04:18

Yeah, I haven't attempted to incorporate generics from Java types.

ambrosebs02:04:56

Mostly because it would take a lot of work to fully emulate how wildcards are inferred on method invocations.

ambrosebs02:04:51

Typed Clojure's view of all Java types and methods is pre-generics.

ambrosebs03:04:30

So not just the variance can be different, you can annotate completely unrelated parameters to the the generics.

ambrosebs03:04:24

Surprisingly this hasn't been much of an issue in my experience. Often I need to tell Typed Clojure that a particular method returns non-nil via typed.clojure.jvm/non-nil-return. It would be handy to know how to infer that information automatically.

emccue03:04:21

I think on the Java side JSpecify is the current space where work on that is being done.

emccue03:04:05

If they get their stuff together, cribbing the rules they come up with would be the way to go. Before that its probably too much of a distraction

👍 1
ambrosebs14:04:51

@emccue What's your opinion on the relevancy of Java generics to Clojure programmers?

emccue14:04:38

Probably not that relevant in practice.

emccue14:04:02

I can't justify that one way or the other though

ambrosebs21:04:18

Fair enough. I think there's a handful of classes that deserve support as they're usually used for optimizations. eg., AtomicInteger, ArrayList.

emccue17:04:55

From my perspective, the most important java classes outside the stdlib are the "library for X" stuff that there isn't likely to be a clojure version of

emccue17:04:46

For instance, you might be able to do some voodoo with cognitect.aws and this new type provider scheme, but for GCP if their classes have generic builders or similar in the apis that is would be a pain point

emccue17:04:52

(if that makes sense)

ambrosebs02:04:57

❤️ 2
😮 1
👏 1
rayat22:04:58

Hey, idk if this is stupid, but what does Schematic do that core-typed doesn't, and vice versa ? (esp once/if the spec->annotation thing gets 'complete')

emccue00:04:22

The answer is going to be "one does runtime validation, the other entirely static validation" - but what library is schematic?

👍 1
rayat20:04:44

Thanks for the response @emccue somehow my brain skipped a cycle and I wrote schematic, when I meant https://github.com/arohner/spectrum, somehow 😅

ambrosebs21:04:36

@U037TPXKBGS spectrum and Typed Clojure (broadly) use the same approach.

ambrosebs21:04:38

It's hard to summarize the differences succinctly. Like comparing Flow lang with Typescript. They have similar goals, completely different solutions.

1
ambrosebs21:04:16

I think it's fair to say Typed Clojure has much loftier goals of correctness, for better or worse. See papers: https://ambrosebs.com/

ambrosebs21:04:08

That means that types are much more precise.

ambrosebs21:04:08

I wouldn't be surprised if the language in Spectrum's readme about avoiding "100% correctness" is a dig at Typed Clojure. Allen used it a lot at circleci.

😆 1
rayat01:04:02

It also looks like it's not particularly active anymore. And before your spec->type endeavor, was much more clearly distinct in approach. I also just noticed you've contributed a commit to that repo yourself haha. I've been messing around with clojure-lsp, compliment, suitable, orchard, cider-nrepl a lil bit while I try to figure out https://github.com/BetterThanTomorrow/calva/issues/1663, and really wish I had access to static type defs or more thorough tests, for everything I'm seeing in those repos. I've seen the Maybe Not talk a bunch and I get and indeed like the idea of using positive predicates to build up the "herd" of the set of possible thingies that a "type" could filter, but it's been hard to get a grasp of what sorts of things to look for when I don't even know what is possible to ask about. So then, as for your proposal exercise of trying to type a library, the ones listed would prob be the first or only non-application clojure code I've ever really delved into enough to grok. Would they be a good jumping-off point then?

ambrosebs14:04:04

> And before your spec->type endeavor, was much more clearly distinct in approach. Yes, Spectrum still has a few neat ideas I want to borrow. I think the main distinguishing features are that Typed Clojure has polymorphic types and occurrence typing (ie., ability to annotate custom predicates and automatic understanding of control flow) which IME are key to modeling clojure programs to a high degree of accuracy. > I've seen the Maybe Not talk a bunch and I get and indeed like the idea of using positive predicates to build up the "herd" of the set of possible thingies that a "type" could filter, but it's been hard to get a grasp of what sorts of things to look for when I don't even know what is possible to ask about. Yes, it's a cool analogy but only applies to first-order data. You can only write a predicate for something that never changes or lacks behavior. eg., number, strings, the class of a local, nested (finite!) immutable collections of those things. Can't write predicates for atoms, functions, channels, infinite or mutable lists. For those things you need contracts that monitor values (see Racket's impersonators & chaperones). Spec rejects those ideas in part for performance reasons. Instrumentation is inspired by a [germ](https://www.scholars.northwestern.edu/en/publications/contracts-for-higher-order-functions) of those ideas, and fspec is an interesting example of borrowing from both approaches. Obviously, static typing is an alternative strategy. I also tried to monitor Clojure values but it was mostly a failure, and I think spec's approach is right for a hosted lang (Racket modified their VM to support monitors). Hopefully that helps... > Would they be a good jumping-off point then? Probably the example projects in the Typed Clojure repo would be a good first step. If you try and check something complicated that would be easy in say Haskell (eg., continuations, monads), it will probably end in frustration. I don't really recommend doing that. How about [clj-time](https://github.com/clj-time/clj-time)? I think that's a good mix of interesting, useful, and achievable.

1
didibus18:04:24

On a side note, I think the truth is no one cares about correctness that is looking for static types in Clojure. They care about "refactoring made easy". That's why clj-kondo got so popular. People miss the IDE conveniences that a static typed language like C#, Java, Kotlin, Typescript+VSCode provides them. I know correctness matters to some extent for correct refactoring or type errors reporting. But my hunch is for users it is much more about IDE features such as refactoring, and not so much about bug-free code.

💯 1
1
didibus18:04:18

Even the hold-outs, when I talk to them, they ask me things like: What do you do if you change a User in a backwards breaking way, and now the key on the User map is not found in the same place it was, say if you move customer-name from User to Profile and have Profile on User:

{:customer-name "Joe"}
;; to
{:profile {:customer-name "Joe"}}
How do you figure out where to refactor for this change? This is the kind of thing I feel people want "static types" for in Clojure. It's not so much the static types they want, as a way to easily refactor this.

❤️ 1
rayat18:04:38

That's an important point. I really enjoy convoluted typescript annotations because I get crazy error checking and auto complete and because they're fun to reason about, but what I really needed, and what made management approve typescript, is easy refactoring. Not only does it make refactoring easier, faster and more trustworthy, it sometimes brought the barrier down to the point where refactoring was even possible, certainly from a justification and time standpoint.