This page is not created by, affiliated with, or supported by Slack Technologies, Inc.
2020-02-22
Channels
- # beginners (43)
- # bristol-clojurians (2)
- # calva (11)
- # cider (10)
- # clj-kondo (3)
- # clojars (19)
- # clojure (93)
- # clojure-france (44)
- # clojure-nl (10)
- # clojure-uk (15)
- # clojuredesign-podcast (1)
- # clr (6)
- # core-typed (102)
- # data-science (1)
- # datomic (11)
- # docker (4)
- # emacs (12)
- # fulcro (27)
- # graalvm (6)
- # joker (1)
- # leiningen (4)
- # lumo (20)
- # nrepl (3)
- # off-topic (63)
- # parinfer (4)
- # reagent (40)
- # remote-jobs (2)
- # shadow-cljs (18)
- # spacemacs (7)
- # tree-sitter (7)
- # yada (3)
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
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
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))
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)
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
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
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 🙈
or even simpler (fn [a :- (U Str Int)] (if (integer? a) (inc a) (str/split "," a)))
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
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?
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
Nothing, but it made me think about type checking
I think the difference is that it is interpreted and not compiled?
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
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
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)
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
I would like to use the position as well. Like how clojure.spec has positions of forms
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)
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.
I'm really happy the Sci feature of being able to blacklist/whitelist functions. That makes it possible to reduce the potential problems
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
yeah exactly
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