Proposal: Partial Type Signatures

[Dan Frumin]

Aha!, that is exactly why TypeHoles were renamed to TypedHoles :)

In the TypedHoles extension underscores are used on the term level.




On March 12, 2014 at 10:18:40 PM, Malcolm Wallace (malcolm.wallace at me.com) wrote:

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 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20140313/0cb34498/attachment.html>