Re: Proposal: Partial Type Signatures - Status update

Hi Thomas, 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? Thanks, Richard On Apr 22, 2014, at 10:17 AM, Thomas Winant wrote:

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:

...

...

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

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