Email Gateway (Aug 22 2022 at 11:50): Email Gateway (Aug 22 2022 at 11:50):From: Michael Norrish <Michael.Norrish@nicta.com.au>
The comment is
(*Substitute arguments for loose bound variables.
Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi).
Note that for ((%x y. c) a b), the bound vars in c are x=1 and y=0
and the appropriate call is subst_bounds([b,a], c) .
Loose bound variables >=n are reduced by "n" to
compensate for the disappearance of lambdas.
*)
The behaviour is to substitute the first term in the list for Bound 0, the second for Bound 1, etc. This doesn't seem to be what the second line of the comment is implying.
Behaviour is visible in
ML {*
Term.subst_bounds ([@{term "x::'a"}, @{term "f::'a => 'b"}], Bound 0 $ Bound 1)
*}
which gives x $ f, rather than f $ x.
Michael
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 11:50):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
I believe the comment is fine, or at least internally consistent. The second line does say "replacing (Bound i) with (argi)", which is what you found out too.
The first half of line 2, about "beta-reduction of arg(n-1)...arg0 into t", did not immediately deliver its meaning to me, but the example "subst_bounds([b,a], c)" (with [b, a] and not [a, b]) illustrates what is meant. In your example, this means you must write
Term.subst_bounds ([@{term "f::'a => 'b"}, @{term "x::'a"}], Bound 0 $ Bound 1)
to obtain f $ x, which is consistent with the beta-reduction
(%y g. g y) x f == f x
i.e. the beta-redex has x f, the list argument to "subst_bounds" has [f, x] in reverse (cf. arg(n-1)...arg0).
Jasmin
Email Gateway (Aug 22 2022 at 11:50):From: Michael Norrish <Michael.Norrish@nicta.com.au>
Right, but why does it then list the args in the order
arg(n-1), ... arg1, arg0
?
I read that as meaning that Bound 0 gets replaced with arg0, and that arg0 is the rightmost element of the list.
If it makes sense to everyone else, I don't mind.
Michael
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 11:50):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Well, the input list is always [args0, ..., args(n-1)]. It's just the corresponding "beta-reduction" that takes the elements in reverse. This could be clearer, but when reading the text under the assumption that "args0" is the first element of the input list (which is reasonable), everything makes sense.
I'm not sure I'd dare to touch any old Larry (?) documentation, but if anybody is willing to clarify the text, I certainly won't stop them. ;)
Jasmin
Email Gateway (Aug 22 2022 at 11:50):From: Makarius <makarius@sketis.net>
These comments belong indeed to ancient tradition from Cambridge. Over
the years, we have fine-tuned many of them, and actually removed the
majority -- because the informal text and the formal explanation in ML did
not agree.
Term.subst_bounds looks a bit old and confusing in various respects, but
it still has a correct reading in the historical context of term.ML, as
already explained by Jasmin.
In general, Isabelle sources are understood as follows (in that order):
(1) reading the definition in ML
(2) looking through typical uses in ML
(3) peeking at the informal snippets around the formal text, without
taking them too seriously
Makarius
Email Gateway (Aug 22 2022 at 11:51):From: Till Mossakowski <till@iws.cs.uni-magdeburg.de>
Note that good software engineering practices would imply the opposite
order.
Best, Till
Email Gateway (Aug 22 2022 at 11:51):From: Lawrence Paulson <lp15@cam.ac.uk>
As the author of both the code and the comment, I can confirm that I always preferred to call this function with singleton lists.
Larry
Email Gateway (Aug 22 2022 at 11:51):From: Makarius <makarius@sketis.net>
Yes, this is what people sometimes say. I am following that with some
interest over 20 years, which some amusement about the fundamental
divergence of theory and practice.
Systems like Isabelle of approx. 30 years of history define their own
single-element category in this game. It would be interesting to look
closely how it was all done, to learn systematically both from the
successes and mistakes.
Apart from the Isabelle sources, I am routinely exposed to the JVM
sources, which are younger and less advanced in many respects. Despite
the relative success of the JVM platform, I see it as a counterexample in
software engineering.
A positive example is probably the Glasgow Haskell Compiler, see also
http://www.aosabook.org/en/ghc.html -- although I have never looked at the
actual sources.
Makarius
Email Gateway (Aug 22 2022 at 11:51):From: Makarius <makarius@sketis.net>
That is why I have called it old-fashioned: in present-day Isabelle, the
canonical operations take only a single argument, and are then used with
"fold" or "fold_rev" for iteration. There is in fact the one-argument
Term.subst_bound as well, although its signature is old-style and requires
an older fold combinator.
The reason why these ancient and important term operations have not been
reformed significantly, is that they are ancient and important. Certain
critical operations depend on them. Too much ambition is likely to cause
problems.
When they are touched again, one question would be if the (raise
Same.SAME) performance tuning is still relevant. The current Poly/ML
runtime system might cope without, but it requires serious empirical
studies.
Makarius
Email Gateway (Aug 22 2022 at 11:51):From: Joachim Breitner <breitner@kit.edu>
Hi,
I have. The GHC sources are full of comments, and one of the main jobs
of Simon Peyton Jones these days seems to be to reply to people who
submit patches to fix bugs or implement new features: „More Notes!“
The concept of Notes is worth describing: Simon has noticed that your
code get harder to read if it is too cluttered by inline comments –
after all, one huge benefit of functional code is its conciseness that
allows you to see more code at once.
OTOH, such code, even if written carefully, often does not explain
itself fully, in particular its interaction with other parts of the
system. So the question arises, where to add this information? Inline
comments are to be avoided if they are longer than a few words. But
stuff in wikis or user guides, or – worse – trac ticket, code reviews,
random READMES or mailing list, quickly goes out of sync with the code.
So the solution is to have Notes, which are extended comments (from a
few lines to several paragraphs), with examples, in the source file,
not within the code in question, but near it (e.g. the bottom of the
fie). They are then referenced from all relevant positions in the code
with, say "See Note [Asymmetry of 'both' for DmdType and DmdResult]".
This alerts everyone who touches an affected function that there is
something non-trivial and non-obvious about the code.
Also, whenever you make a small change to existing code, you are
encouraged to write a Note about it: Because if it were obvious, then
it would have been done like that in the first, place, wouldn’t it?
A quick grep finds 1067 such Notes in GHC’s HEAD.
It still happens that I submit a patch which I think is obvious, and
yet Simon asks me to write a Note, and indeed: Often it would not have
been obvious to me any more after a few months. So all in all, I am
quite fond of this approach, and GHC ability to still evolve and to
take up new contributors shows its strength. But naturally, it needs to
be taken serious, with new contributors trained to follow this style.
Greetings,
Joachim
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC