Re: Functional dependencies, principal types, and decidable type checking

Iavor Diatchki wrote:

Hi,

On Apr 3, 2005 7:33 AM, Manuel M T Chakravarty wrote:

...

Assume the following type class declarations with functional dependencies:

...

{-# OPTIONS -fglasgow-exts #-}

class C a b c | a b -> c where foo :: (a, b) -> c

instance C a a r => C a (b, c) r where foo (a, (b, c)) = foo (a, a)

Now, in GHCi (version 6.4),

...

*FDs> let bar x = foo ((x, x), (x, x)) *FDs> :t bar bar :: (C (a, a) (a, a) c) => a -> c This seems reasonable.

It is reasonable in so far as it is a valid typing, but Haskell (including FDs) comes with the promise of type inference determining principal (as in most general) types.

...

but GHC is also happy to accept the more general type

...

bar :: a -> c bar x = foo ((x, x), (x, x))

We know a -> c <= (C (a, a) (a, a) c) => a -> c where <= is the "is more or as general as" relation, but due to GHCi's answer to ":t bar", it must also be true that (C (a, a) (a, a) c) => a -> c <= a -> c To check whether that relation holds, we need to know the set of satisfiable instances of the predicate "C (a, a) (a, a) c" under the given instance declaration. It seems as if we get infinite inference trees here.

It seems that GHC 6.4 has a new "feature" where it is creating recursive dictionaries (which is sometimes useful). Here is a simpler example of the same behavior:

...

{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}

class T a where t :: a instance T a => T a where t = t

f :: Int f = t GHC accepts this which means that it managed to discharge the constraint "T Int", and the only way it could have done this is by creating a recursive (in this case bottom) dicitionary.

Yes, *but* you have given GHC -fallow-undecidable-instances!! My examples doesn't require that.

...

...

*FDs> let bar x = foo ((x::Int, x), (x, x)) *FDs> :t bar bar :: Int -> () This looks like a bug to me.

This only happens when the functional dependency "a b -> c" is used in the class declaration. I think what is happening is that the type variable that was to the right of the error is "zonk"ed (in error) after type checking.

I think that if an implementation creates recursive dictionaries it may be nice to have some sort of a "progress" check to avoid creating completely undefined dictionaries. I suspect implementing such a thing may be tricky though.

I am actually a bit worried about the type theory of this all. Recursive dictionaries sounds like a cool idea, but what does it mean in terms of typing derivations? Moreover, how does that combine with improving substitutions, such as those used in the implementation of functional dependencies? Manuel