Clojurians Log v2

@ambrosebs would typing clojure.set/rename-keys be a related problem space wrt inference of variables bound by other type variables (f-bounded polymorphism) isn't well supported

@djtango don't think so, is the current annotation not accurate enough?

clojure.set/rename-keys (t/All [x y] [(t/Map x y) (t/Map t/Any x) :-> (t/Map x y)])

Ideally we would like a more precise (dependently typed :)) version

yeah, not sure it needs f bounded polymorphism though

I haven't thought about it though, just my first impression.

I was imagining a type more like:

#_#_clojure.set/rename-keys (t/All [[map :< (t/Map t/Any t/Any)]
                                    [kmap :< (t/Map t/Any t/Any)]]
                                   [map kmap :-> (magic ...)])

my magic type ended up slightly ridiculous 🙂

#_(defalias RenameKeys
    (t/TFn [[map :< (t/Map t/Any t/Any)]
            [kmap :< (t/Map t/Any t/Any)]]
           (ReduceKV (t/TFn [map old new]
                            (If (Contains? map old)
                              (Assoc m new (Get map old))
                              m))
                     (Dissoc map (Keys kmap))
                     kmap)))
#_#_clojure.set/rename-keys (t/All [[map :< (t/Map t/Any t/Any)]
                                    [kmap :< (t/Map t/Any t/Any)]]
                                   [map kmap :-> (RenameKeys map kmap)])

might as well just inline the code. does anyone know similar examples in other type systems?

What is ReduceKV?

magic nonexistent thing that, if it exsted, would be reduce-kv at the type level, like clojure.core/merge => t/Merge.

it would great to have annotations that work for both the homogeneous and heterogeneous cases. right now, heterogeneous cases are mostly hardcoded in the type system.

the magic type might be the kind of thing that allows users to write their own heterogeneous operations.

for example, t/Merge is hardcoded in the type system, but given t/Assoc, t/Get, it might be possible to be a user extension.

I was thinking to write macros

I meant to ask, how does t/Get work?

the type of get does not involve t/Get

that's just a historical thing, I hardcoded get in the type system and then created t/Get later. at some point I will add the expected annotation.

just like assoc, which actually uses t/Assoc.

my current trajectory is to turn these opaque types into type parameters on IPersistentCollection etc.

e.g., clojure.core/get (t/All [m :< (ILookup ... Get ...), k] [m k -> (Get m k)])

Looking forward to this.

unrelated question, in my nvim CheckNs works fine but TypeAt always returns v:null

that's good news about CheckNs, go me for 8 year backwards compat. honestly forgot about the plugin!

I think I broke the TypeAt functionality.

:) what is your worflow like then?

I have a (is (check-ns ...) in the tests for the project. But it's not a great idea, since check-ns reloads files. it can mess with other tests.

I don't have a great answer.

I have the same

I attempted to create an entry point here, it's not quite what I wanted though https://github.com/typedclojure/typedclojure/blob/c0e0b8ac9ab5584204748b947f0b1c80bcb4eabd/typed/clj.checker/src/typed/clojure/main.clj#L136

or maybe I just moved on to the endless other work there is to do. it would be interesting to know if it's useful.

I spend all my time inside the type checker, which is only partially able to check itself. so I don't dogfood this aspect as much as I'd like.

you might find my experiment in type checking malli interesting https://github.com/frenchy64/malli/pull/1/files

that's about the closest I've come using the checker in anger recently

looks like that's a good example of using the exec fn.

and also how to split type checking across separate github actions jobs https://github.com/frenchy64/malli/pull/1/files#diff-8068abef2a43df385283c6bf7dd1b1c51f0a45aa8abb801d4d96fc1bef134795R62-R64

I got further than I remembered. But that doesn't help when you're sitting on a REPL on your own machine. For iterative development I just call (t/check-ns-clj), so basically what you do.

Thank you

1. yes. grep for t/TFn here for examples of type functions. t/Transducer is probably the most interesting https://github.com/typedclojure/typedclojure/blob/f22f2b75542d5fa3f8f3e8325fb9494f7799fcf1/typed/lib.clojure/src/typed/ann/clojure.cljc#L245-L249 2. inference of variables bound by other type variables (f-bounded polymorphism) isn't well supported. the other problem is the kind system is very ad-hoc, I happen to be working on this atm. I (think I) recently realized what the kind of dotted type variables (`:..`) which was a bit roadblock https://github.com/typedclojure/typedclojure/blob/f22f2b75542d5fa3f8f3e8325fb9494f7799fcf1/typed/lib.clojure/src/typed/ann/clojure.cljc#L981

I misread your Haskell example, I thought the <= was bounded polymorphism.

(t/defalias MyList
  (t/TFn [[a :< UpperBound, :variance ThisIsInferredSoCanOmit]]
         (t/List a)))

could you help me understand the haskell type? guessing these are GADT's?

this is the type of leftjoin in the Frames library.

in a few meeting will try to write suff up

my main priority is type checking idiomatic clojure code (still some ways to go), but I like to make sure I'm not shooting myself in the foot for such future extensions.

What I am trying to do is essentially to typecheck a piece of techml.v3.dataset

feel free to send or describe it

thanks, will do/ask when I run into issues. I think your typelevel constructs might just be enough.

have fun!

The runtime is also split so then you don't need to pull in the entire checker in "production".

which has a ton of dependencies

the typed.clojure namespace also lives in that jar. It gives macros to annotate things, such as t/ann for vars and t/ann-form for forms.

thankfully since core.typed became typedclojure, most of the wrapper macros in clojure.core.typed are not needed. so it's primarily for top-level annotations.

there's even a way to avoid using the "runtime" dependency now https://github.com/typedclojure/typedclojure/tree/main/example-projects/zero-deps

useful for libraries that need to distribute without runtime deps

and an "analyzer" outputs a convenient middleground between clojure code and java bytecode for programmatic manipulation. we have our own analyzer because the de-facto analyzer tools.analyzer is too aggressive in macroexpansion. but this is unrelated to how your clojure code compiles. the type checker only runs when you call t/check-ns-clj, so during normal loading the clojure compiler is always used.

during type checking, compilation looks like: read -> analyze (typed.clojure) -> type check -> back to clojure data -> clojure.core/eval usually it's: read -> analyzer (clojure.lang.Compiler) -> .eval

Interesting, thanks for explaining all of this. I appreciate it

Not clear what you mean by a runtime

(defproject a-project "0.0.1-SNAPSHOT"
  :dependencies [[org.clojure.typed/runtime.jvm "1.0.1"]]
  :profiles {:dev {:dependencies [[org.clojure.typed/checker.jvm "1.0.1"]]}})

If you mean https://github.com/clojure/core.typed/tree/master/typed/runtime.jvm that is pretty much core.typed

It is where the code that does the type checking lives

Oh, I see. so it still isn't a replacement for the clojure runtime, correct?

It is for some things, there are some macros in clojure.core that are used a lot that core.typed cannot really handle, the runtime contains replacements that it can

Oh I see