Question about currying (was: RFC: change how named ...)

Stream: new members

[Tom]

I read @Kyle Miller's RFC here (https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/RFC.3A.20change.20how.20named.20arguments.20suppress.20explicit.20parameters/near/472600768), the associated GH issues and and the ensuing discussion).

While I am not the target audience, I have an observation/usability question. First, let me try and motivate:

I love the fact that the "signature" of the function is "carried over" after currying. This is an awesome feature with named parameters:

def simple (x : Nat) (y: Nat) : Nat := x + y
def simple_partial := simple (y := 10)
#eval simple_partial (x := 20)

and

#check simple_partial -- returns `simple_partial (x : Nat) : Nat`

This also works with e.g. structures where the type can be inferred during the initial call:

structure Point (α :Type) where
  x : α
  y : α
deriving Repr

def Point_partial := Point.mk (y:=10)
#eval Point_partial (x:=20)

However, it does not work with functions or structures where there are implicit/type parameters:

def f (x: α) (y: β) : α := x

e.g. unlike the above, the following is not valid:

def g := f (y:=1.0)

This also applies to e.g. generic types, such as Prod or Sigma, i.e. this doesn't work:

def Prod_partial := Prod.mk (snd := 10)

and the output of the partial application is not "super helpful". Specifically, it has lost the type name/information from the original function signature.

#check Prod.mk (snd := 10)        -- fun fst => (fst, 10) : ?m.2068 → ?m.2068 × Nat

How is this related to the RFC? Aside from the inconsistent behavior, part of the confusion seems to have been caused by the fact that users weren't sure what the remaining parameters were/should have been. If after the partial application of a named parameter the signature would more clearly indicate what the "remaining signature is" (including the original type params), perhaps it would also help user to self-diagnose.

I am sure someone will tell me why this is hard :smile:

[Kyle Miller]

This isn't related to the RFC beyond having to do with app elaboration, though it does touch on the same region of code.

You're talking about the "eta expansion" feature. Currently it only applies to explicit parameters — implicit parameters are always elaborated as fresh metavariables.

An expectation of implicit parameters is that they should be eagerly turned into fresh metavariables. If we were to make it so α were eta expanded as well, the type of f (y := 1.0) would be {α : Sort _} -> (x : α) -> α, against expectations. One could imagine that strict implicit arguments could be subject to eta expansion, so for example the resulting type could be {{α : Sort _}} -> (x : α) -> α.

Your example does surface an unfriendly error message with a bug though:

def f (x: α) (y: β) : α := x

example := f (y := Nat.zero)
/-
don't know how to synthesize implicit argument 'α'
  @f ?m.469 Nat _fvar.467 Nat.zero
-/

We shouldn't bee seeing _fvar.467. That indicates that the error didn't capture the correct local context. (Could you please report it?)

[Tom]

This isn't related to the RFC beyond having to do with app elaboration, though it does touch on the same region of code.

That was my understanding and also the reason why I posted here rather than under the RFC, because it seemed tangential.

An expectation of implicit parameters is that they should be eagerly turned into fresh metavariables. <snip>

Could you please clarify this paragraph? What "expectation" are you referring to mention here?
And why would {α : Sort _} -> (x : α) -> α be against expectations?

Also, is there a reason why Lean can't infer the type of g and have the partial application succeed?

Your example does surface an unfriendly error message with a bug though:

Sorry, I seem to keep breaking things! :laughing: I will file. However, what version of Lean did you try this with? I'm on 4.11 stable and I get a different error:

def f (x: α) (y: β) : α := x

example := f (y := Nat.zero)

/-
invalid occurrence of universe level 'u_1' at '_example', it does not occur at the declaration type,
nor it is explicit universe level provided by the user, occurring at expression
  f.{u_1, 1} x Nat.zero
at declaration body
  fun (x : ?m.48) => f x Nat.zero
-/

Maybe it's a regression?

[Kyle Miller]

I see, I'm on a more recent build that changes when universe level errors are reported. You should be able to reproduce it with

def f (x: α) (y: β) : α := x

example := f.{1,1} (y := Nat.zero)

[Kyle Miller]

Tom said:

What "expectation" are you referring to mention here?

The one where implicit arguments are eagerly inserted. The type of an elaborated term doesn't start with {...} -> unless you specifically ask for it (for example by using @).

[Tom]

I just pulled master and can confirm that

example := f (y := Nat.zero)  -- This error is the same as the one above
example := f.{1,1} (y := Nat.zero) -- This demonstrates the issue you mention

I will file. And TIL, you can explicitly provide universe levels!

[Tom]

https://github.com/leanprover/lean4/issues/5475

[Kyle Miller]

Thanks. I edited the issue (lean4#5475). The error is to do with the _fvar.467 in the error message. It doesn't have to do with universe levels — I included the .{1,1} so you could see the error on the older version of Lean.