Proposal: Partial Type Signatures - Status update

[Richard Eisenberg]

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 <thomas.winant at cs.kuleuven.be> 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#PartialExpressionandPatternSignatures
> [2]: https://ghc.haskell.org/trac/ghc/wiki/PartialTypeSignatures#LocalDefinitions
> 
> 
> 
>> On Apr 10, 2014, at 3:48 AM, Thomas Winant <Thomas.Winant at cs.kuleuven.be> 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 at haskell.org
>>> http://www.haskell.org/mailman/listinfo/ghc-devs
> 
> Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm