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

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 wrote:

http://www.haskell.org/haskellwiki/GHC/TypeHoles

| -----Original Message----- | From: ghc-devs [mailto:ghc-devs-bounces@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 | 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 | | _______________________________________________ | 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

On 03/12/2014 08:09 PM, Austin Seipp wrote:

In any case, I believe the original formulation of Holes by Thijs actually somewhat overlapped with the idea presented here. In particular, it would have allowed us to say[4]:

f :: Bool -> _ () f = ...

where _ is a 'hole' in the signature, and the type-checker would try to report some kind of type constructors that might fit based on the definition. But this was never implemented, and the design was more in the style of Agda-goals: they were meant to help you write out the types, not avoid them through inference.

In any case - I too am receptive to the idea of partial type signatures, so I'd like to see this. (And if we could make it optionally work with the ideas proposed by Thijs, that would be great, so we can actually have 'holes' at the type level, like at the term level. But Simon has some good points in [4] worth reading on that note.)

We have also thought about letting the compiler notify the user of the type each wildcard or 'type hole' was instantiated to during type inference. We would certainly like to work further on this front, i.e. reporting the instantiations and/or extending the GHC API to allow Agda-like goal solving. However, we have the impression that no Hole should remain unfilled, whereas using a partial type signature doesn't necessarily mean the program is incomplete. A partial type signature can still be a (stylistic) choice. Cheers, Thomas Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm

First of all: Yay! I've been wanting this for some time. I'm sorry I missed your presentation at PADL about this. I, personally, rather like the design. There may be fine points of discussion as it all becomes reality, but I think this is a great approach -- much like what I've envisioned whenever thinking about the problem. I would allow _ only as a constraint extension and _a in a constraint only when it also appears in the mono-type. I think, contrary to the wiki page, that the scope of named wildcards should mirror the behavior of normal type variables. Yes, it's weird that scoped type variables don't work by default, but I think it's weirder still if some scoped type-variable-like things work and others don't. I don't imagine that this fine control is hard to implement. I think Austin's suggestion below is equally great. Just has 7.8 will now report informative errors when _ is used in an expression position, the implementation for partial type signatures can easily spit out informative errors when _ is used in a type. This would not be an extension, because it does not change the set of programs that compile nor the behavior of compiled programs. However, if a user specifies -XPartialTypeSignatures, then the errors are not reported -- the inferred type is simply used. Thanks so much for doing this! Richard On Mar 13, 2014, at 4:22 PM, Austin Seipp wrote:

On Thu, Mar 13, 2014 at 7:18 AM, Thomas Winant wrote:

...

However, we have the impression that no Hole should remain unfilled, whereas using a partial type signature doesn't necessarily mean the program is incomplete. A partial type signature can still be a (stylistic) choice.

Yes, this is the main hold up I was thinking of. Thinking about it a little more, one way to resolve it perhaps would be to do something similar to we did to typed holes at the term level: make 'holes' at the type level an error by default, which when encountered spit out the error containing the type each hole was instantiated to, and what the partial type signatures would be inferred as. Then, if you enable -XPartialTypeSignatures, these would cease to be errors providing the compiler can infer the types sensibly (and it wouldn't alert you in that case).

That might be a half baked idea (I just sat here for about 5 minutes), but either way I say again I do support -XPartialTypeSignatures anyway, and it sounds like a step in the right direction. :)

-- Regards,

Austin Seipp, Haskell Consultant Well-Typed LLP, http://www.well-typed.com/ _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

i'd like to echo the echo of agreement :) On Thu, Mar 13, 2014 at 5:34 PM, Edward Kmett wrote:

I'd just like to echo that I really like Austin's suggestion as well, as it very nicely unifies the two usecases, while simultaneously *not *dramatically increasing scope.

-Edward

On Thu, Mar 13, 2014 at 4:56 PM, Richard Eisenberg wrote:

...

First of all: Yay! I've been wanting this for some time. I'm sorry I missed your presentation at PADL about this.

I, personally, rather like the design. There may be fine points of discussion as it all becomes reality, but I think this is a great approach -- much like what I've envisioned whenever thinking about the problem.

I would allow _ only as a constraint extension and _a in a constraint only when it also appears in the mono-type. I think, contrary to the wiki page, that the scope of named wildcards should mirror the behavior of normal type variables. Yes, it's weird that scoped type variables don't work by default, but I think it's weirder still if some scoped type-variable-like things work and others don't. I don't imagine that this fine control is hard to implement.

I think Austin's suggestion below is equally great. Just has 7.8 will now report informative errors when _ is used in an expression position, the implementation for partial type signatures can easily spit out informative errors when _ is used in a type. This would not be an extension, because it does not change the set of programs that compile nor the behavior of compiled programs. However, if a user specifies -XPartialTypeSignatures, then the errors are not reported -- the inferred type is simply used.

Thanks so much for doing this!

Richard

On Mar 13, 2014, at 4:22 PM, Austin Seipp wrote:

...

On Thu, Mar 13, 2014 at 7:18 AM, Thomas Winant wrote:

...

However, we have the impression that no Hole should remain unfilled, whereas using a partial type signature doesn't necessarily mean the program is incomplete. A partial type signature can still be a (stylistic) choice.

Yes, this is the main hold up I was thinking of. Thinking about it a little more, one way to resolve it perhaps would be to do something similar to we did to typed holes at the term level: make 'holes' at the type level an error by default, which when encountered spit out the error containing the type each hole was instantiated to, and what the partial type signatures would be inferred as. Then, if you enable -XPartialTypeSignatures, these would cease to be errors providing the compiler can infer the types sensibly (and it wouldn't alert you in that case).

That might be a half baked idea (I just sat here for about 5 minutes), but either way I say again I do support -XPartialTypeSignatures anyway, and it sounds like a step in the right direction. :)

-- Regards,

Austin Seipp, Haskell Consultant Well-Typed LLP, http://www.well-typed.com/ _______________________________________________ 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

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

Indeed, you are right. It's a wiki, so do go ahead. Simon | -----Original Message----- | From: Gabor Greif [mailto:ggreif@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 wrote: | > http://www.haskell.org/haskellwiki/GHC/TypeHoles | > | > | -----Original Message----- | > | From: ghc-devs [mailto:ghc-devs-bounces@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 | > | 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 | > | | > | _______________________________________________ | > | 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 | >

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@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 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

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

| Excellent, I added responses ("thomasw") to your comments on the wiki | page. OK, good. Better still, improve your wording so that no one could make the same mistake as I did, and delete both comments. Simon | -----Original Message----- | From: Thomas Winant [mailto:thomas.winant@cs.kuleuven.be] | Sent: 13 March 2014 19:38 | To: Simon Peyton Jones; ghc-devs@haskell.org | Cc: Tom Schrijvers; Frank Piessens | Subject: Re: Proposal: Partial Type Signatures | | On 13-03-14 10:46, Simon Peyton Jones wrote: | > | Together with Tom Schrijvers, Frank Piessens and Dominique Devriese, | > | I have been working on a proposal for adding *Partial Type | > | Signatures* to GHC. | > | > I'm all for this. Yes, if the design and implementation are solid, | I'd be happy to add it to the main branch. | > | > Do focus on something with excellent power-to-weight ratio: that is, | gives a lot of benefit for a small cost, rather than something that | gives 10% more benefit for 200% more cost. | > | > I've annotated the wiki page with some "SLPJ" comments, which you may | want to look at. | > | > I'd be happy to have a Skype conversation about the details in due | course. | | Excellent, I added responses ("thomasw") to your comments on the wiki | page. | | Cheers, | Thomas | | | > | -----Original Message----- | > | From: ghc-devs [mailto:ghc-devs-bounces@haskell.org] On Behalf Of | > | Thomas Winant | > | Sent: 12 March 2014 13:36 | > | To: ghc-devs@haskell.org | > | Cc: Tom Schrijvers; Frank Piessens | > | Subject: Proposal: Partial Type Signatures | > | | > | 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 | > | | Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm

Hi, My apologies for the late reply. On 2014-04-10 17:43, Richard Eisenberg wrote:

What's the next step from your point of view? Are there unimplemented bits of this?

We do see some bits left to implement: * Partial pattern and expression signatures (see [1] for our view on this issue). * Partial type signatures for local bindings. What with 'let should not be generalised' (see [2])? The implementation also needs a thorough code review (and probably some refactoring as well) from a GHC dev. We'll be talking to SPJ via Skype on Thursday to discuss further details. I'll post another status update in due course. Cheers, Thomas Winant [1]: https://ghc.haskell.org/trac/ghc/wiki/PartialTypeSignatures#PartialExpressio... [2]: https://ghc.haskell.org/trac/ghc/wiki/PartialTypeSignatures#LocalDefinitions

On Apr 10, 2014, at 3:48 AM, Thomas Winant wrote:

...

Hi,

I'm back with a status update. We implemented Austin's suggestion to make wildcards in partial type signatures behave like holes.

Let's demonstrate the new behaviour with an example. The example program:

...

module Example where foo :: (Show _a, _) => _a -> _ foo x = show (succ x)

Compiled with GHC master gives:

...

Example.hs:3:18: parse error on input ‘_’

When we compile it with our branch:

...

Example.hs:3:18: Instantiated extra-constraints wildcard ‘_’ to: (Enum _a) in the type signature for foo :: (Show _a, _) => _a -> _ at Example.hs:3:8-30 The complete inferred type is: foo :: forall _a. (Show _a, Enum _a) => _a -> String To use the inferred type, enable PartialTypeSignatures Example.hs:3:30: Instantiated wildcard ‘_’ to: String in the type signature for foo :: (Show _a, _) => _a -> _ at Example.hs:3:8-30 The complete inferred type is: foo :: forall _a. (Show _a, Enum _a) => _a -> String To use the inferred type, enable PartialTypeSignatures

Now the types the wildcards were instantiated to are reported. Note that `_a` is still treated as a type variable, as prescribed in Haskell 2010. To treat it as a /named wildcard/, we pass the -XNamedWildcards flag and get:

...

[..] Example.hs:3:24: Instantiated wildcard ‘_a’ to: tw_a in the type signature for foo :: (Show _a, _) => _a -> _ at Example.hs:3:8-30 The complete inferred type is: foo :: forall tw_a. (Show tw_a, Enum tw_a) => tw_a -> String To use the inferred type, enable PartialTypeSignatures [..]

An extra error message appears, reporting that `_a` was instantiated to a new type variable (`tw_a`).

Finally, when passed the -XPartialTypeSignatures flag, the typechecker will just use the inferred types for the wildcards and compile the program without generating any error messages.

We added this example and a section about the monomorphism restriction to the wiki page [1].

Comments and feedback are still welcome.

Cheers, Thomas Winant

[1]: https://ghc.haskell.org/trac/ghc/wiki/PartialTypeSignatures

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

Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm

Richard, Since Thomas is attending a summer school for the moment, I'll try to provide a response and Thomas can correct me later if needed... 2014-06-19 17:57 GMT+02:00 Richard Eisenberg :

Vigorous debate on #9200 (https://ghc.haskell.org/trac/ghc/ticket/9200) has led me to think about polymorphic recursion in the presence of a partial type signature. For example, take the following silly but well-typed function:

...

foo :: (a -> Bool) -> a -> () foo _ _ = foo not True

GHC reasonably requires the type signature here, because the recursive call to foo is called with *different* type parameters than the original call -- this is exactly polymorphic recursion. But, what about this?

...

bar :: _ -> a -> () bar _ _ = bar not True

I see several possible outcomes of type-checking bar: 1) Failure. Categorically disallow polymorphic recursion in the presence of a partial type signature. 2) bar :: (Bool -> Bool) -> a -> () 3) bar :: (a -> Bool) -> a -> () 4) bar :: (a -> a ) -> a -> () 5) bar :: (Bool -> a ) -> a -> ()

