Clojurians Log v2

Trimmed video is here https://www.youtube.com/watch?v=QE3PZLlefUE

That’s great

There’s a lot of boilerplate to create and use the type variables. I wonder if bind-tv could just return the result of t/tv

This is one step away from doing type inference before running the app, reminiscent of ectype by holly wu (https://dejawu.me)

@nbtheduke tv is not really a spec, it's just an occurrence of a type variable that's always substituted away by the time the spec is used.

Can you give an example of what you're thinking?

The main reason tv exists is because of s/explicate. It ties your hands in what your syntax can be.

Ah that makes sense.

I was thinking of something like generics in other languages where you specify the type variables as local varies and can use them wherever

clojure.spec’s fspecs are already so verbose lol

I tried that at first. after many failed experiments, I succeeded by following fspec's verbosity. It made some things more obvious actually, in particular how to generate a "binder" of type variables, even ones with bounds that depend on each other.

If you distill down typed.clj.spec and this talk, it's really 99% of the work was getting the syntax and substitution right, and 1% was implementing the idea that you can represent a type variable with a small type in a generator, which is directly from quickcheck. https://hackage.haskell.org/package/QuickCheck-2.14.3/docs/Test-QuickCheck-Poly.html

I wonder if this approach could be brought to Malli

Is the code public?

Here: https://github.com/typedclojure/typedclojure/tree/main/typed/clj.spec

Here's how you do it for schema as a built in extension https://github.com/frenchy64/schema/pull/11/files And as an external library https://github.com/frenchy64/schema/pull/13/files

Here's a conceivable starting point for malli. As-is, this compiles all polymorphic types to what they would instrument to. The basic idea from here would be to figure out how to preserve the :all schema until you're doing generative testing on it. https://github.com/frenchy64/malli/pull/2/files

If you get that far, here's the skeleton quickcheck code to generatively test a polymorphic spec (doesn't implement the "trick" of pushing gensyms through the function, see spec impl for that) https://github.com/frenchy64/schema/pull/13/files#diff-8cf7ec1a3263df0e063ba2a470023329ca838dd99ef8b4137c2cd9348f92df6bR31-R46

And presumably that will break the instrumentation side, and to fix it you need to instantiate the spec when you instrument it like here https://github.com/frenchy64/schema/pull/13/files#diff-06186e539315e4b79419d0a1bf50a613c059f45e5246aa4c0416cebc67cea263R267

Oh, looks like I did implement this as a real library for schema. here it is https://github.com/frenchy64/schema-incubator But I think I didn't port over the generative testing part from that PR above. I lost steam at some point.

makes sense, seems like a ton of work

thanks for the links, i'll read through them

I guess it was, thanks. I think I only stopped because I never got much interest in typed.clj.spec and the maintainer of schema wasn't interested in this feature being merged which led to a laborious process of extracting a library. Popped my bubble for a few years apparently, but this work is some of my favorite!

i've been working more with ocaml recently and i would love for clojure to have something similar. this kind of work is about as good as we can currently get. (i have no idea how you'd handle macros in any type system lol, you'd probably have to macro-expand everything and then run the inference on the resulting forms)

Oh I have ideas!

This was going to be 2 talks actually. Leveling up function specs, and then macro specs.

maybe i'm biased but i really don't like clojure.spec lmao, i want to see this done separate from it. i gotta spend more time with typedclojure, i think

part of the motivation here is to make polymorphic types ubiquitous. then typed clojure can steal them for free instead of having to demand for so many annotations. and then we can translate polymorphic types to a library that implements this runtime checking idea, and get generative testing for free.

also I'm a big fan of just implementing better generators for test.check, but spec kind of killed that area it seems.

we don't even have function generators in test.check.

it's possible I even implemented this for typed clojure and never told anyone https://github.com/typedclojure/typedclojure/blob/7ef50ae3db663a713960a06b804ca0927da71a92/typed/clj.checker/src/typed/clj/generators.clj#L120

