On Sun, Feb 12, 2012 at 02:55:40PM +0100, 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.
Being able to see the available context is indeed a big advantage, but even just seeing the type of the hole is really helpful -- I would certainly use this feature if it were available in Haskell. And we have to start somewhere, don't we? There is certainly no reason we can't later *add* ways of extracting information about the context of a hole.
as others have indicated, it can relatively easily be simulated already.
I don't think this is true. The wiki page includes a discussion of the current methods for "simulating" holes and their (substantial) disadvantages. In order to be useful it seems to me that it must be possible to (1) obtain the inferred type of a hole (2) while still allowing the enclosing module to type check. As far as I know, none of the existing solutions satisfy (2). -Brent