Proposal: Partial Type Signatures

Wed Mar 12 19:09:13 UTC 2014

That page should be reworked a bit - for one, typed holes are actually
no longer an extension. They are a warning which is on by default,
controlled by -f[no-]warn-typed-holes[1][2][3]. This IMO does improve
their utility after using it a bit, because they never allow a program
to typecheck - they only change the results of the errors you get.

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.)

[1] http://www.haskell.org/ghc/docs/7.8.1-rc2/html/users_guide/typed-holes.html
[2] http://www.haskell.org/pipermail/ghc-devs/2014-January/003758.html
[3] https://github.com/ghc/ghc/commit/235fd88a9a35a6ca1aed70ff71291d7b433e45e4
[4] https://ghc.haskell.org/trac/ghc/wiki/Holes

On Wed, Mar 12, 2014 at 1:55 PM, Gabor Greif <ggreif at gmail.com> wrote:
> Just a reminder that the new jargon is TypedHoles, so maybe the page
> should be renamed to reflect that (an possibly combed for the old
> spelling).
>
> Cheers,
>
>     Gabor
>
> On 3/12/14, Simon Peyton Jones <simonpj at microsoft.com> wrote:
>> http://www.haskell.org/haskellwiki/GHC/TypeHoles
>>
>> | -----Original Message-----
>> | From: ghc-devs [mailto:ghc-devs-bounces at haskell.org] On Behalf Of Malcolm
>> | Wallace
>> | Sent: 12 March 2014 18:19
>> | To: ghc-devs
>> | Subject: Re: Proposal: Partial Type Signatures
>> |
>> | Since I never used them, I have honestly been under the impression that
>> | the TypeHoles language extension named exactly this partial type
>> | signatures thing.  I have loved the idea of underspecifying the type
>> | signature, ever since it was first mooted many years ago.  So what does
>> | TypeHoles do, if not this?
>> |
>> | Regards,
>> |     Malcolm
>> |
>> | On 12 Mar 2014, at 15:09, Edward Kmett wrote:
>> |
>> | > Clearly given that term-level holes are called TypeHoles, the extension
>> | to enable these should be called KindHoles. =)
>> | >
>> | > Er.. I'll show myself out.
>> | >
>> | > -Edward
>> | >
>> | >
>> | > On Wed, Mar 12, 2014 at 9:35 AM, Thomas Winant
>> | <thomas.winant at cs.kuleuven.be> wrote:
>> | > Dear GHC developers,
>> | >
>> | > Together with Tom Schrijvers, Frank Piessens and Dominique Devriese, I
>> | > have been working on a proposal for adding *Partial Type Signatures* to
>> | > GHC. In a partial type signature, annotated types can be mixed with
>> | > inferred types. A type signature is written like before, but can now
>> | > contain wildcards, written as underscores. The types of these wildcards
>> | > or unknown types will be inferred by the type checker, e.g.
>> | >
>> | >     foo :: _ -> Bool
>> | >     foo x = not x
>> | >     -- Inferred: Bool -> Boo
>> | >
>> | > The proposal also includes a form of generalisation which aligns with
>> | > the existing generalisation that GHC does. We have written down a
>> | > motivation (when and how might you use this) and details about the
>> | > design and implementation on the following wiki page:
>> | >
>> | > https://ghc.haskell.org/trac/ghc/wiki/PartialTypeSignatures
>> | >
>> | > We have a (work in progress) implementation [1] of the feature based on
>> | > GHC. It currently implements most of what we propose, but there are
>> | some
>> | > remaining important bugs mostly concerning the generalisation. We also
>> | > described our design and presented a formalisation based on the
>> | > OutsideIn(X) formalism in a paper [2] presented at PADL'14.
>> | >
>> | > What we are hoping to get from the people on this list is any of the
>> | > below:
>> | > * Read the design, play with the implementation and tell us any
>> | comments
>> | >   you may have about the feature, its design and implementation.
>> | > * Opinions on whether this feature might be acceptable in GHC upstream
>> | >   at some point (if not, we do not think it's worth developing the
>> | >   implementation much further).
>> | > * Perhaps a code review or a discussion with someone more knowledgeable
>> | >   about the internals of GHC's type checker about how we might fix the
>> | >   remaining problems in our implementation (specifically, we could use
>> | >   some help with implementing the generalisation of partial type
>> | >   signatures).
>> | > * Feedback on the `Questions and issues' section on the wiki page.
>> | >
>> | >
>> | > Kind regards,
>> | > Thomas Winant
>> | >
>> | > [1]: https://github.com/mrBliss/ghc-head/
>> | > [2]: https://lirias.kuleuven.be/bitstream/123456789/423475/3/paper.pdf
>> | >
>> | >
>> | > Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm
>> | > _______________________________________________
>> | > ghc-devs mailing list
>> | > ghc-devs at haskell.org
>> | > http://www.haskell.org/mailman/listinfo/ghc-devs
>> | >
>> | > _______________________________________________
>> | > ghc-devs mailing list
>> | > ghc-devs at haskell.org
>> | > http://www.haskell.org/mailman/listinfo/ghc-devs
>> |
>> | _______________________________________________
>> | ghc-devs mailing list
>> | ghc-devs at haskell.org
>> | http://www.haskell.org/mailman/listinfo/ghc-devs
>> _______________________________________________
>> ghc-devs mailing list
>> ghc-devs at haskell.org
>> http://www.haskell.org/mailman/listinfo/ghc-devs
>>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs
>

-- 
Regards,

Austin Seipp, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/