I've been teaching the Idris program synthesis gadget to not give up after the first result. This is where we're up to... gist.github.com/edwinb/9b5dfda

I'm imagining an editor interface where you press "generate", and if you don't like what you get then you keep frantically pressing the button until you do like it.

Show thread

Just hacked this into the vim mode. Imagine I'm hitting the type declaration with a hammer between each implementation.

It's interesting to see where it goes if you make the lists linear. The first answer is the right one here...

In other news, TIL you can record and edit your screen in Linux. What is this sorcery!

Show thread

Thanks to a suggestion by @Augustsson (generate some candidates then sort by fraction of bound variables used) it gets the right answer much quicker now.

Show thread

@raichoo This is fun, although I don't know if it's going to work for anything real until the program synthesis is improved some more!

@edwinb Seems to be a pretty interesting place for exploration though ^^. Looking forward to what you are going to build there 😸

@edwinb @raichoo man I have this dream of something like the barleyman tool from team minikanren or guanxi from kmett used for program synthesis in an environment with rich type information

@edwinb how did you record and edit your screen in Linux?

@shapr I recorded with kazam then cropped with HandBrake.

One annoying challenge is that lots of programs don't cope well with HiDPI (kazam didn't, I had to put the window in the right corner of the screen!)

@edwinb this is looks like similar kinds of wizardry to lispy-mode :blobcat3c:
Sign in to participate in the conversation

Server run by the main developers of the project 🐘 It is not focused on any particular niche interest - everyone is welcome as long as you follow our code of conduct!