@zilti haha good question. depends on your perspective. xD required a good amount of insight but I'm using spec2's extensibility as intended

I managed to verify clojure.core/map was (All [x y] [[x -> y] (Coll x) -> (Coll y)]) by effectively calling (conform (All [x y] [[x -> y] (Coll x) -> (Coll y)]) map) but with gnarlier syntax for the spec

instead of generating values, we need to generate types (specs) to instantiate x and y

that would be a super compelling story for typed clojure if I can pull off the runtime side of things

2.0 branch lives here now https://github.com/typedclojure/typedclojure

trying to figure out how to deploy it to clojars.. having trouble

going back to the typed groupId and namespace. probably typed/clj with root namespace typed.clj and typed/clj.check with ns typed.clj.check

then library annotations will live in typed.lib/clojure typed.lib/core.async etc, with wrappers and stuff living under typed.lib.clojure.core/doseq typed.lib.clojure.core.async/go etc

I think that's sustainable.

Yea, having core.typed generate specs, mainly for the parts that can't be verified at compile time, would be one helluva feature

Crazy idea.. not sure, is it possible to have a cljc core.typed library? It would be usable from CLJS in the browser, nodejs and Graalvm. We could have type inference in small setting? Not sure if this is stupid to suggest, but I really would like to have it

@jeroenvandijk actually that's behind my obsessive partitioning of typed clojure into "jvm" "js" etc

it's on the roadmap

Awesome!

@zilti yea it all clicks together for me

you could throw away the type checker and still have incredible value

@jeroenvandijk I really want a web demo, I've wanted one since 2013-ish haha

so I've slowly been going towards cljc

If I can help somehow with testing please let me know. It think it will be huge

Will core.typed 2 be syntax-compatible to 1.0 btw?

I have no idea. this whole spec2 thing just popped up a few days ago after about 5 years of thinking

this is totally brand new and I barely understand it

but I do know spec2 syntax is extremely verbose

since my goal is a one-one spec2<==>typedclojure type correspondance, I assume we can easily write a type->spec2 function

and I quite like typedclojure syntax

Yea, the conversion should be rather straightforward. I mean, I did/do it by hand for a few types in core.typed 1 currently

But I miss the varname :- type syntax being equivalent to t/ann

the research I need to do now is how to do these properly in spec2: All, TFn, type variables, t/inst

yea that should be easy to do. it's kinda gross to me tbh

doesn't play well with type hints either aesthetically

Hmm. I mean, in the end, you can leave it to the user which variant they use. But I found it a bit confusing (maybe because I was using core.typed before) that the :- notation and the ann notation differ

but it definitely makes a lot of sense for scoping type variables. you don't want the names of your local type variables to be determined in another file ...

oh yea, that was a consequence of a series of design decisions

definitely a bug that they differ

we can have a defn wrapper that emits (do (ann ..) (c.c/defn ...)) now

I ended up simply placing an ann right above each defn

Yea

yea I recommend that. but inline types are super popular so that's fine.

I think I originally wrote the :- macros back in the day and schema based its syntax on that. then everyone make spec wrappers that work that way.

I also noticed there are still annotations for some clojure.core functions missing in 1.0.0

which ones did you need?

(t/ann clojure.core/update [Coll Any [Coll -> Any] -> Any])
(t/ann clojure.core/re-pattern [Str -> java.util.regex.Pattern])
(t/ann clojure.core/slurp [Str -> Str])

some macros like reify aren't supported

Though the ann for update I made is ugly

ah yea. if you want to contribute the last two feel free

update is a whole nother thing

most of my phd is based on problems like how to type update

so that's a typedclojure 2.0 thing

Just copy over the Haskell type def 😜

something like (All [m k v o z ...] [m k [(Get m k) z ... z -> o] z ... z -> (Assoc m k o)]) would satisfy me LOL

nah man, more like the typescript type

haha

pulling out all the stops

I have no clue about typescript ^^ (neither about Haskell, even though I've read about it a bit though)

typescript has all the these typelevel operators that are pretty crazy

like (Domain [Int -> Str]) => Int

metaprogramming your types

and so many functions in clojure are designed with assoc/get/update as building blocks

so we really need type-level equivalents

I don't know that much about type systems in general, just some silly facts like how Scala's is turing complete apparently

What if you had a tiny subset of Clojure e.g. just (str (+ 2 (inc 4)) . Would that be easy to type check?

I'm hyperfocussed on bidirectional checking myself

so (+ (str "somethin") 2) woudl fail

@jeroenvandijk as soon as you have if and fn you're in trouble

Same with for ?

for's a beast for a different reason

(if you leave out :when etc

if is interesting because updating types of locals to check branches

for is basically an entire logic DSL with all the clauses you can include

Ok but you are saying if it's just function calls that's possible?

fn is interesting because of higher-order functions eg., how to know the type of x in (map (fn [x] ..) ..)

if you just have function calls with annotations, it's easy

ie the functions are annotated

but that's why type checking clojure is so fun

A lot is possible. I mean, you can formally verify that a turing complete subset of the Ada language is bug-free

I think a web demo with the easy cases is already of tremendous value

I think I could use that

hopefully within the year! 🙂

🎉

one thing I'm not sure about is what the differences need to be between typed.clj and typed.cljs

and typed.clj.check and typed.cljs.check

My desire is to create a web framework that allow novices to edit stuff via a web editor. They would only be allowed to do the simple stuff. So super useful if it had type checking

ah nice

Why does it all always have to be in a browser though

what alternative are you thinking about?

JavaFX e.g.

yeah for sure that would be an option too

but the web gives the benefit of lower requirements on the client machine

you just need a browser

cljfx ftw

Actually I am currently looking into creating an editor with syntax highlighting, since there is a mature rich text component with a code edit mode

Well, download and execute is all that's needed these days. At least on MacOS and Linux... Windows, as always, is making lifes difficult

AppImages are such a great thing

What if you want to edit on your mobile? 🙂

But i definitely see benefits with javafx

Just compile the same app for mobile... Granted, the Graal-based plugin to do that is still under heavy development, but they're on their way

Though I have no idea if Clojure's eval is possible in a Graal native compiled binary

Sci?

What's Sci?

ah 🙂

https://github.com/borkdude/babashka

it has another library called sci underneath. Eval in browser, graal, node etc

you don't feel the difference with normal clojure

#babashka

It's a pretty cool addition to the Clojure community

It's the reason i'm thinking of building a web framework

holy crap that's cool

It's interpreter might also be interesting from a type checking perspective

you can type check per form. I don't know much about type checking but as a noob I feel this makes it easier. Type checking the code while interpreting it

So you don't have to say everything ahead of time

I mean you can do that in the REPL, too

LOL core.async is included

And check form by form using cf

like i said i'm a noob 🙂

i'll leave it to the experts

The cool thing is that you control what functions can be executed. So you could say i don't know what the type it is, let's just try it

If you don't have side effects that would not be a weird strategy

since you can control the fn's that are evaluated you know if there are gonna be side effects

even looping is controlled

I suppose that's different than checking a form in the repl