Re: [isabelle] Operator clash for $



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

On 16/06/16 11:54, Manuel Eberl wrote:
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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.