Integrate djinn-like code generation

[TomMD]

What do people think about a type-directed code generation via code action?

I imagine an HLS integration of djinn (de-bitrotted) that adds currently in scope type/data/classes to the djinn environment then can update any undefined or perhaps hole with a djinn query.

[pepeiborra]

This looks quite easy to do with https://hackage.haskell.org/package/djinn-ghc
Ping @serras

[wz1000]

https://github.com/TyGuS/hoogle_plus seems to be a newer alternative

https://cseweb.ucsd.edu/~npolikarpova/publications/hplus.pdf

[serras]

@pepeiborra please tell me if I can help in any way. I'll give djinn-ghc some love this weekend and ensure it works on newer versions of GHC.

[jneira]

@TomMD Afaiu the tactic plugin has brought something similar to described here: type-directed code generation via code action.
So maybe the objective of integrate djinn has been somewhat accomplished?

[isovector]

The tactics plugin subsumes all of djinn's functionality, as well as provides support for inductive types.

[TomMD]

Yep, I was thinking the same thing. Not sure about the UX still, but that's a different ticket.

For those coming here via search consider:

f :: () -> Maybe ()
f a = _

Ask for a code action, you'll have lots of options. Try number 4, Just:

f a = (Just _)

Some extra parentheses and another hole. In my case with nvim I needed to move the cursor to the new hole and re-execute code-action. This time try number 1 a:

f a = (Just a)

The default formatting isn't able to clean this up at this time.