# [isabelle-dev] NEWS: parameterized antiquotations @{map N}, @{fold N} etc.

Makarius makarius at sketis.net
Wed Oct 22 14:51:40 CEST 2014

```On Wed, 8 Oct 2014, Makarius wrote:

> *** ML ***
>
> * Basic combinators map, fold, fold_map, split_list are available as
> parameterized antiquotations, e.g. @{map 4} for lists of quadruples.

There was an off-list proposal by RenĂ© Thiemann to define the following
antiquotation:

@{map_tuple n} = fn f => fn (x1, .., xn) => (f x1, ..., f xn)

That actually generalizes the existing pairself combinator, which goes as
far back as Isabelle86 (at least).  See its unify.ML:

(*handy functional for tpairs*)
fun pairself f (x,y) = (f x, f y);

Later we found this handy in many more situations, and it has become part
of the standard canon long ago.

Maybe we can unify the old and new sprouts further.  What is the canonical
name for this combinator, potentially with some additional generalization?

ap2 f (x, y) = (f x, f y)
@{ap n} f (x1, ..., xn) = (f x1, ..., f xn)

Maybe even this as well?

@{ap n(k)} f (x1, ..., xn) = (x1, ..., f xk, ..., xn)

That might be occasionally useful to map field 1, or 2, or 3 of a triple:
@{ap 3(1)}, @{ap 3(2)}, @{ap 3(3)}.  The existing combinators apfst, apsnd
fit into the same scheme.

Of course, the Isabelle/Pure bootstrap environment would retain the
important apfst, apsnd, ap2 (renamed from pairself).

> Isabelle/ML has antiquotations as some kind of macro language.  It can
> do certain things better than the C preprocessor, although one always
> needs to be careful to stay within reason.

@{ap n} still seems to be within reason, but @{ap n(k)} might be already
unreasonable.

Is there a better name for that combinator?

Note that "app" is already defined in the SML97 basis: alias for List.app.
Also note that "ap1" would be just an instance of "I", and is rarely used
as such anyway.

Makarius

----------------------------------------------------------------------------
http://stop-ttip.org
----------------------------------------------------------------------------
```