This page is not created by, affiliated with, or supported by Slack Technologies, Inc.
2024-03-06
Channels
- # babashka (60)
- # beginners (36)
- # clj-kondo (29)
- # clojure (91)
- # clojure-dev (18)
- # clojure-europe (12)
- # clojure-nl (1)
- # clojure-norway (11)
- # clojure-uk (5)
- # clojuredesign-podcast (8)
- # clojurescript (40)
- # core-typed (74)
- # data-science (8)
- # datomic (9)
- # emacs (22)
- # events (5)
- # fulcro (56)
- # gratitude (3)
- # hyperfiddle (11)
- # lsp (6)
- # malli (36)
- # meander (23)
- # off-topic (50)
- # polylith (4)
- # portal (10)
- # reitit (4)
- # schema (1)
- # shadow-cljs (66)
- # squint (3)
- # tools-deps (16)
I'll be talking about bringing some ideas from the statically typed world to runtime systems like clojure spec.
sadly, I will be putting the kids to bed at that time, but I can't wait to watch it tomorrow
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)
@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.
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'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)
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.
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
Well, favor #2 would be: please boot up a repl and see if those typedclojure check
tests work 🙂
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 willI 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]]
That’s a nice syntax
I believe the right syntax for relational problems should also be borrowed from a relational language 🙃
I invented a sort of ass backwards pattern matching syntax partially inspired by scheme syntax case and meander to represent repetition
I'm on my phone so going to be extremely hand wavy -
[?in [f [?x ...]]]
[?out [?y ...]]
[(f ?x) ?y]
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
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.
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 🙂
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
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
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