Fork me on GitHub
#core-typed
<
2024-03-08
>
Noah Bogart16:03:46

i was looking at the typedclojure readme today and it still points at the clojure/core.typed wiki. worthwhile to move things over/clean them up a bit?

ambrosebs16:03:51

I think I'd rather move them into the repo itself. it's just a big job I've been avoiding, but there's some useful nuggets in there.

👍 1
ambrosebs16:03:07

any help would be appreciated

👍 1
Noah Bogart16:03:22

it would certainly help with getting them nicely displayed on clojuredocs (if that's a goal of yours)

ambrosebs16:03:36

how does that work?

Noah Bogart16:03:12

i mean cljdoc, sorry

Noah Bogart16:03:40

cljdoc will analyze your jar to build the api reference docs, and it will also go to the associated git repo and use a doc/cljdoc.edn file to build "documentation" pages.

ambrosebs16:03:38

yeah that looks like a great idea

Karol Wójcik16:03:54

I’m dreaming about guardrails+core.typed to become a thing.

3
ambrosebs16:03:36

what's your vision?

ambrosebs16:03:00

guardrails syntax => static typing?

ambrosebs17:03:30

it just compiles to malli and spec right? there's early work on that here: • https://github.com/typedclojure/typedclojure/tree/main/example-projects/spec1-type-providershttps://github.com/typedclojure/typedclojure/tree/main/example-projects/malli-type-providers if you could tweak those examples to use guardrails syntax I'd be happy to add new example projects to the test suite.

Karol Wójcik17:03:19

Yes. In the end guardrails are backed by malli. I’m wondering if we can get all of the goodness of core.typed 😍 for free!

ambrosebs17:03:45

It's worth a shot! I need people to try it and report bugs, because I didn't fully implement the translation from malli to types https://github.com/typedclojure/typedclojure/blob/main/typed/malli/src/typed/malli/schema_to_type.cljc

Karol Wójcik17:03:15

I feel that most of the people want optional typing in Clojure, but till malli is alpha not so many are keen to invest time on it.

ambrosebs17:03:52

my hot take: there's a consistent desire for better error messages, I don't know if most people care how they get it. IMO a dev-only debug clojure jar that hardcodes error messages would go a long way.

👍 1
ambrosebs21:03:43

I've been thinking that for a long time and 1) it's not going to happen, 2) forking clojure is bad for the community. I'm thinking of resurrecting dynalint which hardcodes error messages. https://github.com/frenchy64/dynalint

Mateo Difranco16:05:03

I would also love to see guardrails support 🙂 Is adapting the example project to it enough to help?

ambrosebs17:05:47

yeah that's all that's needed. just add a new namespace in the spec/malli example projects with the equivalent guardrails forms.

ambrosebs17:05:04

If it doesn't work I will look at it

Zeniten19:03:37

I'm interested in Typed Clojure, and schema solutions like Clojure spec, Malli, and Schema, but I'm confused on how they relate to each other. I've read that Malli has some integration with Typed Clojure, and I've picked up that you've made some connection between Schema and Typed Clojure, Ambrose. Then there's also clj-kondo, how would you conceptually fit clj-kondo into the picture? I feel like all of these are merging together, would you say that's accurate? Is it natural for schemas to become "static typers" as time goes on? Some further questions that I thought of: • How does static typing, which I assume Typed Clojure is an example of, differ from what spec, Malli, and Schema are? • What can you do with static typing that you can't do with the kind of thing that spec, Malli, and Schema are, and vice versa? • I feel like static typing is something more. Are schemas like a "pseudo-subset" of static typing? (Sorry for being a bit all-over-the-place; I'm lacking in terminology, and I'm anxious to know more. 😅)

ambrosebs20:03:46

clj-kondo is completely static checking like Typed Clojure, except it's (currently) less ambitious in terms of expressivity (no polymorphism) and more successful in terms of usability (caching, performance, active community).

👍 1
ambrosebs20:03:00

Schema, Malli, and spec are pretty similar in that they do completely runtime checking. Malli and spec are basically the same in many ways. What sets them apart from schema is they have regular expressions for sequences and a better generative testing story. Also Schema's error messages are often great and readable.

ambrosebs20:03:39

There's a few bridges being built to take advantage of all the specs that already exist in schema, spec, and malli to get static type checking for free. Malli can output clj-kondo annotations. Typed Clojure can convert Malli and spec specs to types.

ambrosebs20:03:28

> How does static typing, which I assume Typed Clojure is an example of, differ from what spec, Malli, and Schema are? Typed Clojure and clj-kondo are static typing. they analyze the source code of your program before it's run and flag potential errors. Spec, malli, schema use dynamic verification. They don't have/need access to the source code of your program, and use purely runtime information to verify your program conforms to your spec. Like instrumenting functions and asserting specs just-in-time as the program runs, or generating examples to exercise functions.

💡 1
ambrosebs20:03:35

> What can you do with static typing that you can't do with the kind of thing that spec, Malli, and Schema are, and vice versa? It's a huge subject but there's really an entire spectrum between dynamic and static typing. there's not just two approaches. for example, many static type systems check as much as they can at compile-time and then emit runtime assertions to check the rest.

ambrosebs21:03:11

the way I see it is that they are complimentary approaches. sometimes you can prove something more convincingly with static typing, other times with dynamic testing or assertions. they both have their costs and benefits. dynamic is more probabilistic but more expressive. you often are constrained in what you can prove statically, but there's a bit more certainty (if you believe the type system is sound).

ambrosebs21:03:37

I think you're on the right track in terms of convergence. What I care about is verifying programs, and I want to use the right tool for the job. Ideally, the full spectrum of verification approaches are available for whenever they are needed.

Zeniten21:03:07

Great, that cleared up a lot. Thanks for taking the time, Ambrose! 🙂

🙏 1
1
leifericf06:03:39

Isn't performance one of the big topics surrounding static vs. dynamic typing? With static typing (and AOT compilation), more of the performance cost is paid upfront at compile-time, and the compiler can use type information to do some clever low-level optimizations that would be incredibly difficult or maybe even impossible to do at runtime. With dynamic typing, the JIT compiler/VM/runtime is burdened with more work when doing schema validation, etc.

Ben Sless12:03:37

Yes, although a static type system doesn't guarantee better performance, only that you CAN get the benefits of polymorphism and pay the cost at compile time. There's still plenty of performance to be gained in other means but that's orthogonal

👍 1