dotParam

Stream: lean4

[Kyle Miller]

RFC: lean4#6489

This RFC is trying to address being able to write generic API that we can export into other namespaces and use via dot notation. There are a few solutions in the design space, and this RFC is suggesting a dotParam widget (like `optParam, etc.). Comments welcome!

[Edward van de Meent]

i seem to recall a similar RFC (lean4#5482) proposing to have this/similar behaviour linked to parameters named self... how does this compare?

[Kyle Miller]

The downside of self is that this puts pressure on libraries to name arguments self rather than a better-named argument. (That's the summary of the thread referenced by this comment.)

[Eric Wieser]

I worry this would interact badly with alias Foo.ofBar := Bar.toFoo, as here the argument marked as dotParam on the RHS should not necessarily be inherited by the LHS

[Eric Wieser]

Maybe this isn't prevalent enough to actually matter though

[Kyle Miller]

It'd be good to find a concrete example where this would be an issue. Note that the Batteries alias command does not create aliases in the export sense — it creates a new declaration. Possibly alias could be modified to have an option to strip dotParam before it makes such an "alias".

[Kyle Miller]

I also have another alternative design to this RFC than dotParam, but it's a bit more complicated, and it's not clear it's implementable within the current dot notation resolution framework.

The rule for resolving dot notation could be modified to the following: Suppose we have x.f with x : S. Resolve the name S.f to get the name N.g. Look for the first parameter of N.g whose type T is of the form N ... If N is a class and x is not an instance of N, then if T is of the form T .. A .. with A the first type argument, we look instead for an argument of type A.

[Kyle Miller]

Benefit: this seems to handle many practical uses of dotParam, without needing to write dotParam.

Drawback: it's less-flexible, and the rule is somewhat complicated to explain.

[Eric Wieser]

Would another option be @[dotParam param_name]?

[Kyle Miller]

A downside to a dotParam attribute is that you wouldn't be able to control dot notation with CoeFun. One of the use cases of the dotParam widget is that you can use dotParam in a CoeFun instance to specify which argument gets used.

[Eric Wieser]

(Apologies, I searched for @[ in the rfc, but missed the word "attribute")

[Eric Wieser]

Can you elaborate on how dotParam would be used with a CoeFun instance, with a code sample?

[Kyle Miller]

I was imagining something like

instance (priority := 100) hasCoeToFun : CoeFun F (fun _ ↦ ∀ a : dotParam α, β a) where
  coe := @DFunLike.coe _ _ β _

(or rather to put the dotParam into the type of DFunLike.coe, since coercions get unfolded)