I don't know an algorithm that can always infer the most general types in 
situations like this.  In your example, if you give a signature for the simple 
function (f :: Y Maybe -> Int), and use RelaxedPolyRec, then GHC will happily 
infer the type you want for g.   For RelaxedPolyRec to work its magic, you just 
need to cut the strongly connected component with a type signature - but you 
can cut it anywhere you please.

Interesting example, though.  I've added a test to GHC's regression suite to 
make sure we do infer the right type for g, given the monomoprhic type for f.

Simon

From: haskell-cafe-boun...@haskell.org 
[mailto:haskell-cafe-boun...@haskell.org] On Behalf Of Job Vranish
Sent: 22 June 2010 16:06
To: Haskell Cafe mailing list
Subject: [Haskell-cafe] Inferring the most general type

Esteemed fellow haskellers,

I recently ran into a very simple real life case where Haskell's rules for 
inferring the types for mutually recursive definitions resulted in a type that 
was less general than it could be. It took me a while to realize that the type 
error I was getting wasn't actually a problem with my code. I understand why 
Haskell does this (it infers the strongly connected mutually recursive 
definitions monomorphically), but I think it _could_ infer the more general 
type even with recursive definitions like this.

Here is a simplified example that illustrates the problem:

> import Data.Maybe

> -- The fixed point datatype
> data Y f = Y (f (Y f))

> -- silly dummy function
> maybeToInt :: Maybe a -> Int
> maybeToInt = length . maybeToList

> -- f :: Y Maybe -> Int
> f (Y x) = g maybeToInt x

> g h x = h $ fmap f x

This is the type it wants to infer for g
g :: (Maybe Int -> Int) -> Maybe (Y Maybe) -> Int

This is the type I think it should have, note you can't force the type with a 
typesig without -XRelaxedPolyRec
g :: (Functor f) => (f Int -> b) -> f (Y Maybe) -> b

If I use -XRelaxedPolyRec I can manually specify the more general type, but 
then I have to convince myself that there isn't a more general type that I'm 
missing.


Are there other known algorithms that yield a more general type? and if so, 
what was the rational for Haskell keeping the current method?

I worked out an alternative algorithm that would give a more general type 
(perhaps the most general type) but it has factorial complexity and probably 
wouldn't be good for strongly connected groups with 7 or more members.

Even so, I would much rather have the inferred types always be the most general 
ones and be required to add type signatures for mutually recursive groups with 
7 or more members (which probably need to be redesigned anyway) than be always 
required to manually figure out the more general signatures.
What do you think?


- Job
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Reply via email to