Interesting example | class Monad2 m a ma | m a -> ma, ma -> m a where | return2 :: a -> ma | bind2 :: Monad2 m b mb => ma -> (a -> mb) -> mb | _unused :: m a -> () | _unused = \_ -> () | instance Monad2 [] a [a] where | bind2 = error "urk" The functional dependencies say m a -> ma Instantiating this with the instance declaration instance Monad2 [] a [a] we can deduce that given any constraint (Monad2 t1 t2 t3), if t1 = [], then t3 must be [t2] In the instance declaration, we instantiate the type of bind2 to get the type of bind2 needed for this particular instance declaration: bind2 :: forall b mb. Monad2 [] b mb => ma -> (a -> mb) -> mb Now the rule above says "that means mb must be [b]" and that gives rise to the error. GHC is consistent about this --- if you don't supply an defn for bind2, it makes one up, and complains in more or less the same way. Here's a less complicated variant of the same problem: class C a b | a -> b where {} instance C Int Int where {} f :: (C Int b) => Int -> b f x = x Is the defn of f legal? Both GHC and Hugs reject it because the inferred type of f is more like C Int Int => Int -> Int Functional dependencies tell us that 'b' must be Int, so in fact the two types are equivalent. In this example the programmer could write the 'correct' type, but in your case you can't because the type signature arises by instantiating the one in the class declaration. I'm really not sure what to do about this. GHC has an excellent way of keeping me honest in type-checking: the type checker has to produce a translation of the program into the (typed) core language. What could f's translation look like. It must presumably be f (d::C Int Int) (x::Int) = x giving f the type f :: C Int Int -> Int -> Int Another translation could be f b (d::C Int b) (x::Int) = x (the 'b' is a type variable, a big-lambda binding) giving f the type f :: forall b. C Int b -> Int -> Int But what I *cannot* get is the type f : forall b. C Int b -> Int -> b how could I write the term? f b (d:: C Int b) (x::Int) = ????? I suppose I could use (unsafeCoerce x) as the RHS, which amounts to saying "in every call to f, b will be Int, so we know that the coercion is safe". But that is a scarily global property. For example, if a call site of f does not "see" the instance declaration, it might call f with an argument of type (C Int Bool) or something. Nor can I see an easy way to insert the 'right' coercions in general. Bottom line: excellent point, but I can't see how to fix it. Maybe there are some fundep experts out there who can guide us through the swamp? Simon
Hi Simon, all,
Here's a less complicated variant of the same problem:
class C a b | a -> b where {}
instance C Int Int where {}
f :: (C Int b) => Int -> b f x = x
This is interesting, but I'm not entirely sure what the problem is (from a theoretical, not practical, standpoint). Obviously there is no problem in a one module program, so let's assume we have the following modules: module C where class C a b | a -> b where {} module I1 where import C instance C Int Int where {} module I2 where import C instance C Int Bool where {} module U where import C import ? f :: C Int b => Int -> b f x = x Now, there are four cases: 1) U (transitively) imports I1 2) U (transitively) imports I2 3) U (transitively) imports both I1 and I2 4) U (transitively) imports neither I1 nor I2 Suppose we are in case 1. Then the programmer has written a too-general type signature on f. The programmer *must* know that b=Int in this case otherwise his function definition makes no sense. However, I don't really see a reason why this should be an error rather than just a warning. If some other module K imports both U and (for instance) I2, then we'll get a fundep clash and the whole program will be invalid. Suppose we are in case 2. Then the programmer has clearly screwed up because we know b=Bool and x::Int and x::Bool are incompatible. This should clearly be a type error. Case 3 is impossible, as this will be a fundep clash. Case 4 should produce an error (IMO). Of course, there could be a module K which imports this U and also I1 in which case you might argue that this should be allowed, but I don't think that makes much sense.
I suppose I could use (unsafeCoerce x) as the RHS, which amounts to saying "in every call to f, b will be Int, so we know that the coercion is safe". But that is a scarily global property. For example, if a call site of f does not "see" the instance declaration, it might call f with an argument of type (C Int Bool) or something. Nor can I see an easy way to insert the 'right' coercions in general.
Is this possible? In order for this to happen, this evil module M must import U. This means that it has transitively imported I1 and thus has the instance declaration. Or am I missing something. I think the unsafeCoerce x is safe in these cases.
Bottom line: excellent point, but I can't see how to fix it. Maybe there are some fundep experts out there who can guide us through the swamp?
Yes, please! - Hal
Suppose we are in case 1. Then the programmer has written a too-general type signature on f. The programmer *must* know that b=Int in this case otherwise his function definition makes no sense. However, I don't really see a reason why this should be an error rather than just a warning. If some other module K imports both U and (for instance) I2, then we'll get a fundep clash and the whole program will be invalid.
I now retract this comment :). Clearly this is just as bad as saying:
f :: Bool -> b f x = x
since this claims that it will take a Bool and produce a value of type b for all types b. However, would it be all right to say (in pseudo-Haskell):
f :: exists b . Bool -> b f x = x
? Here, we're simply claiming that there is *some* type b for which f takes a Bool and produces a b? I believe this same analysis extends to something like:
class C a b | a -> b where {} instance C Int Int where {} f :: exists b . C Int b => Int -> b f i = i
It seems that this would be legal in a language like haskell but which allowed existensial quantification. Am I correct?
In article <DE924A789E3C124F8C8A319F273357E7014E30CF@lon-msg-01.europe.corp.microso ft.com>, "Simon Peyton-Jones" <simonpj@microsoft.com> wrote:
Here's a less complicated variant of the same problem:
class C a b | a -> b where {}
instance C Int Int where {}
f :: (C Int b) => Int -> b f x = x
Is the defn of f legal? Both GHC and Hugs reject it because the inferred type of f is more like C Int Int => Int -> Int
If this were allowed, it would effectively allow type-lambda. For instance, I have a type function T that maps Int to Bool and Bool to Char: class C a b | a -> b instance C Int Bool instance C Bool Char newtype T a = MkT (forall b.(C a b) => b) helperIn :: (forall b.(C a b) => b) -> T a helperIn b = MkT b; -- currently won't work helperOut :: T a -> (forall b.(C a b) => b) helperOut (MkT b) = b; Here T is a type-constructor that does that. If I like, I can represent Char as "T (T Int)", though of course I need to use the helper functions to actually use it as a Char. -- Ashley Yakeley, Seattle WA
participants (3)
-
Ashley Yakeley -
Hal Daume III -
Simon Peyton-Jones