[Haskell-cafe] Re: Re: aggressiveness of functional dependencies

8 Nov 2006

      Last post until a response I promise! Another demonstration:

bar () = runIdentity . flip runStateT 0 $ return 'c'

Inferred signature:
   bar :: (Monad (StateT s Identity), Num s) => () -> (Char, s)

Why not?
   bar :: Num s => () -> (Char, s)

I am not coming up with an s that could prevent (StateT s Identity)
from being a monad. Is there one?

Nick

On 11/7/06, Nicolas Frisby  wrote:
...
Having thought longer about it, it seems to be an issue with
functional dependencies and overlapping instances.
Perhaps, because an overlapping instance may be defined in some other
module which would trump the Iso instance for Either, the type
inference mechanism cannot commit to the instance presented in my
code. It's being conservative.
My confusion stems from the notion of functional dependency. Given the
functional dependencies of Iso, there is exactly one type b for any
type a such that Iso a b (and also vice versa). Thus it would seem
that c for Iso (Either a b) c is always uniquely determined because of
the instance from my code.
However, because a more specific overlapping instance could always be
added, this isn't the case. That more specific instances could specify
something like Iso (Either Char Char) (Either Int Int). The functional
dependency check does not recognize that this violates the
dependencies introduced by the more general instance's context. I
think this is because said dependencies (the inductives: Iso f f' and
Iso g g') are introduced iff the more general instance fires.
Is the type inference conservative because the possibility of a new
overlapping instance always looms? If so, is this a good thing or a
bad thing? Is this the "murky water" that Strongly Typed Heterogeneous
Collections mentions?
Sorry to double post. Thanks again,
Nick
On 11/6/06, Nicolas Frisby  wrote:
...
I have a question about functional dependencies, instance contexts,
and type inference. A specific example and question is in the attached
code.
In brief the question is: to what degree does type inference use the
functional dependencies of an instance's class and context? I believe
I am wishing it were more aggressive than it is. Please note that I
have not enabled overlapping instances.
Any suggestions regarding how to get the inferred type of |rite_t1| to
be the one I anticipated would be much appreciated. Of course, I would
also appreciate explanations of why I shouldn't anticipate it!
The rest of this message is a copy of the attached code.
Thanks,
Nick
I'm using GHC 6.6, but I see the same inferred types with 6.4.1.
...
{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-} -- for the coverage condition
module FunDepEx where
A plain ole' isomorphism class.
...
class Iso a b | a -> b, b -> a where
    rite :: a -> b
    left :: b -> a
Isomorphism lifts through the sum bifunctor.
...
bifmap_either f g = either (Left . f) (Right . g)
instance ( Iso f f', Iso g g'
         ) => Iso (Either f g) (Either f' g') where
    rite = bifmap_either rite rite
    left = bifmap_either left left
Some types to play around with.
...
newtype MyChar = MyChar Char deriving (Show, Eq)
instance Iso MyChar Char where
    rite (MyChar c) = c
    left c = MyChar c
instance Iso Char MyChar where
    rite c = MyChar c
    left (MyChar c) = c
My type inference confusion follows; the unit arguments are just to
suppress the monomorphism restriction.
...
t1 :: Either Char a
t1 = Left 'c'
rite_t1 () = rite t1
The inferred type for rite_t1 is
rite_t1 :: (Iso (Either Char a) (Either f' g')) => () -> Either f' g'
Why isn't the inferred type of rite_t1 the same as the ascribed type
of rite_t1'?
...
rite_t1' :: Iso b b' => () -> Either MyChar b'
rite_t1' () = rite t1