For those of us unfamiliar with Agda would somebody explain what you mean by showing ‘anything introduced in local scopes around the hole’? If the hole were at the top level then this would be the module context and loading it into ghci would give you what you need? (Or more realistically you would be looking at the import statements and looking up the documentation, possibly with IDE tools.) Of course, if the hole is inside the scope of ‘let’ or ‘where’ clauses then you could be missing some details of important pieces needed to fill the hole. If I have understood this, the hole names a context in the code, which is generally *not* at the top level; the filling machinery is mostly concerned with reporting on that context. Thijs is proposing to start by providing tools to locate the context and report on its type, and add tools for extracting other context later. FWIW, I think Thijs is wise to focus on a core extension to start with. Chris From: [email protected] [mailto:[email protected]] On Behalf Of Edward Kmett Sent: 19 February 2012 02:58 To: Thijs Alkemade Cc: Andres Löh; [email protected] Subject: Re: Holes in GHC Not sure if I misparsed your response or not. Its not just things that can or could match the type of the scope, but basically anything introduced in local scopes around the hole, those can have types that you can't talk about outside of a local context, due to existentials that were opened, etc. The usual agda idiom is to make the hole, then check to see what is available that you can use to build towards filling it in, but those locally introduced things may not have anything in common with the type of the hole. -Edward On Mon, Feb 13, 2012 at 4:09 AM, Thijs Alkemade <[email protected]> wrote: On Sun, Feb 12, 2012 at 2:55 PM, Andres Löh <[email protected]> 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. Your page doesn't seem to discuss this at all. Without that > extra info, I don't see much purpose in the feature, though, because > as others have indicated, it can relatively easily be simulated > already. > > Cheers, > Andres Hi Andres,
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. I think finding the types of the holes is a good first step that should make this feature easier to implement later. Best regards, Thijs Alkemade _______________________________________________ Glasgow-haskell-users mailing list [email protected] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
_______________________________________________ Glasgow-haskell-users mailing list [email protected] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