you've done so much, i'm surprised you can remember all of this

Here's the WIP test xD https://github.com/typedclojure/typedclojure/blob/7ef50ae3db663a713960a06b804ca0927da71a92/typed/clj.checker/test/typed_test/clj/generators.clj#L266-L268

Haha clearly I've forgotten most of it!

Well, favor #2 would be: please boot up a repl and see if those typedclojure check tests work 🙂

sadly, I will be putting the kids to bed at that time, but I can't wait to watch it tomorrow

I tried applying a very similar notion to malli using datalog syntax, which is a fun cheat when you're immutable, to treat the input and output as relations. It also lets you constrain the inputs like you wouldn't be able to otherwise, e.g.

[:map {:in ['e] :where '[[?e :a ?a] [?e :b ?b] (< ?a ?b)]} [:a :int] [:b :int]]

I think this representation lends itself well to programmatic manipulation and value generation but I have no proof yet

For functions it would look sort of like

;; ID
[:=>
 '{:in [[?in] ?out]
   :where
   [(= ?in ?out)]}
 [:cat :any] :any]


;; comp
[:=>
 '{:in [[f g] h]
   :where
   [[(f ?a) ?b]
    [(g ?b) ?c]
    [(h ?a) ?c]]}
 [:cat
  [:=> [:cat :any] :any]
  [:=> [:cat :any] :any]]
 [:=> [:cat :any] :any]]

I think this sort of creates the same data flow graph

That’s a nice syntax

I believe the right syntax for relational problems should also be borrowed from a relational language 🙃

That's cool. Have you tried applying this to sequence regular expressions?

Like say the kw args version of your :map spec.

I invented a sort of ass backwards pattern matching syntax partially inspired by scheme syntax case and meander to represent repetition

How might you psuedocode the spec for clojure.core/map?

I'm on my phone so going to be extremely hand wavy -

[?in [f [?x ...]]]
[?out [?y ...]]
[(f ?x) ?y]

I think that's sufficient for drawing all the arrows

Ok I'm starting to see it.

I think it's more difficult with things like unordered data with non canonical representation which @noprompt directed me to the research in the Egison language for

I like that it's parsable so you can use it for generators, instead of relying on an opaque function to tighten a dependent spec.

Like [:map {:fn (fn [k v] (< k v))} :int :int] would be tough to generate.

It would be impossible to generate! But its a relation, so it should be trivial to generate

That's my big contribution - in a functional language the input and optional outputs of a spec form a relation Generating relations is easy The hard part is you'll have to write a relational eval for Clojure 🙂

If William Byrd is looking for disciples students I'm game

It's interesting I'm coming from the opposite side. I'm fascinated by how polymorphic types imply relations.

Every sufficiently advanced type system contains a poorly specified bug ridden implementation of Prolog

So just lean into it and use relational programming as the bedrock

Pretty sure I implemented a Typed Racket in minikanren. It had some drawbacks 🙂

Such as?

Probably stemming from all the concepts not having bedrock in relational programming 🙂 encoding subtyping and occurrence typing was difficult and slow I think.

I think this was it https://github.com/frenchy64/miniKanren-occurrence-type-inferencer/blob/master/inferencer.rkt

Did you look into generating values from relations?

Not yet, I actually assumed that would be trivial as each additional clause just adds a bind

I have about three reimplementations of core logic in various degrees of incompleteness

I want a high performing implementation which would support unordered collections from the get go, not just sequences

Do you think generating functions might be trivial?

With a relational evaluator, sure

Not sure how you'll do narrowing with this

Keep me posted on your progress.

expect very little unless I get a sabbatical or lots of free time otherwise. Kids are loads of fun, but also a time sink 🙃 As you can see it's still sitting pretty high at the top of my mind so it'll probably be the first thing I get to when I do have time

I mean I'm 12 years into Typed Clojure, no rush. 😉

MiniKanren is sort of why I ended up here 🙂