Thanks.

it would also motivate people to write type signatures from the get go

In terms of running typedclojure without a REPL, that's not going to happen yet. Too much runtime information is used currently. I haven't looked into converting clj-kondo annotations to typedclojure yet. In terms of piggybacking off clj-kondo's caching and automatically type checking when clj-kondo senses a change, I briefly looked into it but decided to build a more robust classpath watching system native to typedclojure. The prototype is here https://github.com/typedclojure/typedclojure/blob/main/typed/clj.checker/src/typed/clojure/main.clj#L136

here's an example using it as an :exec-fn https://github.com/typedclojure/typedclojure/blob/2ab74a28829d3e0c020d97df80fe9457072258c5/deps.edn#L71-L157

there's also typed.clojure/check-dir-clj for checking directories of code. So there's a bunch of small pieces there, but no coherent story yet.

I think caching type checking results will be very important given the liberties I'm taking trading performance to type check more expressions (symbolic execution). So I think this part will need to be carefully designed, and then retrofitted to clj-kondo integration.

but given the fact that we need a REPL, it might be a non-starter. we'll see.

turnstile is great. You can build custom typing rules for macros in typedclojure but they only fire during type checking. So unlike turnstile, you don't have access to the type checker during normal expansion/compilation.

typedclojure is just a linter in that respect. there are various experiments in combining the two (there's an unused extensible #lang system in typedcloure), but in the end they interfere with IMO one of the strongest features of typedclojure which is you can just turn it off by simply compiling the file as usual. checking is completely optional. so I've been leaning into complete separation of runtime expansion and type checking expansion, and haven't fully explored a turnstile-like approach, but the pieces are there.

how hard is it to go into the direction of dependent types?

i would like to have a general relational abstract interpretation framework for clojure

to allow things like partial evaluation, which works remarkably well if you know that expressions are pure

could you drop an example and I'll think about it

have you seen will byrds work on barliman and relational scheme?

I saw the talk IIRC

at a conj

right

i think a stack of languages like this (e.g. like a fused nanopass stack) for a compiler framework would be very powerful to build runtimes and inference engines

mostly i am wondering whether you are interested in a set of general purpose libs for interpreter building including type checkers

which do bidirectional abstract interpretation usually

I kind of understand those words but I'm lacking a precise understanding of them

on a basic level i would appreciate tooling to build towers of interpreters

i think racket and scheme have quite a bit of work there

and i think you know more about the technical details than i do probably

i have built this multipass compiler https://github.com/plai-group/daphne with aggressive partial evaluation

and compile neural network architectures for probabilistic inference basically

(writing my thesis about it atm.)

but i have not done a lot pl work beyond that yet

are nanopass and towers of interpreters related?

they implement towers of languages

nanopass fuses the compiler so that you don't have to run each pass explicitly

but are as efficient as a one/few pass compiler

ah so you use nanopass to efficiently collapse the tower?

my tower is not that high

haven't been able to put in effort into better PL abstractions

I just meant in general, trying to unrust my PL knowledge 🙂

that is why i am reaching out to you

right

what would you need to have better symbolic interpretation?

e.g. to facilitate stronger forms of logic

I basically just implement beta reduction. what are other strategies?

i see. i thought that ghc and some other compilers can also infer backwards from return values to inputs (and any other direction)

i guess most type checkers propagate forward though

ah yes. typedclojure is just forwards.

mostly because local type inference is eager in that way

my symbolic execution amounts to little tricks delaying type checks until local type inference can kick back in again

i see

makes sense

have you thought about dependent types? f* or lean can discharge to z3

it's not my area no.

meaning that they have abstractions over representing the type constraints

ok

spec is very dependent type like

I think occurrence typing might be roughly related.

for example you can learn the length of a vector and assert that you only nth a valid length.

that has a flavor of dependent types but the formalism is probably very different

plus all the hacks/extensions I've made might make the research irreconcilable with my impl

there's a lot of overlap between spec and typedclojure's types, so it might fit your conception. I don't have a strong sense of when you're allowed to use the Dependent term to characterize a type system.

though I'm sure it's very specific and not related to my work

what part of spec says dependent to you?

i can define types with predicates that are turing complete

ok yep that makes sense.

I mean a symbolic closure type is just code that we beta expand with types. surely I'm flirting with that idea at least.

I never understood how checking and evaluation actually is interleaved in dependent typing, does the checker literally run during runtime?

I know turnstile can check during a macro expansion, but does it check during runtime?

or do turnstile rules just expand to code that checks at runtime?

perhaps I'm thinking of that "other" more recent dependent type system in racket. I think it starts with a C.

erm maybe I'm just thinking of https://www.williamjbowman.com/resources/wjb2019-depmacros.pdf

Cur

we might need to circle around the topics you want to talk about until I catch up. I think you're right that I probably can help.

oh yeah, william is here in the department

yes, i think you need to add runtime checks

i would rather think of runtime as a continuation of compile time

i think the whole distinction of statics and dynamics is a bit overdone

oh I thought you were in Europe. nice

i am german, but live in vancouver atm.

yeah I hope no-one ever asks me to choose static vs dynamic in an argument.

it's one big sludge in my head at this point 😉

hehe

that makes sense. similar to gradual typing.

thinking about the bar based tree syntax of rules for proofs, you can push type constraints back and forward whenever you get them along the tree and resolve it

that is why i think it should be a relational interpreter

"it" is what here?

daphne?

hehe

well, yes. i mean in general interpreter frameworks

do most type systems you know just follow beta reduction?

no, comparatively what I'm doing is insane. type systems don't usually put code in types. kind of defeats the point of a type.

the trick with local type inference is transferring expected types to/from functions/arguments at application points.

you usually need to make a choice: check arguments first, or check function first.

if you check function, then you have expected types for args. useful if you have hard-to-infer args like functions.

if you check args, then you have expected types for fn params, which is the classic problem in local type inference: where to find types for params.

there's all sorts of papers with specific rules about when to do which strategy, or hybrids.

I just threw all that out the window. if you find a hard-to-infer expression (i.e., lambdas), then just stuff its code into its type, then wait for it to be applied via the application rule or subtyping etc

I forgot the specific strategy, but standard ML does something similar in spirit. IIRC it effectively inlines lambdas to its application position.

you don't need major changes to the formalisms for all these other strategies. I'm not aware of anything trying to formalize my strategy, except maybe symbolic execution land. I had a draft in my phd.

it's probably most similar to how Typed Racket checks function intersections. you check the function body multiple times for each type the function is supposed to have. the intuition with my approach is that you build up that intersection as you type check.

Do you have to have a relational interpreter for partial evaluation? I thought a staging interpreter was sufficient

Like in Nada Amin's papers on collapsing reflective towers

Relational interpreters can be used to check typing though (Greenspun's twelfth rule)

This is pretty much my white whale whilo I'd very much like to explore this field

Hey, sorry, just saw this. I agree @UK0810AQ2, it should be a tower of relational interpreters. A first step I would like to see better PL tooling, e.g. for building interpreters. Do you have a take on this?

I'm still not sure why they need to be relational, but off the top of my head • start with a minimal interpreter for Clojure with the requirement it be metacircular • add staging • ensure a tower of these interpreters can be collapsed • convert the interpreter to a relational interpreter That exercise lets you identify what tools are missing, then build them and port the interpreter to them. Maybe I'm off base, but the requirement for better PL tooling is too broad for me to imagine what exactly you're looking for and how you'd want to use it

@UK0810AQ2 Sorry for just throwing this at you without more context, I was in a meeting. What I mean is that racket has a lot of libraries that help to implement interpreters, in particular redex. I have seen very little work in Clojure so far trying to make it easy to port racket language implementations or features over to DSLs that also work in Clojure. Nada's racket implementation of the tower for instance would be readily portable with a few primitives from redex https://github.com/TiarkRompf/collapsing-towers/blob/master/popl18/core.rkt#L2.

Clojure compilers typically are one-pass, directly hooking into tools.analyzer. But even the AST of the analyzer is not optimal if you compare it to chez scheme for example (or also the datalog parser we use in datahike). There you use dedicated types (e.g. defrecords) to make dispatch on nodes super fast without having to access datastructures to dispatch. nanopass can then collapse the tower of compilers and erase the overhead of having many passes and languages. I am trying to figure out atm. how to do this with Clojure.

I think the limited engagement with racket is a huge lost opportunity for Clojure, because people in racket do a lot of work implementing languages, but racket will never be a mainstream industrial environment, I think, because too few people in its ecosystem care about that. But making it easy for them to ship a language of theirs to the JVM or JavaScript would for sure be interesting enough so that they would also promote Clojure to PL researchers.

Would be curious what @ambrosebs’s take is on this.

It is unlikely that we would get any stack of building something like this optimal in the first go, figuring out how to build supporting tooling to do so would amortize the cost of iteration.

Having said all this, I think most PL rewriting systems are fundamentally unidirectional, i.e. they reduce terms forward and are not really relational.

@U06MDAPTP is working on something interesting, maybe he wants to chime in

I'll take some time to digest this, but regarding performance etc, I've started sketching out a port of tools analyzer to records

I would like to go the other way and start bottom up with Datalog, similar to https://dl.acm.org/doi/10.1145/3591239 and use the persistent indices we have in datahike now.

Nice!

I think porting some of the typical special forms of redex might pay off a lot to integrate into racket. It would be good to have somebody with a bit more racket experience than me though.

@UK0810AQ2 I have built https://github.com/plai-group/daphne which has multiple passes but operates naively on sexps, which is convenient, but not ideal.

First order languages like this can be integrated with Datalog and restricted relational languages that could have termination guarantees and cost models.

One thing I would like to be able to do is fit a measure estimator (e.g. tranforrmer-based diffusion model) automatically to your database queries to invert certain relations effectively.

E.g. summarized here https://icml.cc/virtual/2023/oral/25446

In other words a strict generalization of relational programming is measurable programming (or probabilistic programming), i think this would fit in nicely into a relational interpreter stack that can do many different forms of inference.

What about https://github.com/pangloss/pattern?

https://github.com/pangloss/pattern/blob/main/test/nanopass_test.clj

That looks super interesting!

@UK0810AQ2 regarding tools.analyzer with records, I did basically that with my fork. These macros might come in handy https://github.com/typedclojure/typedclojure/blob/a74c51a8242bdb747e1e79e969c98fe31a4d3e36/typed/cljc.analyzer/src/typed/cljc/analyzer.cljc#L144-L220 Grep around the codebase for those 3 operators and you'll probably get the idea, basically defrecord => defexpr, ->Record => (create-expr {..} Record), and assoc => (update-expr expr Record [k v] [k v]). e.g., browse this file from here, you'll probably recognize most of it from tools.analyzer https://github.com/typedclojure/typedclojure/blob/a74c51a8242bdb747e1e79e969c98fe31a4d3e36/typed/cljc.analyzer/src/typed/cljc/analyzer.cljc#L311

I tried to get clever in my implementation and get rid of the op keyword and implemented walk directly instead of via children It was a slog so I put it aside

I'll get back to it, sometime in the future

Interesting, your dispatch was slower than accessing the keyword?

Mine or Ambrose's?

I'll dig it up when I get home but I focused my macrology on specifying the expression children at definition time to emit the walking and update code

Here

(defmacro defop
  "Adds op, env, form fields, first group of fields is children, rest are
  not children but still AST fields."
  [name children extra-fields & opts]
  `(defrecord ~name [~'op ~'env ~'form ~@children ~@extra-fields]
     p/IChildren
     (~'-children* [~'_]
       ~(mapv (fn [c] [(keyword c) c]) children))
     (~'-children [~'_]

      ~(if (some #(:vector (meta %)) children)
         (-emit-children-cat children)
         (mapv symbol children)))
     p/IUpdateChildren
     (~'-update-children [~'ast ~'f]
      ~(-emit-update-children 'ast children 'f))
     ~@opts))

Then this expands like:

(defop If [test then else] [children])
(defrecord
  If
  [op env form test then else children]
  p/IChildren
  (-children* [_] [[:test test] [:then then] [:else else]])
  (-children [_] [test then else])
  p/IUpdateChildren
  (-update-children
    [ast f]
    (let [G__11305 ast
          G__11305 (update-child G__11305 f :test test)
          G__11305 (if (reduced? G__11305)
                     G__11305
                     (update-child G__11305 f :then then))
          G__11305 (if (reduced? G__11305)
                     G__11305
                     (update-child G__11305 f :else else))]
      G__11305)))

Next step is figuring out how I can avoid intermediate allocations during update-children