At Mon, 27 Jun 2011 15:02:33 +0100, Paterson, Ross wrote: > > > There is no a priori reason why b should depend on a in a pair of > > bindings such as these: > > > > a = const (\x -> x) b > > b = const (a :: Int -> Int) (a :: Bool -> Bool) > > There is: section 3.16 says that in an expression type signature e::t, > the type derived for e must be more specific than t. To derive the > type of e, in this case a, before matching it against t, we have no > alternative but to use the definition of a.
I saw this, but I guess I didn't realize it was relevant to 4.5.1. When I read 3.16, the following sentence: the declared type may be more specific than the principal type derivable from exp, but it is an error to give a type that is more general than, or not comparable to, the principal type seemed so obvious that I just glossed over it. There's actually an important point here, which is that in order to infer the type of an expression type-signature e :: t, you first must infer the type of e, and only then check it against t. If this is the intent, it would be clearer to say "more specific than the principle type *derived* from exp", rather than "derivable", since the derivation must actually happen. But in fact, the relation of expression type signatures to type inference is even subtler. Expression type signatures *can* affect type inference in code such as the following: f1 () = 5 where { _ = f2; _ = n } f2 () = f1 () :: Rational -- changes type of n to Rational n = f1 () I guess the rule is that expression type signatures can affect type inference by resolving ambiguities or avoiding defaulting, but not in any other way? To understand that, you have to understand sections 4.5.1 and 4.5.2, meaning we've come full circle. And there's another sentence in 4.5.2 that makes this harder to understand: If the programmer supplies explicit type signatures for more than one variable in a declaration group, the contexts of these signatures must be identical up to renaming of the type variables. This makes it sound like declaration type signatures don't break up declaration groups. I suppose the above sentence is technically applicable for non-simple pattern bindings, but it would be clearer to add something along of the lines of "... type signatures for more than one variable (which can occur when a non-simple pattern binding binds multiple variables)...". > > Even if you don't think the report is ambiguous, it is at least prone > > to misinterpretation, which is why a couple of examples would really > > help at the end of 4.5.1. > > Fair enough. Perhaps the example on the H' page would help: > > http://hackage.haskell.org/trac/haskell-prime/wiki/RelaxedDependencyAnalysis Sure, that's a good example. But it would also be nice to have an example with an expression type signature, maybe with an explanation that references 3.16 to make clear what is going on (and maybe with a change of derivable -> derived in 3.16). David _______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime