What is a "simple pattern binding"?
Section 4.4.3.2 of the 2010 Haskell report says: 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. This makes it sound as though p is a pattern, which I assume means what section 3.17 defines as the non-terminal "pat". pat -> lpat qconop pat | lpat This is further suggested by the explicit mention of ~, which would be redundant if p had to be a var, since variables always match (according to section 3.17.2 rule 1). So my reading of section 4.4.3.2 is that the following is considered a simple pattern binding (because it has no guards): (f, g) = (\x -> x, f) However, section 4.5.5 seems to contradict this. It reads: Recall that a variable is bound by either a function binding or a pattern binding, and that a simple pattern binding is a pattern binding in which the pattern consists of only a single variable (Section 4.4.3). Moreover, it goes on to give an example and explanation: [(n,s)] = reads t ... Hence, when non-simple pattern bindings are used This text makes it sound as though a "simple pattern binding" can have only a single variable to the left of the = sign, meaning: f = \x -> x Further confusing things, GHC accepts the following: g1 x y z = if x>y then show x ++ show z else g2 y x g2 :: (Show a, Ord a) => a -> a -> String g2 | False = \p q -> g1 q p () | otherwise = \p q -> g1 q p 'a' where x = True and infers type: g1 :: (Show a, Show a1, Ord a1) => a1 -> a1 -> a -> [Char] According to 4.4.3.2, g2 definitely does not have a simple pattern binding, as its binding is not of the form p = e where p is a pattern. Yet by section 4.5.5, if g2 were not considered a simple pattern binding, the constrained type variables in the binding group containing g1 and g2 (in particular the inferred type (Show a => a) of z in g1) would not be allowed to be generalized. So is section 4.4.3.2 of the Haskell 2010 report just wrong? Or is GHC allowing code prohibited by the standard? Or am I somehow misreading the standard? Anyway, if someone can provide a less ambiguous definition of the term "simple pattern binding", I would appreciated it, particularly if you can point to support for your definition in the Haskell 2010 report... Thanks, David
On 2011-06-25 10:52, David Mazieres wrote:
Further confusing things, GHC accepts the following:
g1 x y z = if x>y then show x ++ show z else g2 y x
g2 :: (Show a, Ord a) => a -> a -> String g2 | False = \p q -> g1 q p () | otherwise = \p q -> g1 q p 'a' where x = True
and infers type:
g1 :: (Show a, Show a1, Ord a1) => a1 -> a1 -> a -> [Char]
According to 4.4.3.2, g2 definitely does not have a simple pattern binding, as its binding is not of the form p = e where p is a pattern. Yet by section 4.5.5, if g2 were not considered a simple pattern binding, the constrained type variables in the binding group containing g1 and g2 (in particular the inferred type (Show a => a) of z in g1) would not be allowed to be generalized.
It appears to me that GHC is justified. According to 4.5.1 and 4.5.2, g1 by itself constitutes a declaration group. It is considered by itself and is generalized prior to combining it with g2. I agree that the report is confusing in its use of "simple pattern binding".
At Sat, 25 Jun 2011 14:20:52 -0400, Scott Turner wrote:
g1 x y z = if x>y then show x ++ show z else g2 y x
g2 :: (Show a, Ord a) => a -> a -> String g2 | False = \p q -> g1 q p () | otherwise = \p q -> g1 q p 'a' where x = True
It appears to me that GHC is justified. According to 4.5.1 and 4.5.2, g1 by itself constitutes a declaration group. It is considered by itself and is generalized prior to combining it with g2.
I agree that the report is confusing in its use of "simple pattern binding".
Great, now I'm even more confused. 4.5.1 says: 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 2. b1 depends on a binding that depends on b2. A declaration group is a minimal set of mutually dependent bindings. Hindley-Milner type inference is applied to each declaration group in dependency order. So here the first binding (of g1) contains the free identifier g2, which is bound by the second binding. Conversely, the second binding contains g1 free. So the two bindings are mutually dependent, no? In fact, section 4.5.2 goes on to use the following example for a declaration group: f x = let g1 x y = if x>y then show x else g2 y x g2 p q = g1 q p in ... This example is very close to the code I gave. How can my example have two declaration groups when this example has only one? David
g1 x y z = if x>y then show x ++ show z else g2 y x
g2 :: (Show a, Ord a) => a -> a -> String g2 | False = \p q -> g1 q p () | otherwise = \p q -> g1 q p 'a' where x = True
It appears to me that GHC is justified. According to 4.5.1 and 4.5.2, g1 by itself constitutes a declaration group. It is considered by itself and is generalized prior to combining it with g2.
Great, now I'm even more confused. 4.5.1 says:
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
2. b1 depends on a binding that depends on b2.
A declaration group is a minimal set of mutually dependent bindings. Hindley-Milner type inference is applied to each declaration group in dependency order.
So here the first binding (of g1) contains the free identifier g2, which is bound by the second binding. Conversely, the second binding contains g1 free. So the two bindings are mutually dependent, no?
No, the binding of g1 doesn't depend on the binding of g2, because g2 has a type signature (clause 1). The type of g1 is inferred using the declared type of g2. Then that type is used in inferring a type for g2, which will be compared with its declared signature.
At Sun, 26 Jun 2011 00:17:12 +0100, Paterson, Ross wrote:
g1 x y z = if x>y then show x ++ show z else g2 y x
g2 :: (Show a, Ord a) => a -> a -> String g2 | False = \p q -> g1 q p () | otherwise = \p q -> g1 q p 'a' where x = True
It appears to me that GHC is justified. According to 4.5.1 and 4.5.2, g1 by itself constitutes a declaration group. It is considered by itself and is generalized prior to combining it with g2.
Great, now I'm even more confused. 4.5.1 says:
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
2. b1 depends on a binding that depends on b2.
A declaration group is a minimal set of mutually dependent bindings. Hindley-Milner type inference is applied to each declaration group in dependency order.
So here the first binding (of g1) contains the free identifier g2, which is bound by the second binding. Conversely, the second binding contains g1 free. So the two bindings are mutually dependent, no?
No, the binding of g1 doesn't depend on the binding of g2, because g2 has a type signature (clause 1).
I thought "no type signature" meant no type signature inside b1. Otherwise, you are saying nothing could depend on a binding with a type signature. By that logic, there can be no mutual dependence, and so every declaration with a type signature is its own (singleton) declaration group. But this can't be what the committee was thinking given the following language in section 4.5.2: 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. Such a restriction would be vacuous if every type signature created a singleton declaration groups. Moreover, section 4.5.5 is also inconsistent with such an interpretation: The monomorphism restriction Rule 1. 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. If every binding with an explicit type signature is its own declaration group, then why isn't the monomorphism restriction stated more simply as follows? (a): every binding is a function binding, or (b): the group consists of a pattern binding with an explicit type signature. When they say "an explicit type signature is given for every variable in the group..." they have to be thinking there may be more than one of them.
The type of g1 is inferred using the declared type of g2. Then that type is used in inferring a type for g2, which will be compared with its declared signature.
Thanks for the reply, but now I'm now even more confused. Perhaps I should ask if someone can give me a better definition of declaration group, ideally with support in the language spec... David
I thought "no type signature" meant no type signature inside b1.
No, it means no type signature for the variable.
Otherwise, you are saying nothing could depend on a binding with a type signature. By that logic, there can be no mutual dependence, and so every declaration with a type signature is its own (singleton) declaration group.
A pattern binding can bind more than one variable. If all the variables bound by a binding have type signatures, that binding is indeed a singleton declaration group.
At Sun, 26 Jun 2011 01:41:01 +0100, Paterson, Ross wrote:
I thought "no type signature" meant no type signature inside b1.
No, it means no type signature for the variable.
Otherwise, you are saying nothing could depend on a binding with a type signature. By that logic, there can be no mutual dependence, and so every declaration with a type signature is its own (singleton) declaration group.
A pattern binding can bind more than one variable. If all the variables bound by a binding have type signatures, that binding is indeed a singleton declaration group.
If this is the case, then multiple sentences in the 2010 report don't make sense, though the way in which they don't make sense sort of depends on what "simple pattern binding" means. Which of the following constitute a simple pattern binding? a. a | False = undefined | otherwise = \x -> x b. Just b = Just (\x -> x) c. Just c | False = undefined | otherwise = Just (\x -> x) d. (d, d') = (\x -> x, d) e. (e, e') | False = undefined | otherwise = (\x -> x, e) If it's any clue, GHC infers a polymorphic type for a only. It infers type "GHC.Prim.Any -> GHC.Prim.Any" for the others. Moreover, GHC accepts the type signature "a :: t -> t", but rejects such a polymorphic signature for the other variables, and also rejects programs such as: Just b = Just (\x -> x) f :: (Show a) => a -> a f = b -- illegal So let's work under the assumption that a is a simple pattern binding, and the others are not. If you have a different definition, I'll make a different argument. (Note also that if you agree with this definition, then there is a bug in section 4.4.3.2 of the report, since a is not of the form "p = e". But if you take the 4.4.3.2 definition, then I'll argue section 4.5.5 has a bug.) Let's posit a definition that accepts only a (and in particular that rejects d and e). Such a definition is further supported by the phrase "a simple pattern binding is a pattern binding in which the pattern consists of only a single variable" (from section 4.5.5). If we accept that a simple pattern binding cannot bind more than one variable, then the definition of the monomorphism restriction in section 4.5.5 is not consistent with your interpretation of the term declaration group. After all, given our posited definition, the following language in 4.5.5: (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. should instead read: (a): every binding is a function binding, or (b): the group consists of a simple pattern binding with an explicit type signature. In particular, why would the report say "an explicit type signature is given for EVERY variable" when there can be only one such variable? David
If this is the case, then multiple sentences in the 2010 report don't make sense, though the way in which they don't make sense sort of depends on what "simple pattern binding" means.
Indeed, the Report has two problems: Sections 4.4.3.2 and 4.5.5 have different definitions of "simple pattern". This has been there since section 4.5.5 (Monomorphism Restriction) was added in Haskell 1.1. But then the only technical use of the term is in section 4.5.5. When the definition of declaration group (section 4.5.1) was changed in Haskell 2010 to break dependencies on type signatures, Rule 1 of the Monomorphism Restriction (section 4.5.5), while not incorrect, became partially redundant and overly complex. It could have been simplified along the lines you describe.
At Sun, 26 Jun 2011 09:31:05 +0100, Paterson, Ross wrote:
Indeed, the Report has two problems:
Sections 4.4.3.2 and 4.5.5 have different definitions of "simple pattern". This has been there since section 4.5.5 (Monomorphism Restriction) was added in Haskell 1.1. But then the only technical use of the term is in section 4.5.5.
When the definition of declaration group (section 4.5.1) was changed in Haskell 2010 to break dependencies on type signatures, Rule 1 of the Monomorphism Restriction (section 4.5.5), while not incorrect, became partially redundant and overly complex. It could have been simplified along the lines you describe.
Aha! This is starting to make sense! Indeed the Haskell98 text is far clearer, and when I look at the differences in section 4.5.1, I start to understand what the committee meant. Still, the clause b1 contains a free identifier that has no type signature and is bound by b2 applies the phrase "has no type signature" to the identifier, not to the binding. Such phrasing does not exclude expression type-signatures. I presume that in the following code, binding b1 does not depend on b2: (x, y) = (z, 1) -- call this binding b1 (z, _) = (2, y) -- call this binding b2 w = 1 + (z :: Double) So my reading was that they meant "has no type signature *in b1*". I take it that your reading is that they meant: b1 contains a free identifier that is bound by b2 and b2 is accompanied by a type signature for that identifier I think, given the ambiguities here, it's worth filing a ticket on the haskell' web site. Thank you. David
Still, the clause
b1 contains a free identifier that has no type signature and is bound by b2
applies the phrase "has no type signature" to the identifier, not to the binding. Such phrasing does not exclude expression type-signatures.
True. That ambiguity could be avoided by adding the word "declaration" after "type signature".
Still, the clause
b1 contains a free identifier that has no type signature and is bound by b2
applies the phrase "has no type signature" to the identifier, not to the binding. Such phrasing does not exclude expression type-signatures.
True. That ambiguity could be avoided by adding the word "declaration" after "type signature".
On second thoughts, this is unnecessary. The Report consistently uses "expression type signature" for the expression and "type signature" for the declaration.
At Sun, 26 Jun 2011 21:15:06 +0100, Paterson, Ross wrote:
True. That ambiguity could be avoided by adding the word "declaration" after "type signature".
On second thoughts, this is unnecessary. The Report consistently uses "expression type signature" for the expression and "type signature" for the declaration.
I already sent the haskell-prime mailing list a proposal for the following wording: 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 http://www.haskell.org/pipermail/haskell-prime/2011-June/003482.html I think this is clearer, but it might make more sense to discuss on haskell-prime. David
On 26/06/2011 09:31, Paterson, Ross wrote:
If this is the case, then multiple sentences in the 2010 report don't make sense, though the way in which they don't make sense sort of depends on what "simple pattern binding" means.
Indeed, the Report has two problems:
Sections 4.4.3.2 and 4.5.5 have different definitions of "simple pattern". This has been there since section 4.5.5 (Monomorphism Restriction) was added in Haskell 1.1. But then the only technical use of the term is in section 4.5.5.
When the definition of declaration group (section 4.5.1) was changed in Haskell 2010 to break dependencies on type signatures, Rule 1 of the Monomorphism Restriction (section 4.5.5), while not incorrect, became partially redundant and overly complex. It could have been simplified along the lines you describe.
Indeed, I have on my ToDo list for the Haskell report: Fix confusion about "simple pattern binding" terminology in Sec 4. we should try to fix this in Haskell 2012. Cheers, Simon
participants (4)
-
dm-list-haskell-cafe＠scs.stanford.edu -
Paterson, Ross -
Scott Turner -
Simon Marlow