Email Gateway (Aug 22 2022 at 13:37): Email Gateway (Aug 22 2022 at 13:37):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
it appears that the infix operator $ is used both for the n-th component
of a vector and the n-th coefficient of a Formal Power Series.
Since I now use both Multivariate_Analysis and Formal_Power_Series, I
get lots of syntax ambiguity warnings all the time. We should probably
do something about this.
I see the following three options:
Rename one of the operators. Since Formal_Power_Series is used less
than vectors, this is probably the one to change in this case. I am not
sure, however, what it could be renamed to. The standard mathematical
notation is something like "[X^n] f", so I suppose we could go for
"⟨X^n⟩ f", but I'm not sure if that's a good idea.
Disable the "$" notation completely outside the FPS theory, or put it
in a locale that has to be interpreted every time one wants to use the
notation. On the down side, one still runs into problems when one wants
to use the $ notation for FPSs but has Multivariate_Analysis loaded as
well. I guess one could put both of them in locales, but I don't know if
we want that.
Use ad-hoc Overloading, similar to what is done for monads. One could
then also use $ e.g. for the n-th coefficient of a polynomial, or
perhaps even unify the notation with the n-th element of lists and
arrays etc. at some point. The down side of this is that when there are
ambiguities/type errors, the error messages get a bit confusing.
Note that "normal" overloading does not work, since the constant would
have to have the type "'a => nat => 'b", and that means one has to write
type annotations everywhere.
Any opinions? Whatever the outcome is, I will take care of implementing it.
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 13:37):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Note that starting from a59801b7f125 bundles have become a convenient
mechanism to organize modularized syntax. The »$« notation would be a
nice candidate to demonstrate that.
Cheers,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 13:37):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Manuel,
The $ notation is used also in other places of the HOL Library, e.g., in
Library/FinFun_Syntax and HOLCF/Cfun. I'd recommend that the operations by default use
subscripts for disambiguation, e.g. (we can discuss about the concrete subscripts),
op $\<^sub>v for vectors
op $\<^sup>p for formal power series
op $\<^sup>f for FinFun
In HOLCF/Cfun, Rep_cfun uses \<cdot> in jEdit, so one could in theory drop the ASCII
notation there.
Then, if a user wants to use several of the theories at the same time, she can always use
unambiguous syntax. However, typing subscripts can be annoying, so there should be support
for users that use only one of the theories. Makarius recently [1] renovated bundles to
support that. Then, users can install their op $ syntax for what they want in one line.
I am against adhoc_overloading, because the type error messages just get incomprehensible
and adhoc_overloading is not complete (in some cases, it fails to find a resolution of
overloading, but when I add type annotations, then it succeeds).
[1] https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2016-June/006891.html
Andreas
Email Gateway (Aug 22 2022 at 13:37):From: Tobias Nipkow <nipkow@in.tum.de>
I would like to see the following setup:
$ is for vector subscripting, its main use.
When combining multiple definitions of $, it should be possible to retain one
of the $ while giving new syntax to the others.
It would be suboptimal if we would need to sprinkle additional lines all over
MVA to cater for potential conflicts.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 13:40):From: Makarius <makarius@sketis.net>
On 16/06/16 12:08, Andreas Lochbihler wrote:
Hi Manuel,
The $ notation is used also in other places of the HOL Library, e.g., in
Library/FinFun_Syntax and HOLCF/Cfun. I'd recommend that the operations
by default use subscripts for disambiguation, e.g. (we can discuss about
the concrete subscripts),op $\<^sub>v for vectors
op $\<^sup>p for formal power series
op $\<^sup>f for FinFun
(This thread still seems to be unresolved.)
How about this?
$ for vectors
$\<^sup>p for formal power series
$\<^sup>f for FinFun
Then, if a user wants to use several of the theories at the same time,
she can always use unambiguous syntax. However, typing subscripts can
be annoying
How about this in etc/abbrevs?
"$" = "$\<^sub>f"
"$" = "$\<^sub>p"
Makarius
Last updated: Nov 21 2024 at 12:39 UTC