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

Nicolas Frisby nicolas.frisby at gmail.com
Wed Nov 8 18:51:32 EST 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 <nicolas.frisby at gmail.com> 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 <nicolas.frisby at gmail.com> 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
> >
> >
> >
>


More information about the Haskell-Cafe mailing list