You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The point of this project isn't so much just what typed functional programming can do for program synthesis, but more importantly, what program synthesis can do for typed functional programming.
I believe program synthesis by types + examples is the killer app that will super-charge Idris-style hole-filling suggestions, and having this integrated in an IDE for a language like Haskell or Idris should help bring about code that 'writes itself' from the given examples for these (already awesome yet in the non-CS mainstream vastly under-appreciated) languages.
This use-case brings a bunch of questions:
Does this make more sense for Haskell or Idris? It seemed hole-filling suggestions (with IDE integration) were more mature in Idris? - given ML bits I'm def doing Haskell
Could I adapt existing extensions for these languages for e.g. VSCode to do hole filling suggestions? - probably! I may wanna check other Haskell extensions there, while for GHC I would likely need a compiler plugin as well for synthesis-based hole suggestions as well...
Can I hook into the compiler APIs for suggestions? - yes, listing holes is built-in there
How the heck would we make it aware of the samples input-output pairs for a given function? Could we do something involving the decorator pattern?
The text was updated successfully, but these errors were encountered:
The point of this project isn't so much just what typed functional programming can do for program synthesis, but more importantly, what program synthesis can do for typed functional programming.
I believe program synthesis by types + examples is the killer app that will super-charge Idris-style hole-filling suggestions, and having this integrated in an IDE for a language like Haskell or Idris should help bring about code that 'writes itself' from the given examples for these (already awesome yet in the non-CS mainstream vastly under-appreciated) languages.
This use-case brings a bunch of questions:
Does this make more sense for Haskell or Idris? It seemed hole-filling suggestions (with IDE integration) were more mature in Idris?- given ML bits I'm def doing HaskellThe text was updated successfully, but these errors were encountered: