How does optParam works?

Stream: lean4

[Esteban Martínez Vañó]

Hi everyone.

I thought that if I define something like:

def sum'' (x: ℕ := 1) (y: ℕ) : ℕ := x + y

Then, when I eval sum 3 I would get 4, but that's not what happens. I'm doing something wrong?

Is there a way to really have an optional parameter such that when not introduced it is automatically replaced by its default value?

Thanks in advance.

[Floris van Doorn]

Optional parameters are mostly useful if they're the last parameter. But you can also use them together with named arguments. These both work as you want them to work:

def sum (x: Nat := 1) (y: Nat) : Nat := x + y
#eval sum (y := 3) -- 4
def sum' (y: Nat) (x: Nat := 1) : Nat := x + y
#eval sum' 3 -- 4

[Esteban Martínez Vañó]

I see. Thanks!

[Kyle Miller]

I wouldn't mind seeing an RFC for "implicit optional parameters", like

def sum'' {x: ℕ := 1} (y: ℕ) : ℕ := x + y

There are some details to nail down, like for example what if x appears in the type of another argument. Would it try to be inferred by unification before the optional parameter is tried? Or would it simply mean "use this value unless it's given as a named argument"? I think the latter is easiest to implement and to reason about, but the former might be what some users would expect.

Similarly, there could be "implicit autoparameters" like {h : x = y := by rfl}. The same questions apply: should it immediately use by rfl for the value of h, or should it wait to see if h was solved for by unification?

[Tom]

I already ran into cases where that would be useful. Also - and perhaps this is not he same as saying by rfl in your example - it seems that you can't use function calls in the definitions of defaults, which would be useful, too.

[Kyle Miller]

I'm not sure what you mean about not being able to use functions in defaults, do you have an example?

[Yuri]

It seems that the following does not apply for structure .mk?

For instance, following from this example:

def sum' (y: Nat) (x: Nat := 1) : Nat := x + y
#eval sum' 3 -- 4

I would expect the following to work:

structure A where
  b : Nat
  a : String := "aDefault"

#eval A.mk 1

I get the following error:

type mismatch
  A.mk 1
has type
  String → A : Type
but is expected to have type
  A : Type

Due to that fact that A.mk is elaborated ignoring the defaults:

A.mk (b : Nat) (a : String) : A

On the other hand, it does work when using { b := 1 }, but not ⟨ 1 ⟩.

[Kyle Miller]

@Yuri de Wit That's a known issue, but surprisingly fixing it depends on fixing a kernel bug. Fixing it is in progress.

[Mario Carneiro]

@Kyle Miller What kernel bug?

[Kyle Miller]

@Mario Carneiro lean4#4824

[Mario Carneiro]

that's not a kernel bug

[Mario Carneiro]

the error message is correct, but confusing

[Mario Carneiro]

You can't make a nested inductive like that

[Mario Carneiro]

to fix it you would have to hide the optParam wrapper from the kernel

[Kyle Miller]

The bug is that the nested inductive processor isn't erasing the optParam, but the issue is that this erases them on the elaborator side too.

Is it not possible to translate the optParam?

[Kyle Miller]

Could you explain what's wrong with the inductive?

[Mario Carneiro]

no, part of nested inductive validation involves replacing all types involved in the cycle with type variables, and none will not have this type

[Mario Carneiro]

in general you can't use functions defined on Option at all

[Mario Carneiro]

this amounts to a kind of induction-recursion if you did allow it

[Mario Carneiro]

the only reason it's okay here is because you can defeq replace the types of the constructors with ones that pass the check

[Mario Carneiro]

but the kernel doesn't know how to find such a type

[Mario Carneiro]

in particular, the kernel takes care not to reduce the types of constructors at all, even though it does reduce the type of the inductive

[Mario Carneiro]

i.e. if you introduce an abbreviation for A -> B, it will work if you use it in the type of the inductive but not in the constructor

[Kyle Miller]

Ok, thanks, this is in line with my understanding. It's just not clear to me that it's not possible to fix this in some way so that the elaborator still sees an optparam. (So far it's seemed likely we'll sacrifice that though.)

[Mario Carneiro]

we can probably fix it with a kernel patch, but I'm not a big fan of those for obvious reasons

[Mario Carneiro]

The most sensible general technique I see here is the ability to post-facto change the type of a constant to something defeq

[Mario Carneiro]

but maybe only very special cases of that (like removing optParams) are surfaced in practice