Proposal: Partial Type Signatures

[Edward Kmett]

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