Clojurians Log v2

No, sounds pretty familiar. I also really discovered a cider feature recently that lets you mark functions in your code, and when you do something in the REPL that calls that function, CIDER will live-display the variable values inside your code

But maybe I gotta try it. Maybe it throws stuff at me that makes me reconsider

also @ambrosebs maybe an inspiration for your web type checking https://borkdude.github.io/sci.web/

Do you know about clj-kondo btw? It's by the same guy

He does simple type checking (effective, but probably not allowed to call it type checking)

#clj-kondo

yea @borkdude reached out to me a few days ago about clj-kondo

it's an opt-in linter, which is basically what typed clojure is 🙂

just less rigorous soundness xD

so I'm a fan

g2g have a good night

bye!

good night!

I just crossed the threshold of "holy shit I'm going to have to rewrite typed clojure", and I didn't like it at all. Taking a step back to figure out how to embed what I need into our normal type syntax so then we can generate specs (eg., specify custom generators) and then I'm going to write type->spec, and spec->type transformations.

effectively to make generators work with polymorphic functions I needed a subtyping hierarchy for spec that exactly corresponds to typed clojure's subtyping.

so this is much easier: (defn subspec? [s1 s2] (subtype? (spec->type s1) (spec->type s2))

than rewriting typed clojure!

so it seems likely the 1.0 <-> 2.0 syntax will be similar for those reasons @zilti

also, thanks all for hanging out in this channel, it really helps to know I'm not in a vacuum

I'm not sure if I understand above, apologies for my ignorance. I was thinking about the things you said about how hard it is to have to type check update-in and higher level functions. Is this because in theory you have to support weird things like (update-in {} [:a] update-in [:b] update-in [:c] update-in [:d] (fnil inc 0))

If so, my naive brain thinks a more constrained version of Clojure could be a lot easier to type check? So maybe easier to make a constrained version of Clojure?

@jeroenvandijk yea the nested update-in's are really really hard and interesting. And the constrained version of Clojure you're talking about is effectively the subset that core.typed <=1.0 supports. The secret weapon we have is that I spend 5 years doing a phd researching how to tackle exactly the problem of how to support a full clojure language.

IMO Clojure at its heart is about higher-order functions and immutable reasoning about data structures. we can't really get away from that. eg., even in babashka, all the examples use higher-order functions

I have a pretty good idea how to type check any combination of nested update-in's or whatever using symbolic execution and following the implicit data flow in polymorphic types

even a simple expression like (if (integer? x) (inc x) (str x)) is mandatory for a clojure type system to be able to check. that brings a lot of complexity (that thankfully Typed Racket already solved)

I personally don't think there is a subset of clojure that is particularly easier to type check (at least to the rigor that would satisfy me)

you basically need to take away all the features that make it resemble clojure

if , fn , higher-order functions, immutable data structures (and reasoning about them) and macros are extremely important to clojure. and that combination is what's so hard about it.

Thanks for explaining! I really have a poor idea of what problems you have needed to tackle and are trying to tackle

totally

and it's really cool you realize that nested update-in's are hard. it took me a long time to even think of those cases

hehe it's only because you mentioned it I thought of that example. In that notation it is actually not super visible that it has several orders

xD

but like (update-in m [:a :b] dissoc :b) is just as hard and much more realistic

erm. not quite as hard. but similar solution.

I'm suprised that if is causing so many problems. I can imagine the higher order functions, but I have no feeling with if yet. I built a very simple type checker today and if seems not too bad. But I cannot evaluate anything so what am I saying 🙈

yea, think about (fn [{:keys [a] :as m}] (when a (:a m)))

you can use fast and loose reasoning with immutable data structures

like knowing that a is non-nil means you also need to update m

that kind of stuff is pretty common

at least of that flavor

or even simpler (fn [a :- (U Str Int)] (if (integer? a) (inc a) (str/split "," a)))

a is Int in the then branch, but it's Str in the else

and you must update its type otherwise the branches won't type check

the tech behind that is called occurrence typing

it basically uses propositional logic to update local variables' types

like at first we know a :- (U Str Int) , but we learn a :- Int in the then branch, and a :- (Not Int) in the else branch

and if you smash all the info together, you get the types you need

It sounds super complicated and I really have no clue about all this, but super interesting nonetheless!

Is there something like just in time type checking?

dependent type checking, maybe?

that interleaves evaluation and type checking

I was thinking of having a sci like interpreter that does some basic type checking and gives type feedback when it comes accross incompatible types

there are also systems that check what it can at compile time, and then emit assertions to ensure the stuff it can't verify at runtime

I have the ignorance is bless advantage, I really have no clue

what does sci have?

Nothing, but it made me think about type checking

oh I mean what features compared to clojure?

Ah ok

does it have all the features I listed?

I think the difference is that it is interpreted and not compiled?

ahk. so it's just the same language

That's the intention at least. It is still new so some macros are missing. And I recently added a check for the number of args to if. But all in all it's getting pretty feature complete

ok interesting. I'd encourage you to try your hand at type checking it.

I'm extremely ambitious with my type checking work

so it's hard for me to relate to what you need

I just think the bare minimum would already be of incredible value in a basic context. I'm thinking of creating a web framework where I also different experience levels. So a novice would not have access to update-in . Maybe if though :)

Btw this is my weird approach I tried today https://gist.github.com/jeroenvandijk/aac0d4373ede06aea927840f3fd41faf

ah nice

it's nothing serious, but I thought of combining type checking with the interpreter. So if it is hard to type checking just run it throught the interpreter and see what comes out (given no side efffects)

yea this looks great

But looking at the code of Sci I have a long way to go 🙂 And then i might realize that i have to solve all the problems you want to solve

I think the interesting design point on a system like yours is deciding when to warn the user.

Yeah indeed

IIRC Java has some interesting rules for when a cast is allowed

I would like to use the position as well. Like how clojure.spec has positions of forms

you can only cast to a type that is a subtype of its static type

you can't cast an Int to a String

might be remembering it wrong. but that's the gist of the tradeoff you have to make

so you might not warn if you're expecting Str and you get (U nil Str). But warn if you get Int. But don't warn if you get (U Str Int)

stuff like that

there's probably a nice balance that can weed out many small bugs

so I think your approach is a great idea

Thanks! I hope it has some practical value later

"success typing" is a related area. it only throws a type error if it's guaranteed to blow up at runtime.

Dialyzer uses that iirc

I'm really happy the Sci feature of being able to blacklist/whitelist functions. That makes it possible to reduce the potential problems

blacklist?

Ah interesting

it has deny and allow (https://github.com/borkdude/sci#usage)

also it can control how many iterations it can do. To prevent endless loops for instance

So a nice clojure sandbox

oh man. now I get it. this throws away all the issues with sandboxing on the JVM

mind blown

without having to use cljs

yeah exactly

even that is too much

Yeah I think this has many applications

So I want to use Sci for novices and say hey you can use the 40 function specifically for web templates

something like that

It is also a much better eval strategy than cljs had with self-hosted

self-hosted cljs was still a pain