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 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@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs