Proposal: Partial Type Signatures

[Thomas Winant]

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