On 03/12/2014 08:09 PM, Austin Seipp wrote:
In any case, I believe the original formulation of Holes by Thijs actually somewhat overlapped with the idea presented here. In particular, it would have allowed us to say[4]:
f :: Bool -> _ () f = ...
where _ is a 'hole' in the signature, and the type-checker would try to report some kind of type constructors that might fit based on the definition. But this was never implemented, and the design was more in the style of Agda-goals: they were meant to help you write out the types, not avoid them through inference.
In any case - I too am receptive to the idea of partial type signatures, so I'd like to see this. (And if we could make it optionally work with the ideas proposed by Thijs, that would be great, so we can actually have 'holes' at the type level, like at the term level. But Simon has some good points in [4] worth reading on that note.)
We have also thought about letting the compiler notify the user of the type each wildcard or 'type hole' was instantiated to during type inference. We would certainly like to work further on this front, i.e. reporting the instantiations and/or extending the GHC API to allow Agda-like goal solving. However, we have the impression that no Hole should remain unfilled, whereas using a partial type signature doesn't necessarily mean the program is incomplete. A partial type signature can still be a (stylistic) choice. Cheers, Thomas Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm