Optional and named arguments

[lukaszcz]

We could consider adding optional arguments in general. This would generalise the accumulator arguments in recursive lambdas (issue #1638). Plus, optional arguments are useful independently.

But for them to fit into our syntax we would need to require the following.

1. Forbid multi-clause definitions with optional arguments: if there are optional arguments then the definition has only one clause. For example:

fun : Nat -> Nat -> Nat;
fun (n := 0) m := n + m;

Then it makes sense that for a lambda the optional arguments can be declared before the lambda, like with go below:

go(acc1 := [])(acc2 := 0)@\{
     []        := (acc1, acc2)
   | (x :: xs) := go (acc1 := x :: acc1) (acc2 := acc2 + 1) xs
  };

Then inside the lambda we can have multiple pattern matching clauses. This generalises the accumulator arguments to recursive lambdas (issue #1638).
2. The optional arguments can only be provided in an application by explicitly naming them, to avoid ambiguity with partial application, e.g., go (acc1 := x :: acc1) (acc2 := acc2 + 1) xs.
3. Perhaps we should somehow indicate the optionality of arguments in the type? Otherwise, the types are confusing. For example:

fun : ?(n : Nat) -> Nat -> Nat;
fun (n := 0) m := n + m;

[janmasrovira]

Would it be correct to think about optional arguments in the following way?

• An optional argument behaves as an implicit argument except that when it is omitted, the default value is inserted instead of a hole.

If so, we could use the following syntax:

fun : {n := 0 : Nat} -> Nat -> Nat;

This syntax has the advantages:

1. The braces {} already hint at the optionality, since we also use them for implicit arguments. So we don't need special ? syntax.
2. Since the default value is given in the type signature, the function is allowed to have multiple clauses. So we drop restriction 1.

About restriction 2. Is the behavour that you have in mind as follows?
Given a function with named arguments f : {a1 := 1 : Nat} {a2 : Type} {a3 := 4 : Nat} -> Nat -> Nat, in the call site, if we write

f {a3 := 10}

It will be desugared into

f {1} {_} {10}

That is, when we pass an explicit named argument, we assume that arguments that come before it, have been omitted.

Another example, If we have

f 7

Then, it desugars to

f {1} {_} {4} 7

[lukaszcz]

Would it be correct to think about optional arguments in the following way?

• An optional argument behaves as an implicit argument except that when it is omitted, the default value is inserted instead of a hole.

Yes, I think that's actually a better way to think about it. Then restrictions 1 and 2 are not needed because there is no ambiguity anymore. And for 3 the existing implicit syntax needs to be extended instead of creating a new syntax.

The only disadvantage is that the default values are not really a part of the type, but we're putting them in the type signature, because we have no better place for. Though maybe it makes sense to put them there, because the signature should provide info on how to call the function, including which values will be provided for omitted arguments. Strictly speaking, being implicit itself is something "on top" of the type system already.

About restriction 2. Is the behavour that you have in mind as follows? Given a function with named arguments f : {a1 := 1 : Nat} {a2 : Type} {a3 := 4 : Nat} -> Nat -> Nat, in the call site, if we write

f {a3 := 10}

It will be desugared into

f {1} {_} {10}

That is, when we pass an explicit named argument, we assume that arguments that come before it, have been omitted.

Another example, If we have

f 7

Then, it desugars to

f {1} {_} {4} 7

Named arguments are actually a separate issue from optional ones. When optional arguments are not implicit then there is an ambiguity between whether the function is partially applied or the default values should be substituted, e.g., should

go lst

desugar to

go [] 0 lst

or to the partial application (where the argument acc1 receives lst)

go lst

If all optional arguments are implicit, then it's not ambiguous.

As for named arguments, I think they are a useful syntactic convenience. They can but don't have to be implicit/optional. When they are specified in an application by naming them, it should be possible to specify them in any order, e.g.:

f {a3 := 10} {a1 := 0}

should desugar to

f {0} {_} {10}

In Haskell, the lack of named arguments is usually circumvented by declaring a separate record to capture all "named" arguments of a function if it needs many of them. This works less well with type dependencies, and in general is a bit less convenient than a proper named arguments syntax.

[lukaszcz]

Then to make named lambdas consistent we would need to write:

go{acc1 := []}{acc2 := 0}@\{
     []        := (acc1, acc2)
   | (x :: xs) := go {x :: acc1} {acc2 + 1} xs
  };

That's perhaps better, because it makes it clear that the acc1 and acc2 arguments don't need to be provided to the lambda.

[janmasrovira]

If all optional arguments are implicit, then it's not ambiguous.

Exactly, so only implicit arguments should be allowed to have default values.

As for named arguments, I think they are a useful syntactic convenience. They can but don't have to be implicit/optional. When they are specified in an application by naming them, it should be possible to specify them in any order

I am not sure about this. Since we already have Pi types (currently only over Type but in the future it may expand), the order of the arguments can matter, so I'd say it is better to force named arguments to be given in order.
Even if the types of the arguments don't have dependencies, I don't see a strong benefit to allow call sites to change the order. Maybe there is a benefit that I don't see?

[lukaszcz]

The order in which you provide the arguments doesn't matter as long as the compiler can unambiguously reshuffle them to their "proper" order before type-checking. The names enable this reshuffling.

The benefit is that you want to refer to a named argument by its name, and you don't want to remember or care about the order - that's why you named the argument in the first place. When you're using named arguments seriously, you'll have double-digit numbers of them for some functions, as you sometimes have double-digit numbers of fields in a record. If you have good error messages that clearly indicate the order, you can reduce the reordering pain, but why generate the pain if it's not necessary?

I see this as analogous to ordering the fields in a record. They do have an order (which is significant for type-checking with dependent records), but when you provide the field values by naming the fields you don't need to list them in their original order, which is often arbitrary (disregarding type-checking). I think few languages with records enforce the order of record fields. Because it's inconvenient.

[lukaszcz]

Exactly, so only implicit arguments should be allowed to have default values.

Yes, right. If you allow them to be explicit you would have to restore restriction 2 to resolve the ambiguity.

[janmasrovira]

We've discussed offline the idea of passing arguments in unordered groups.
A group of named arguments would be written in {} or () depending on the implicitness of the arguments. Implicit and explicit arguments cannot be mixed in the same group. Inside the delimiters, we would have a non-empty list of argName := expr items separated by ;, where the order of the items does not matter.

E.g. if we have the following definition (I omit the types because they are not relevant):

g : {a : _} -> {a' : _} -> (b : _) -> {c := _} -> _

It would be possible to write:

1. g {a' := 1; a := 2} to mean g {2} {1}
2. g {a' := 2} to mean g {_} {2}
3. g (b := 3) to mean g {_} {_} 3
4. g {a := 1} (b := 3) to mean g {1} {_} 3
5. and so on

Note that groups must still be ordred with respect to other regular arguments or other groups, so the following is not acceptable

g {a' := 1} {a := 2}