aggressiveness of functional dependencies

newer
Announcement: new maintainers forr...

Nicolas Frisby

6 Nov 2006 6 Nov '06

5:09 p.m.

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

Attachments:

FunDepEx.lhs (application/octet-stream — 1.2 KB)

Show replies by date

Nicolas Frisby

7 Nov 7 Nov

1:39 p.m.

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

Nicolas Frisby

8 Nov 8 Nov

6:51 p.m.

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

apfelmus＠quantentunnel.de

9 Nov 9 Nov

8:44 a.m.

Nicolas Frisby wrote:

...

...
...
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

I think GHC does not know whether the given instance declaration instance ... => Iso (Either a b) (Either a' b') even applies to the special case of (a = Char) because it mostly ignores the preconditions on the left side of (=>). Hugs is much different. Maybe throwing away undecidable instances will drastically change things.

...

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?

The same might go on for this case. By not looking at the preconditions in the instance declaration instance Monad m => Monad (StateT s m) GHC concludes that (Monad (StateT s Identity)) might or might not hold depending on s. Regards, apfelmus

Nicolas Frisby

10 Nov 10 Nov

11:35 p.m.

First off, thanks for the reply. I am accustomed to GHC ignoring instance contexts as you mentioned. It's the "mostly" part that I'm curious about: mostly implies there's some phases that don't ignore context. Is that only the checking the type of the method definitions and absolutely nothing else? So it seems... My project is rather committed to GHC, but could you elaborate on your reference to Hugs being different? Thanks again, Nick On 11/9/06, apfelmus@quantentunnel.de wrote:

...

Nicolas Frisby wrote:

...
...
...
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

I think GHC does not know whether the given instance declaration

instance ... => Iso (Either a b) (Either a' b')

even applies to the special case of (a = Char) because it mostly ignores the preconditions on the left side of (=>). Hugs is much different. Maybe throwing away undecidable instances will drastically change things.

...
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?

The same might go on for this case. By not looking at the preconditions in the instance declaration

instance Monad m => Monad (StateT s m)

GHC concludes that (Monad (StateT s Identity)) might or might not hold depending on s.

Regards, apfelmus

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

apfelmus＠quantentunnel.de

11 Nov 11 Nov

7:08 a.m.

Nicolas Frisby wrote:

...

First off, thanks for the reply.

I am accustomed to GHC ignoring instance contexts as you mentioned. It's the "mostly" part that I'm curious about: mostly implies there's some phases that don't ignore context. Is that only the checking the type of the method definitions and absolutely nothing else? So it seems...

I just said "mostly" because I don't know exactly... Though I strongly suspect, like you, that the preconditions are only used in type inference/checking and not for overlapping instances and similar questions related to uniqueness of instance declarations.

...

My project is rather committed to GHC, but could you elaborate on your reference to Hugs being different?

By tradition from Gofer, Hugs implements type classes more flexible than GHC does. I once experimented with the following code using overlapping instances:

...

data Lift a = Lift a type Test = Char

class Message m o where send :: m -> o -> Test

instance Message (o -> Test) o where send m o = m o

instance Message m o => Message m (Lift o) where send m (Lift o) = send m o

msg :: Test -> Test msg = id

r1 = send msg 'a' r2 = send msg (Lift 'b')

It implements some kind of subtyping. GHC won't typecheck this but "hugs -98 +m" will. If I remember correctly, the problem was with instance Message (Lift a -> Test) (Lift a) Does this follow from the first or from the second instance declaration? GHC ignores the precondition in the second declaration, thus believes it follows from both and consequently rejects it. But Hugs has no problems with that: it follows the precondition and sees that the second declaration does not apply to the culprit because there is no (instance (Lift a -> Test) a). Note that if you add this instance later on (perhaps in a different module), things will break. The flexibility comes at a price: Gofer's type class system was unsound and I don't know how much Hugs comes close to this. Regards, apfelmus

6766

Age (days ago)

6771

Last active (days ago)

List overview

Download

5 comments

2 participants

participants (2)

apfelmus＠quantentunnel.de
Nicolas Frisby