Fork me on GitHub
#core-typed
<
2024-03-06
>
ambrosebs06:03:16

I'll be talking about bringing some ideas from the statically typed world to runtime systems like clojure spec.

😍 4
👍 1
Noah Bogart16:03:50

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

Noah Bogart18:03:20

That’s great

Noah Bogart19:03:15

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

Noah Bogart19:03:28

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

ambrosebs00:03:34

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

ambrosebs00:03:53

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

ambrosebs00:03:06

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

👍 1
Noah Bogart00:03:23

Ah that makes sense.

Noah Bogart01:03:57

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

Noah Bogart01:03:21

clojure.spec’s fspecs are already so verbose lol

ambrosebs02:03:45

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.

ambrosebs02:03:07

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

👍 1
Noah Bogart04:03:08

I wonder if this approach could be brought to Malli

Noah Bogart04:03:34

Is the code public?

ambrosebs05:03:59

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

ambrosebs06:03:28

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

ambrosebs06:03:10

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

ambrosebs06:03:47

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

ambrosebs06:03:39

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.

Noah Bogart14:03:05

makes sense, seems like a ton of work

Noah Bogart14:03:10

thanks for the links, i'll read through them

ambrosebs16:03:08

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!

🤝 1
Noah Bogart16:03:08

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)

ambrosebs16:03:49

Oh I have ideas!

ambrosebs16:03:27

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

👍 1
Noah Bogart16:03:58

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

ambrosebs16:03:13

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.

ambrosebs16:03:53

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

ambrosebs16:03:00

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

Noah Bogart16:03:11

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

ambrosebs16:03:56

Haha clearly I've forgotten most of it!

ambrosebs16:03:37

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

Ben Sless09:03:48

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]]
Apply to functions at will

Ben Sless09:03:21

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

Ben Sless09:03:57

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

Ben Sless09:03:07

I think this sort of creates the same data flow graph

Noah Bogart11:03:41

That’s a nice syntax

Ben Sless12:03:32

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

ambrosebs16:03:11

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

ambrosebs16:03:24

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

Ben Sless16:03:26

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

ambrosebs16:03:24

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

Ben Sless16:03:59

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

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

Ben Sless16:03:19

I think that's sufficient for drawing all the arrows

ambrosebs16:03:24

Ok I'm starting to see it.

Ben Sless16:03:46

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

ambrosebs16:03:22

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.

ambrosebs16:03:35

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

Ben Sless16:03:25

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

Ben Sless16:03:35

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 🙂

Ben Sless16:03:45

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

😄 2
ambrosebs16:03:56

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

Ben Sless16:03:09

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

😂 2
Ben Sless16:03:03

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

ambrosebs17:03:08

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

ambrosebs17:03:05

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

ambrosebs17:03:27

Did you look into generating values from relations?

Ben Sless17:03:43

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

Ben Sless17:03:16

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

Ben Sless17:03:51

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

ambrosebs17:03:47

Do you think generating functions might be trivial?

Ben Sless17:03:59

With a relational evaluator, sure

Ben Sless17:03:13

Not sure how you'll do narrowing with this

ambrosebs17:03:29

Keep me posted on your progress.

Ben Sless17:03:30

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

❤️ 1
💯 1
ambrosebs18:03:51

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

Ben Sless18:03:10

MiniKanren is sort of why I ended up here 🙂