Proposal: Partial Type Signatures

[Simon Peyton Jones]

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