[Haskell-cafe] Generalization of types during inference

[chris done]

Thanks Richard and for the paper link! This answers my question and then some.

Cheers!

On Sun, Jun 7, 2020, at 6:53 PM, Richard Eisenberg wrote:
> Yours is an example of polymorphic recursion, when a function calls itself at a different type than at which it was, itself, called. (What an ugly English construction. Apologies. But it's hard to describe this somehow.) Inference of polymorphic recursion is undecidable in the general case: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.42.3091&rep=rep1&type=pdf
> 
> Some special cases can be inferred, and indeed GHC does a little inference of this in types, in some scenarios. (We'd actually prefer not to, in order to be consistent, but oddly it's hard to avoid in our algorithm.) But generally inferencers avoid trying here.
> 
> Richard
> 
>> On Jun 7, 2020, at 6:46 PM, chris done <haskell-cafe at chrisdone.com> wrote:
>> 
>> I'm writing a type checker with type classes and for some reason thought
>> that the below program should be inferred and generalized automatically. I
>> wasn't sure whether or not GHC would actually accept this or not, so I had to test.
>> 
>> For both Hugs and GHC, a recursive definition's type is not generalized
>> by the inferer. You need a type signature. See below. I checked with
>> Hugs just in case there was a generalization limit in GHC due to its more exotic
>> capabilities (like how let generalization is disabled by type families).
>> 
>> I wonder: is it in general impossible or super hard to infer the most
>> general type for all cases like this without a type signature? Or is it just considered a 
>> rare case that we don't care about? Perhaps it has subtler downsides? 
>> 
>> It any case, I'm happy to just copy GHC and Hugs as it makes my life
>> easier to just require an explicit signature in this case.
>> 
>> Cheers
>> 
>> -- ERROR "Q.hs":4 - Type error in application
>> -- *** Expression : f (n - 1) 'a'
>> -- *** Term : 'a'
>> -- *** Type : Char
>> -- *** Does not match : ()
>> 
>> -- • Couldn't match expected type ‘()’ with actual type ‘Char’
>> -- • In the second argument of ‘f’, namely ‘'a'’
>> -- In the expression: f (n - 1) 'a'
>> 
>> -- f :: Int -> a -> Int
>> f 0 x = 0
>> f 1 x = f 0 ()
>> f n x = f (n-1) 'a'
>> _______________________________________________
>> Haskell-Cafe mailing list
>> To (un)subscribe, modify options or view archives go to:
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>> Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20200607/a84dde98/attachment.html>