Optional implicit argument

Stream: lean4

[Tomas Skrivan]

I would like to have optional implicit argument i.e. define function like def foo {n := 1} := n. The only way to specify the argument would be with named argument assignment foo (n:=5).

For example I want to write funcitonboundingSphere which returns the smallest sphere(center and radius) bounding a set s

def boundingSphere (K) [NormedField K] {X} [AddCommGroup X] [NormedSpace K X] (s : Set X) : X×ℝ := ...

you can see that K has to be set as explicit argument here as it can't be inferred from other arguments.

I would really like to write boundingSphere s but right now I have to write boundingSphere K s.

My idea is to use the trick described in the notation over field thread. With that I would define the function as

def boundingSphere {K:=currentBaseRing%} [NormedField K] {X} [AddCommGroup X] [NormedSpace K X] (s : Set X) : X×ℝ := ...

where currentBaseRing% is a macro that identifies the current field/ring we are working with. This is very common scenario that I have one filed/ring parameter through out the whole file and it a chore to mention it all the time.

I guess this is feature request for Lean core, I would like opinion of others if this is a good idea or not.

[Richard Copley]

Why do I want that? I write lots of code polymorphics in the base field

I'm sure I'm just being dim, but what's the connection, explicitly? Can you spell it out?

[Tomas Skrivan]

Ahh sorry, Zulip failed me and the post disappeared while I was writing it. At first it looked like it didn't get posted but it did ... I need to finish the question :face_palm:

[Richard Copley]

It seems like you might have forgotten to ask a question. Or is this a feature request?

[Tomas Skrivan]

Ok I fixed the question now, and yes it is more of a RFC then a question

[Kyle Miller]

I've thought this would be a neat feature to have. I'd like it to support auto-params too (i.e., {K := by tactics...}).

[Kyle Miller]

Question about this RFC: when would the default values be inserted? Would it try to use unification first and only insert a default value later? Or would it not use unification and insert the default value immediately?

[Kyle Miller]

Would it be better to modify optParam and autoParam to have a Bool flag that indicates whether the explicit argument can be provided positionally? And to come up with a syntax using ( ... ) for this concept?

[Tomas Skrivan]

Kyle Miller said:

Question about this RFC: when would the default values be inserted? Would it try to use unification first and only insert a default value later? Or would it not use unification and insert the default value immediately?

Good question but I'm afraid that is above my pay grade :grinning_face_with_smiling_eyes: I was thinking about it only in the context specifying the base field/ring. In that case I would insert the default value immediately.

[Kyle Miller]

Here's a partially formed competing idea:

The named% term would tag a type with metadata to let the app elaborator know that this parameter must be passed using named arguments. You could write for example (x : named% _) or (x : named% Nat) or (x : named% _ := defVal), and these parameters will not be given any of the positional arguments. If the argument is not supplied and it has no default value, the elaborator raises an error that the argument is missing.

[Kyle Miller]

named% here is just a barely acceptable placeholder. Using explicit parameters means we can avoid questions about whether these are implicit arguments.

[Tomas Skrivan]

If you keep such argument implicit {x : _} and assuming such argument can't be inferred from other arguments or return type then calling such function will be only valid if you specify x with a named argument. I'm not completely convinced for the need of named% macro

[Kyle Miller]

The point is to be clear that it's not interacting with the metavariable-insertion feature of implicit arguments in any way. It's weird to say "this implicit argument must be passed explicitly" -- that means it's explicit, right?

[Tomas Skrivan]

Yes I agree that treating implicit arguments this way breaks the normal meaning of implicit arguments and relying on doc string explaining that is probably suboptimal.

[Tomas Skrivan]

Kyle Miller said:

The point is to be clear that it's not interacting with the metavariable-insertion feature of implicit arguments in any way.

I'm afraid I do not understand this part of Lean so I don't see the potential consequences.

[Kyle Miller]

I'm not sure there's anything particularly weird, other than some confusion (for the user) about whether the default arguments are applied now or later, and to what extent it's by unification or assignment.

Using {...} instead of (...) also means there's not a possibility for letting the user know that a particular argument is supposed to be supplied by name. I'm not sure there are many uses for required-named arguments that don't have default values however, though what does come to mind is an API that requires Bool flags to be passed by named argument, so that the API is free to reorder them as it wishes without breaking downstream code.

[Kyle Miller]

(There's also a feature that some languages have -- for example Common Lisp and Swift -- which is being able to specify the the external name of a named parameter, letting the internal name used in the function be different. This isn't very related, but maybe it's worth thinking about since it's in the general design space.)

[Tomas Skrivan]

Writing {x := ...} would mean that you should not provide the argument by name, it should be inferred automatically from the default value or maybe by unification in special cases.

[Kyle Miller]

Right, but I mean the (x : named% _) feature, with no defaults, which can't really be represented using {...} (in the sense that {...} gives a bad error message, "cannot synthesize placeholders")

[Tomas Skrivan]

Yes agreed! I got a bit confused as we started discussing multiple somewhat related things.

[Tomas Skrivan]

Would this be the use case for (x : named% _) ?

import Mathlib.Probability.Density
open MeasureTheory
variable {X : Type} [MeasurableSpace X] (ℙ : Measure X) (μ : Measure ℝ) (f : X → ℝ) (x : ℝ)

#check pdf f ℙ _ x
#check pdf f ℙ x -- error: application type mismatch
#check pdf f ℙ x (μ:=μ)

