Holes in GHC

[Conor McBride]

Hi

Sorry to pile in late...

On 13 Feb 2012, at 09:09, Thijs Alkemade wrote:

> On Sun, Feb 12, 2012 at 2:55 PM, Andres Löh <andres.loeh at googlemail.com> wrote:
>> Hi Thijs.
>> 
>> Sorry if this has been discussed before.
>> 
>> In my opinion, the main advantage of Agda goals is not that the type
>> of the hole itself is shown, but that you get information about all
>> the locally defined identifiers and their types in the context of the
>> hole.

[..]

> Thanks for your feedback. Showing everything in scope that matches or
> can match the type of a hole is certainly something I am interested
> in, but I'm afraid it's out of the scope of this project.

That's not quite what Andres said, although it would also be a useful
piece of functionality.

If I might plug a bit of kit I knocked together recently, if you

  cabal install shplit

(see also https://personal.cis.strath.ac.uk/~conor/pub/shplit/ )

you'll get the beginnings of an editor-assistant which just works as
a stdin->stdout transducer. I've been able to wire it into emacs quite
neatly and gedit more clunkily. I'm told vi should be no problem.

Shplit turns

  foo :: [x] -> [x]
  foo xs{-?-} =

into

  foo :: [x] -> [x]
  foo [] =
  foo (x : xs) =

by (i) snarfing the datatype declarations from your file (no import
chasing yet) and adding them to a standard collection, (ii) figuring
out the type of the pattern variables given the type signature
provided. Shplit is still very dumb and makes no use of ghc's
typechecker: shplit's typechecker could be used just as easily to
mark up pattern variables with their types, as to do case analysis.

It is rather tempting to push further and make the thing label holes
with their types. Sometimes, the adoption of primitive technology is
a spur to design. If one adopts the transducer model, the question
then arises "in what format might we insert this data into the file?".
In the case of typed holes, we can go with types in comments, or
(with careful use of ScopedTypeVariables) we can really attach them
in a way that would get checked.

I think it could be quite a lot of fun to build a helpful tool,
splitting cases, supplying type information, perhaps even offering
a menu of possible ways to build a term. I think the transducer
method is a relatively cheap (* major caveat ahead) and editor-neutral
way to go about it. If you fix a text format for the markup (i.e., for
requests to and responses from the transducer-collaborator), at worst
it's usable just by running the thing on the buffer, but with more
programmable editors, you can easily make more convenient triggers
for the requests, and you can parse the responses (e.g. generating
tooltips or lifting out a list of options as a contextual menu). The
adoption of the transducer model effectively separates the choice of
information and functionality from the design of the user interface,
which has certainly helped me to get on and do something.

The caveat is that transducers require not just parsing source code
but the ability to reconstruct it, slightly modified. Currently,
she and shplit have very selective, primitive technology for doing
this. Parsing-for-transduction is surely worth a proper think.

All the best

Conor