None of (2-5) is more general than another. So, I advocate for (1), which is essentially what we have decided to do at the kind level. The other approach is to say that wildcards refine to types that never mention user-written type variables. This would select (2) as the correct type. But, it is generally useful to allow wildcards to unify with user-written type variables! We could, I suppose, notice that polymorphic recursion is happening and then impose the restriction, but that seems very unpredictable to a user.

What do you think? Have you pondered this particular corner case?

Interesting question. In general, we definitely unify wildcards with user-written type variables. This is implied by a guiding design principle that we have used: a function with a trivial partial signature ":: _ => _" should be treated the same as one with no signature at all. We even share most of the code that does inference for definitions with partial type signatures with the code for definitions with no signature. Note: this sharing is something Thomas has worked on recently, after discussion with SPJ. As for your concrete example, I have tried it on our current branch and here's an overview of what we get for the function definition "bar _ _ = bar not True", depending on the provided signature: signature result inferred type/error no signature works (Bool -> Bool) -> Bool -> t _ -> _ -> () works (Bool -> Bool) -> Bool -> () _ works (Bool -> Bool) -> Bool -> t _ -> a -> () doesn't work Couldn't match type ‘a’ with ‘Bool’ (a -> _) -> a -> () doesn't work Couldn't match type ‘a’ with ‘Bool’ So in general, if there is a partial type signature, the compiler tries to infer a type under the assumption that there is no polymorphic recursion, similar to what it does when there is no signature. Regards, Dominique

Great -- this agrees with the current proposal at the type level ((NEWCUSK) in the language of #9200.) Thanks for the quick response! Richard On Jun 19, 2014, at 6:00 PM, Simon Peyton Jones wrote:

| So in general, if there is a partial type signature, the compiler | tries to infer a type under the assumption that there is no | polymorphic recursion, similar to what it does when there is no | signature.

Yes. The way to think of it (at both term and type level) is this.

A full type signature breaks dependency loops, and supports polymorphic recursion.

A partial type signature is treated exactly like *no* type signature, except that extra typing constraints are added. Where the signature has a variable, we insist that the result is a variable; where the signature are distinct variables we insist that the final inferred type has distinct variables. Moreover, the explicitly mentioned variables can lexically scope over the definition.

But no polymorphic recursion at all, with a partial type signature.

Simon