[Haskell-cafe] Re: aggressiveness of functional dependencies

Nicolas Frisby nicolas.frisby at gmail.com
Tue Nov 7 13:39:02 EST 2006


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