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@xxxxxxxxxxx
[mailto:glasgow-haskell-users-bounces@xxxxxxxxxxx] On Behalf Of Edward Kmett
Sent: 19 February 2012 02:58
To: Thijs Alkemade
Cc: Andres LÃh; glasgow-haskell-users@xxxxxxxxxxx
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@xxxxxxxxx> wrote:
On Sun, Feb 12, 2012 at 2:55 PM, Andres LÃh <andres.loeh@xxxxxxxxxxxxxx> 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@xxxxxxxxxxx
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@xxxxxxxxxxx
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users