4 ms·
I would really love to see an IDE that auto suggests / autocompletes code based on typed holes like this. Does such a thing exist?
by Gormisdomai 7y ago
I would really love to see an IDE that auto suggests / autocompletes code based on typed holes like this.
Does such a thing exist?
- Jtsummers 7y agoCheck out Idris and the book Type Driven Development. It has an emacs mode that does that for you. I’m not sure about other languages. It was a very nice experience though I just went through it for the learning experience and haven’t tried to apply it to any problems since then.
- gcommer 7y agoHoles in Agda are a good bit more powerful than in Haskell, and agda's emacs mode has a bunch of very powerful commands for working with them, eg: listing possible values, automatically filling, splitting them by case, etc. For example, for this post's "jonk" example I just had to copy the type into emacs, reformat it a bit into Agda syntax, then press C-c C-a and it automatically figured out the solution that the author worked through manually: λ z z₁ z₂ → z₁ (λ z₃ → z₂ (z z₃)) See the full list of commands at https://agda.readthedocs.io/en/v2.5.2/tools/emacs-mode.html https://agda.readthedocs.io/en/v2.5.2/tools/emacs-mode.html
- derefr 7y agoWhy even have the code? The type is all the compiler needs to spit out a definition. Your source can just be the type.
- pirocks 7y agoIntellij can sorta do this for Java if you fo ctrl+shift+space.
- hardwaresofton 7y agoIdris does this with a REPL-like interface: https://www.youtube.com/watch?v=mOtKD7ml0NU https://www.youtube.com/watch?v=mOtKD7ml0NU