Proposal: Partial Type Signatures

[Gabor Greif]

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
>