Re: Holes in GHC

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 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