[Primer] Program synthesis

[dhess]

Edwin Brady has some sort of Idris program synthesizer. I'm not sure it's public yet, but here's the output from a session where he asked it to synthesize append on lists:

https://gist.github.com/edwinb/9b5dfda2ddf402133ab5d2ce47e85f3e

There's also Barliman:

https://www.youtube.com/watch?v=er_lLvkklsk

Ed Kmett was working on guanxi and coda, but those seem to be stalled:

https://github.com/ekmett/guanxi https://github.com/ekmett/coda

[brprice]

Some other similar projects:

• agda's auto mode / agsy: https://agda.readthedocs.io/en/v2.6.0.1/tools/auto.html IIRC some agda dev told me that the auto code was rather arcane and that nobody understood it or had much motivation to maintain/improve it!
• djinn: https://hackage.haskell.org/package/djinn seems dead
• justdoit: https://github.com/nomeata/ghc-justdoit This actually says "LJT proof search" - probably should look up the literature at some point!

justdoit mentions the following similar tools:

• exference
• curryhoward for Scala
• hezarfen for Idris

---

Looking at that append example it strikes me that linear types would help the search out massively (or even just a bias in the search engine to use all the input data preferentially)

Also, as Drew mentioned in a meeting, test cases would help filter the results!

[dhess]

I think this should be our 3rd (and final?) prototype project, before we move on to productizing Primer.

[dhess]

This ended up being several steps too far for our initial version of Primer, so I'm marking it as a long-term goal. I'll keep it open, however.