Iterator syntax

[lukaszcz]

• Closes Special syntax for folds, maps, etc #1992

A function identifier fun can be declared as an iterator with

syntax iterator fun;

For example:

syntax iterator for;
for : {A B : Type} -> (A -> B -> A) -> A -> List B -> List A;
for f acc nil := acc;
for f acc (x :: xs) := for (f acc x) xs;

Iterator application syntax allows for a finite number of initializers acc := a followed by a finite number of ranges x in xs. For example:

for (acc := 0) (x in lst) acc + x

The number of initializers plus the number of ranges must be non-zero.

An iterator application

fun (acc1 := a1; ..; accn := an) (x1 in b1; ..; xk in bk) body

gets desugared to

fun \{acc1 .. accn x1 .. xk := body} a1 .. an b1 .. bk

The acc1, ..., accn, x1, ..., xk can be patterns.

The desugaring works on a purely syntactic level. Without further restrictions, it is not checked if the number of initializers/ranges matches the type of the identifier. The restrictions on the number of initializers/ranges can be specified in iterator declaration:

syntax iterator fun {init: n, range: k};
syntax iterator for {init: 1, range: 1};
syntax iterator map {init: 0, range: 1};

The attributes (init, range) in between braces are parsed as YAML to avoid inventing and parsing a new attribute language. Both attributes are optional.

[janmasrovira]

• See style #2139 for some style changes

We should have a test that shows the syntax for multiple initializers/ranges.
I propose that the syntax for that follows this schema:

fun (acc1 := a1; .. ; accn := an) (x1 in b1; .. ; xk in bk) body

[janmasrovira]

• @lukaszcz have you considered how this syntax (specially initializers) could interact with the proposed syntax in Optional and named arguments #1991?

[lukaszcz]

• @lukaszcz have you considered how this syntax (specially initializers) could interact with the proposed syntax in Optional and named arguments #1991?

Yes, there is a possibility of ambiguity, I realise this.

My proposal is for the iterators to take priority.

If one really wants to have a function application with named non-implicit arguments at the beginning, then one can put it in parentheses

(fun) (arg := a)

This would not be parsed as an iterator because an iterator requires an identifier at the front.

This would perhaps be inconvenient if used often, e.g., for the record syntax. But we need something like the with notation anyway that I proposed in the comments (for record update and/or construction), because otherwise record update is already ambiguous with named implicit arguments.

[lukaszcz]

See:

• Add syntax support for record updates #1642
• Add record declaration syntax support  #1641

[lukaszcz]

With a bit more effort in the parser/scoper, one could also recognise when an identifier is an iterator and prioritise iterator syntax only then. But this would require reworking the current iterator parsing concept (to have separate "initializer" and "range" atoms and build (or not) an iterator application only during scoping).