Discussion:
[isabelle] Operator clash for $
(too old to reply)
Manuel Eberl
2016-06-16 09:57:07 UTC
Permalink
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:

1. 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.

2. 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.

3. 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
Andreas Lochbihler
2016-06-16 10:13:39 UTC
Permalink
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
Post by Manuel Eberl
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.
1. 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.
2. 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.
3. 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
Makarius
2016-07-25 15:37:37 UTC
Permalink
Post by Andreas Lochbihler
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
Post by Andreas Lochbihler
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

Loading...