Right now you have to write down the underscore for the autoParam (μ : Measure E := by volume_tac). So with named% you could specify μ only by (μ:=...), is that the idea?

[Kyle Miller]

For a case study, Python has multiple kinds of parameters: positional only, keyword only, and ones that can be passed either positionally or by keyword (the default). Its syntax is def f(a,b,c,/,d,e,f,*,g,h) to get a,b,c being positional-only and g,h keyword-only. The syntax isn't relevant here, but they have PEPs supporting the use cases for these parameter types.

[Kyle Miller]

Right now you have to write down the underscore for the autoParam (μ : Measure E := by volume_tac). So with named% you could specify μ only by (μ:=...), is that the idea?

Yeah, that looks like a good use case for it.

[Kyle Miller]

(Your version with {μ : Measure E := by volume_tac} would work here too)

[Kyle Miller]

That's not the only use case though. I could imagine docs#Lean.Elab.Term.elabAppArgs using it for its last three Bool arguments, to require you to use named arguments for them, since it doesn't seem like good practice to depend on whatever order they're in.

[Kyle Miller]

Imagine the explicit argument gets a default value. For that to be effective, it would have to be moved after ellipsis, and that does not sound like a fun refactor.

[Tomas Skrivan]

Yeah I ran into this annoying issue multiple times already and I had to rearrange function arguments.

[Mario Carneiro]

I'm not sure I understand in what way named% differs from Tomas's proposal

[Kyle Miller]

Two ways:

1. It's clear it's meant to elaborate similar to an explicit argument because it uses (...).
2. It supports named-only arguments without default values. (It can give a better error message than "cannot synthesize placeholder".)

[Kyle Miller]

The first isn't a functional difference. Maybe {x := v} is completely self-explanatory, but at least for me I think I would wonder how exactly the default argument is passed in, like whether it does it immediately or it defers it until checking for unsynthesized placeholders.

[Mario Carneiro]

I don't think that's something most users will be wondering about. Elaboration order is an extremely niche aspect of lean

[Mario Carneiro]

I think the "surface reading" being sensible is more important

[Mario Carneiro]

but regarding elaboration order I would expect it to behave the same as implicit arguments currently do

[Mario Carneiro]

you can already specify the values of implicit arguments using named arguments, so it seems this question is already decided?

[Mario Carneiro]

The error message being bad is something that can be improved independently, even for unmarked implicits

[Kyle Miller]

Mario Carneiro said:

you can already specify the values of implicit arguments using named arguments, so it seems this question is already decided?

How so? Passing named arguments is a very different feature from default values for missing arguments.

[Kyle Miller]

The error message being bad is something that can be improved independently

Let's say we want to support named-only arguments. Would you suggest that error handling should detect that this argument can never be inferred, and from that explain that it must be supplied as a named argument? While that could work, I think it could be confusing to people trying to make sense of an API -- how can they tell whether the argument is supposed to be a named-only argument?

[Mario Carneiro]

I don't think that this needs to be something the function author needs to decide on behalf of clients

[Mario Carneiro]

if it's confusing to call this function with 5 bools in it, then let the client code use named arguments if it wants

[Mario Carneiro]

I think the error handling should always suggest using named arguments when an implicit argument fails to be inferred (whether or not it is impossible for it to ever be inferred)

[Tomas Skrivan]

Another reason why I want default arguments for implicit arguments is to do reductions in function return types.

Consider this function

def halve {n} (i : Fin n) : Fin (n/2) := ...

I would like to reduce n/2 as much as possible when you do the application.

I have a prototype of a tactic infer with which you can define the function as

def halve {n m} (i : Fin n) (hm : 2 * m = n := by infer) : Fin m := ...

the tactic figures out that m is meta variable and should be equal to n/2, it reduces n/2 and assigns the result to m. For i : Fin 10 calling halve i returns term of type Fin 5.

Ideally the argument hm is an implicit argument:

def halve {n m} {hm : 2 * m = n := by infer} (i : Fin n) : Fin m := ...

[James Gallicchio]

Kyle Miller said:

I'm not sure there are many uses for required-named arguments that don't have default values

this is a feature in ocaml that i genuinely miss in Lean.

one extra-- in OCaml there's syntax sugar for passing the same labeled argument around, so instead of writing f ~arg:arg you can just write f ~arg (where arg is a variable in the context with the right type). akin to the structure syntax allowing you to pass names directly. I'm not sure how this would be adapted to Lean.

[Eduardo Ochs]

What are the parsers that parse optParams?
I couldn't find mentions to optParams in the main manuals - are there any? - and I'm trying to read the sources to understand more about them...

As I already had the parsing diagrams below I tried to read the parsers starting from funBinder and typeAscription, but I couldn't find the code that parse the "(... := ...)"s in:

def f1 (a : Nat      ) (b : Nat     ) : Nat := a+b
def f2 (a : Nat := 20) (b : Nat := 3) : Nat := a+b
def f3 (a       := 20) (b       := 3) : Nat := a+b

[Eduardo Ochs]

sshot.png

[Eric Wieser]

Again, you can ask lean for the names of the parsers by using `(command| def f2 (a : Nat := 20) (b : Nat := 3) : Nat := a+b)

[Eduardo Ochs]

Oops, sorry - I forgot that! It's binderDefault...
Thanks!