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

[Peter Lammich]

Hi all.


> 
> > The whole point of the new \<^Const> antiquotation is to cultivate
> > a view of
> > Consts.typargs almost everywhere, with very little recomputation of
> > types for
> > subterms (no more Term.fastype_of).
> > 
> You are right with the cost of Term.fastype_of. But many use-cases of
> @{mk_term} are situations where the term size is under control of the
> actual code. 
> There is no additional user-space input coming in. E.g. think of
> something like the
> @{command record} where you have to generate lots of lemmas about 
> field lookup / update etc. There something like @{mk_term} leads to
> very readable and compact code
> to generate the terms for the propositions.

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!)


> 
> 
> > 
> > > Having antiquotations for cterms can be a powerful show-case for
> > > the potential
> > > of antiquotations, bringing together readability / conciseness as
> > > well as
> > > scalability.
> > 
> > This sounds like marketing-speak.
> 
> What I like about the application here is that the antiquation in a
> sense stretches the type-system of ML. 
> What results in a sequence of combinator applications becomes an
> atomic entity.
> 
> > Note that too much complexity in ML antiquotations can degrade the
> > robustness
> > and maintainability of ML tools. For example, too much concrete
> > syntax will
> > lead to surprises after inevitable changes of abbreviations,
> > translations etc.
> > over the years / decades.
> > 
> > With \<^Type> / \<^Const> everything is clear and well-defined.
> > 
> That is certainly true. The more syntax is involved the more can go
> wrong. But in my experience with these antiquotation so far this
> falls in the category of “benign” issues. Meaning that you will hit
> the problem quite early. In the best case
> already at compile time. Or if that does not work the problem
> manifests upon every and thus already the first actual usage of the
> antiquotation.
> In those situations the benefits of a readable and concise term
> overweight.


I agree here. 

Me, personally, am not yet convinced to switch from the very consise
and high-level mk_term / mpat to the still more verbose and low-level
Type/Const. Obviously, I would like to improve these high-level
concepts, but not at the cost of readability or conciseness, which is
exactly what makes them so appealing.

Peter




> 
>   Norbert