Fork me on GitHub
#core-typed
<
2020-02-21
>
ambrosebs01:02:53

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

ambrosebs01:02:08

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

ambrosebs01:02:04

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

ambrosebs01:02:17

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

ambrosebs01:02:01

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

ambrosebs02:02:13

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

ambrosebs02:02:30

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

ambrosebs02:02:03

I think that's sustainable.

zilti10:02:11

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

jeroenvandijk10:02:20

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

ambrosebs23:02:26

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

ambrosebs23:02:34

it's on the roadmap

ambrosebs23:02:07

@zilti yea it all clicks together for me

ambrosebs23:02:21

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

ambrosebs23:02:48

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

ambrosebs23:02:59

so I've slowly been going towards cljc

jeroenvandijk23:02:37

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

zilti23:02:16

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

ambrosebs23:02:18

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

ambrosebs23:02:28

this is totally brand new and I barely understand it

ambrosebs23:02:40

but I do know spec2 syntax is extremely verbose

ambrosebs23:02:15

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

ambrosebs23:02:25

and I quite like typedclojure syntax

zilti23:02:49

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

zilti23:02:24

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

ambrosebs23:02:41

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

ambrosebs23:02:32

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

ambrosebs23:02:49

doesn't play well with type hints either aesthetically

zilti23:02:10

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

ambrosebs23:02:21

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

ambrosebs23:02:52

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

ambrosebs23:02:54

definitely a bug that they differ

ambrosebs23:02:23

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

zilti23:02:26

I ended up simply placing an ann right above each defn

ambrosebs23:02:08

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

ambrosebs23:02:56

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.

zilti23:02:00

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

ambrosebs23:02:36

which ones did you need?

zilti23:02:59

(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])
are the ones I made

ambrosebs23:02:00

some macros like reify aren't supported

zilti23:02:53

Though the ann for update I made is ugly

ambrosebs23:02:55

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

ambrosebs23:02:03

update is a whole nother thing

ambrosebs23:02:37

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

ambrosebs23:02:46

so that's a typedclojure 2.0 thing

zilti23:02:50

Just copy over the Haskell type def 😜

ambrosebs23:02:51

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

ambrosebs23:02:11

nah man, more like the typescript type

ambrosebs23:02:20

pulling out all the stops

zilti23:02:38

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

ambrosebs23:02:03

typescript has all the these typelevel operators that are pretty crazy

ambrosebs23:02:21

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

ambrosebs23:02:36

metaprogramming your types

ambrosebs23:02:56

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

ambrosebs23:02:04

so we really need type-level equivalents

zilti23:02:07

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

jeroenvandijk23:02:36

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

ambrosebs23:02:41

I'm hyperfocussed on bidirectional checking myself

jeroenvandijk23:02:56

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

ambrosebs23:02:05

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

jeroenvandijk23:02:26

Same with for ?

ambrosebs23:02:41

for's a beast for a different reason

jeroenvandijk23:02:46

(if you leave out :when etc

ambrosebs23:02:01

if is interesting because updating types of locals to check branches

zilti23:02:03

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

jeroenvandijk23:02:16

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

ambrosebs23:02:35

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

ambrosebs23:02:51

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

ambrosebs23:02:00

ie the functions are annotated

ambrosebs23:02:09

but that's why type checking clojure is so fun

zilti23:02:12

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

jeroenvandijk23:02:19

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

jeroenvandijk23:02:38

I think I could use that

ambrosebs23:02:18

hopefully within the year! 🙂

ambrosebs23:02:23

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

ambrosebs23:02:35

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

jeroenvandijk23:02:37

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

zilti23:02:00

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

jeroenvandijk23:02:21

what alternative are you thinking about?

zilti23:02:28

JavaFX e.g.

jeroenvandijk23:02:39

yeah for sure that would be an option too

jeroenvandijk23:02:52

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

jeroenvandijk23:02:00

you just need a browser

zilti23:02:15

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

zilti23:02:42

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

zilti23:02:01

AppImages are such a great thing

jeroenvandijk23:02:07

What if you want to edit on your mobile? 🙂

jeroenvandijk23:02:34

But i definitely see benefits with javafx

zilti23:02:41

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

zilti23:02:13

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

zilti23:02:35

What's Sci?

jeroenvandijk23:02:09

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

jeroenvandijk23:02:18

you don't feel the difference with normal clojure

jeroenvandijk23:02:45

It's a pretty cool addition to the Clojure community

jeroenvandijk23:02:57

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

ambrosebs23:02:13

holy crap that's cool

jeroenvandijk23:02:11

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

jeroenvandijk23:02:55

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

jeroenvandijk23:02:24

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

zilti23:02:40

I mean you can do that in the REPL, too

ambrosebs23:02:51

LOL core.async is included

zilti23:02:53

And check form by form using cf

jeroenvandijk23:02:24

like i said i'm a noob 🙂

jeroenvandijk23:02:46

i'll leave it to the experts

jeroenvandijk23:02:49

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

jeroenvandijk23:02:03

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

jeroenvandijk23:02:28

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

jeroenvandijk23:02:31

even looping is controlled

jeroenvandijk23:02:54

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