[isabelle-dev] NEWS: ML antiquotations for type constructors and term constants

[Peter Lammich]

On Thu, 2021-10-14 at 10:06 +0200, Makarius wrote:
> On 14.10.21 09:49, Peter Lammich wrote:
> > I'm also, in many cases, in favour of clear and readable code over
> > efficient and less readable. (That's the reason why we use
> > functional
> > programming for Isabelle, in first place!)
> 
> The new \<^Type> / \<^Const> antiquotations are designed to be both
> efficient in the runtime, and efficient in the source text (readable,
> maintainable).

but they are clearly less concise than mk_term/pat, at least for some
applications.

The usage of mk_term/pat, and the fact that it has been invented at
least twice independently, indicates that there is some sweet spot
here, which, at least for some use cases, allows a very concise
notation.

This still has some problems in other cases (e.g., treatment of types).
However, this should not be a reason for abandoning this promising
find, but to try to understand it further: in what cases is use of
mk_term/pat adequate, and in what cases do we have to fall back to the
more low-level but robust/general Type/Const. Can we even have both:
the benefit of concise treatment of type arguments AND the benefit of
concise, high-level notation?

--
  Peter

> 
> As usual, it is just a matter to get used to a new way of thinking,
> which is actually closer to the old way of direct use of datatype
> constructors.
> 
> Moreover, the treatment of type arguments is much more concise: the
> term
> (patterns) are rather awkward in that respect: both in the text and
> at
> runtime (fastype_of).
> 
> 
> This thread was mainly meant to figure out shortcomings that can be
> improved further: this often becomes apparent in concrete use, e.g.
> while converting an application to the new format.
> 
> (Doing that here and there, I did already see another are of reform,
> namely "instantiate" forms for thm, cterm, maybe even term.)
> 
> 
> 	Makarius