Holes in GHC

[Chris Dornan]

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: glasgow-haskell-users-bounces at haskell.org [mailto:glasgow-haskell-users-bounces at haskell.org] On Behalf Of Edward Kmett
Sent: 19 February 2012 02:58
To: Thijs Alkemade
Cc: Andres Löh; glasgow-haskell-users at haskell.org
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 <thijsalkemade at gmail.com> 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. 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
Glasgow-haskell-users at haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20120219/fe186eee/attachment-0001.htm>