Proposal: fix "simple pattern binding" and "declaration group"
The Haskell 2010 report contains ambiguous and sometimes contradictory definitions of the terms "simple pattern binding" and "declaration group". The confusion is compounded by the phrasing of the monomorphism restriction, which is carried over from the Haskell98 report in which a different definition of declaration group required a more complicated description of the monomorphism restriction. A recent thread on the haskell cafe mailing list summarizes the problem: http://www.haskell.org/pipermail/haskell-cafe/2011-June/093488.html To resolve this confusion, I propose applying the following changes to the Haskell 2010 report for the next revision of the language: In section "4.4.3.2 Pattern bindings", replace: - A pattern binding binds variables to values. A simple pattern - binding has form p = e. The pattern p is matched “lazily” as - an irrefutable pattern, as if there were an implicit ~ in - front of it. See the translation in Section 3.12. With the following: A pattern binding binds variables to values. A /simple/ pattern binding is one in which the pattern consists of a single variable, yielding a declaration of the form /var/ /rhs/. Recall from section 3.17 that such a pattern is always irrefutable. In section 4.5.1, replace this text: - A binding b1 depends on a binding b2 in the same list of - declarations if either - - 1. b1 contains a free identifier that has no type signature - and is bound by b2, or with the following: A binding b1 depends on a binding b2 in the same list of declarations if either 1. b1 contains a free identifier v, v is bound by b2, and the list of declarations does not contain a type signature for v; or Add the following text to the end of section 4.5.1: For example, the following two bindings form a single declaration group, as each contains a free identifier bound by the other and, despite the presence of expression type-signatures, the declaration list contains no type signatures: (x, y) = (z :: Int, 1 :: Int) -- binds y, has z free (z, t) = (2 :: Int, y :: Int) -- binds z, has y free Conversely, the following two bindings constitute two different declaration groups. Even though f and g contain each other as free identifiers, the declaration list contains a type signature for f, so g does not depend on f. f :: (Eq a) => (a, a) -> (Bool, a) f = \(x, y) -> (x == y, snd (g (x, y))) g pair = (fst (f pair), snd pair) Note that if b is a function binding or simple pattern binding and b is accompanied by a type signature, then b always constitutes a /singleton/ declaration group, regardless of what free identifiers it contains. (If b is a non-simple pattern binding, it may bind multiple variables simultaneously.) Finally, change Rule 1 of the monomorphism restriction in section 4.5.5, by replacing the following text: - We say that a given declaration group is unrestricted if and - only if: - - (a): every variable in the group is bound by a function - binding or a simple pattern binding (Section 4.4.3.2), - and - - (b): an explicit type signature is given for every variable in - the group that is bound by simple pattern binding. with the following: We say that a given declaration group is unrestricted if and only if: (a): every variable in the group is bound by a function binding, or (b): the group consists of exactly one binding, the binding is a simple pattern binding of some variable v, and the binding's declaration list contains an explicit type signature for v. If there is agreement on these changes or something along these lines, I can create a ticket and/or wiki page. I propose the name SimplePatternBinding for the change. David
A recent thread on the haskell cafe mailing list summarizes the problem:
http://www.haskell.org/pipermail/haskell-cafe/2011-June/093488.html
To resolve this confusion, I propose applying the following changes to
the Haskell 2010 report for the next revision of the language: I think bug fixes get applied directly to the Report, once there's agreement on the fix. I don't believe the definition of "depends" in Section 4.5.1 needs to change. The Report consistently uses "expression type signature" for the expression and "type signature" for the declaration, so it is clear that the latter is meant here. In contrast, there's a clear error in the definition of "simple pattern binding": 4.4.3.2 Pattern bindings: "A /simple/ pattern binding has form p = e." 4.5.5 The Monomorphism Restriction: "Recall that ... a /simple/ pattern binding is a pattern binding in which the pattern consists of only a single variable (Section 4.4.3)." This conflict has apparently been there since the MR was introduced in Haskell 1.1. They're talking about different things, and I think the fix is to separate them (though 4.4.3.2 doesn't make much use of its version). That is, remove or rename the definition in 4.4.3.2, and have the definition of "simple pattern binding" introduced locally in 4.5.5 without the back references to 4.4.3. I also agree that Rule 1 of the Monomorphism Restriction (4.5.5) became partially redundant when the definition of dependency (4.5.1) was changed in Haskell 2010, and should have been simplified.
Finally, change Rule 1 of the monomorphism restriction in section 4.5.5, by replacing the following text:
- We say that a given declaration group is unrestricted if and - only if: - - (a): every variable in the group is bound by a function - binding or a simple pattern binding (Section 4.4.3.2), - and - - (b): an explicit type signature is given for every variable in - the group that is bound by simple pattern binding.
with the following:
We say that a given declaration group is unrestricted if and only if:
(a): every variable in the group is bound by a function binding, or
(b): the group consists of exactly one binding, the binding is a simple pattern binding of some variable v, and the binding's declaration list contains an explicit type signature for v.
We could simplify that even further: We say that a given declaration group is unrestricted if it comprises either (a): one or more function bindings, or (b): a simple pattern binding for a variable that has a type signature. Note that it follows from the definition in Section 4.5.1 that such a binding always constitutes a declaration group by itself.
At Mon, 27 Jun 2011 00:06:09 +0100, Paterson, Ross wrote:
I don't believe the definition of "depends" in Section 4.5.1 needs to change. The Report consistently uses "expression type signature" for the expression and "type signature" for the declaration, so it is clear that the latter is meant here.
Okay, but what about at least adding a couple of examples of declaration groups? The Haskell98 report is very clear about what a declaration group is. The 2010 report definition is extremely terse and borderline ambiguous. Even if the report is 90% consistent about using the term "expression type signature", it is not 100% consistent and more importantly never explicitly says that in the absence of the word "expression", the term "type signature" always means declaration type signature when both readings make sense. A reader could reasonably expect that a phrase such as "an expression with an expression type signature" might sometimes be shortened to "an expression with a type signature" when it is clear one is talking about expression type signatures. For example, section 3.13 ends with the note: case x of { (a,_) | let b = not a in b :: Bool -> a } ... Programmers are advised, therefore, to avoid guards that end with a type signature. The example inspiring this advice clearly contains an expression type signature, not a "normal" type signature. Moreover, it is not possible for a guard to end with a non-expression type signature, so the report clearly means "avoid guards that end with an expression type signature"--the word expression has been dropped because it is clear from context. Unfortunately, the context of section 4.5.1 provides less help. 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) Thanks to your email on haskell cafe, I now understand that the spec considers these two bindings as one declaration group, which explains why GHC rejects the program. I assume this is to facilitate type checking at the time of type inference (which, if so, might be worth pointing out to help the reader's intuition). By contrast, the Haskell98 report is dead clear that both bindings above form a single declaration group and hence that the program should be rejected. But someone familiar with Haskell98 might read section 4.5.1 of the 2010 report and say "oh, they seem to want to shrink declaration groups by breaking dependencies when a programmer-specified type can short-cut type inference." That leads to interpreting "a free identifier that has no type signature" as a more concise formulation of "a free identifier that has neither an expression type signature nor a normal type signature in the declaration list." 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.
We could simplify that even further:
We say that a given declaration group is unrestricted if it comprises either
(a): one or more function bindings, or
(b): a simple pattern binding for a variable that has a type signature. Note that it follows from the definition in Section 4.5.1 that such a binding always constitutes a declaration group by itself.
Yes, I much prefer your formulation to mine. Succinct and very clear. David
For example, section 3.13 ends with the note:
case x of { (a,_) | let b = not a in b :: Bool -> a }
... Programmers are advised, therefore, to avoid guards that end with a type signature.
I would support changing "a type signature" to "an expression type signature" in this note for consistency.
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.
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
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
Once you guys have reached consensus on appropriate revised wording for this issue, I'll happily apply the changes to the Haskell 2012 Report as a bugfix. Regards, Malcolm
participants (3)
-
dm-list-haskell-prime＠scs.stanford.edu -
Malcolm Wallace -
Paterson, Ross