Re: Proposal: fix "simple pattern binding" and "declaration group"
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 ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: Proposal: fix "simple pattern binding" and "declaration group"
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
RE: Proposal: fix "simple pattern binding" and "declaration group"
> 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
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
Re: Proposal: fix "simple pattern binding" and "declaration group"
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
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
RE: Proposal: fix "simple pattern binding" and "declaration group"
> 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. ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
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 ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
