Proposal: Partial Type Signatures

[Gabor Greif]

Yeah, done.

Cheers,

    Gabor

On 3/12/14, Simon Peyton Jones <simonpj at microsoft.com> wrote:
> Indeed, you are right.  It's a wiki, so do go ahead.
>
> Simon
>
> | -----Original Message-----
> | From: Gabor Greif [mailto:ggreif at gmail.com]
> | Sent: 12 March 2014 18:55
> | To: Simon Peyton Jones
> | Cc: Malcolm Wallace; ghc-devs
> | Subject: Re: Proposal: Partial Type Signatures
> |
> | 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
> | >
>