Holes in GHC
andres.loeh at googlemail.com
Mon Feb 13 09:35:08 CET 2012
>> as others have indicated, it can relatively easily be simulated
> 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).
You are right, and I want to apologize if I sounded overly negative. I
think I was a bit disappointed to see the feature being sold as "Agda
goals" where in fact a major aspect of Agda goals wasn't even being
discussed. I agree now, however, that adding the feature in a limited
form is still quite useful.
More information about the Glasgow-haskell-users