Clojurians Log v2
core-typed
@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 🙂
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