Fork me on GitHub
#core-typed
<
2020-02-22
>
zilti00:02:51

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

zilti00:02:17

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

jeroenvandijk00:02:42

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

jeroenvandijk00:02:19

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

jeroenvandijk00:02:09

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

ambrosebs00:02:32

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

ambrosebs00:02:13

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

ambrosebs00:02:23

just less rigorous soundness xD

ambrosebs00:02:27

so I'm a fan

ambrosebs00:02:33

g2g have a good night

ambrosebs18:02:33

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.

ambrosebs18:02:09

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

ambrosebs18:02:02

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

ambrosebs18:02:09

than rewriting typed clojure!

ambrosebs18:02:55

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

ambrosebs18:02:11

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

❤️ 16
jeroenvandijk22:02:36

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))

jeroenvandijk22:02:04

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?

ambrosebs23:02:49

@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.

ambrosebs23:02:02

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

ambrosebs23:02:28

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

ambrosebs23:02:14

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)

ambrosebs23:02:04

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)

ambrosebs23:02:29

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

ambrosebs23:02:37

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.

jeroenvandijk23:02:30

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

ambrosebs23:02:06

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

jeroenvandijk23:02:22

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

ambrosebs23:02:14

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

ambrosebs23:02:24

erm. not quite as hard. but similar solution.

jeroenvandijk23:02:31

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 🙈

ambrosebs23:02:04

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

ambrosebs23:02:22

you can use fast and loose reasoning with immutable data structures

ambrosebs23:02:37

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

ambrosebs23:02:48

that kind of stuff is pretty common

ambrosebs23:02:04

at least of that flavor

ambrosebs23:02:19

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

ambrosebs23:02:36

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

ambrosebs23:02:01

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

ambrosebs23:02:14

the tech behind that is called occurrence typing

ambrosebs23:02:45

it basically uses propositional logic to update local variables' types

ambrosebs23:02:25

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

ambrosebs23:02:36

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

jeroenvandijk23:02:11

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

jeroenvandijk23:02:39

Is there something like just in time type checking?

ambrosebs23:02:49

dependent type checking, maybe?

ambrosebs23:02:56

that interleaves evaluation and type checking

jeroenvandijk23:02:22

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

ambrosebs23:02:43

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

jeroenvandijk23:02:46

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

ambrosebs23:02:02

what does sci have?

jeroenvandijk23:02:22

Nothing, but it made me think about type checking

ambrosebs23:02:35

oh I mean what features compared to clojure?

ambrosebs23:02:47

does it have all the features I listed?

jeroenvandijk23:02:30

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

ambrosebs23:02:41

ahk. so it's just the same language

jeroenvandijk23:02:40

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

ambrosebs23:02:29

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

ambrosebs23:02:12

I'm extremely ambitious with my type checking work

ambrosebs23:02:23

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

jeroenvandijk23:02:19

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 :)

jeroenvandijk23:02:16

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)

ambrosebs23:02:57

yea this looks great

jeroenvandijk23:02:00

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

ambrosebs23:02:54

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

ambrosebs23:02:35

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

jeroenvandijk23:02:45

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

ambrosebs23:02:56

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

ambrosebs23:02:05

you can't cast an Int to a String

ambrosebs23:02:24

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

ambrosebs23:02:59

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)

ambrosebs23:02:01

stuff like that

ambrosebs23:02:24

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

ambrosebs23:02:42

so I think your approach is a great idea

jeroenvandijk23:02:17

Thanks! I hope it has some practical value later

ambrosebs23:02:49

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

ambrosebs23:02:54

Dialyzer uses that iirc

jeroenvandijk23:02:58

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

jeroenvandijk23:02:12

Ah interesting

jeroenvandijk23:02:35

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

jeroenvandijk23:02:50

So a nice clojure sandbox

ambrosebs23:02:53

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

ambrosebs23:02:06

without having to use cljs

ambrosebs23:02:13

even that is too much

jeroenvandijk23:02:53

Yeah I think this has many applications

jeroenvandijk23:02:48

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

jeroenvandijk23:02:54

something like that

jeroenvandijk23:02:19

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

jeroenvandijk23:02:28

self-hosted cljs was still a pain