Zulip Chat Archive

Stream: general

Topic: Eta expand implicit arguments


Jannis Limperg (May 21 2020 at 16:50):

Suppose I have an expression e with type ∀ (x : T) {y : U}, V. From this, I'm generating something of the form λ (x' : T'), e (f x'), which I'd like to have type ∀ (x' : T') {y : U}, V. However, when elaborating this generated expression, Lean eagerly creates a metavariable for {y : U}, so the actual type is ∀ (x' : T'), V[y/?m].

To avoid this, I thought I'd eta-expand the implicit argument, generating λ (x' : T') {y : U}, @e (f x') y. However, I can't find the incantation that gives me @e for an arbitrary e. (In the application, e is a local constant, if that helps.) Any pointers?

(Unrelated question but I'm hijacking my own thread: Can I match on a level in an expression pattern? `(eq.{%%u} ...) doesn't seem to be a valid pattern.)

Mario Carneiro (May 21 2020 at 16:57):

You can write @e if e is a local constant though

Reid Barton (May 21 2020 at 17:11):

You could also consider changing the type of e to ∀ (x : T) {{y : U}}, V

Jannis Limperg (May 21 2020 at 18:18):

Mario Carneiro said:

You can write @e if e is a local constant though

In surface Lean, yes, but how do I represent this as an expr? I tried variations of `(@%%e ...), but that doesn't seem to work. In general, what is the expr corresponding to @h if h is a local const?

Reid Barton said:

You could also consider changing the type of e to ∀ (x : T) {{y : U}}, V

Yeah, I thought about that as well. This would be a slightly confusing change for users, but if nothing else works, I'll take it.

Mario Carneiro (May 21 2020 at 18:19):

as an expr, you don't have to do anything because you can just call expr.app and so on, elaboration doesn't happen unless you tell it to

Mario Carneiro (May 21 2020 at 18:20):

You don't have to use `(%%e ...) to construct exprs, in fact I wouldn't recommend it because it's not very general

Mario Carneiro (May 21 2020 at 18:21):

but I would need to see more precisely what you are trying to do to give more targeted advice

Jannis Limperg (May 21 2020 at 19:13):

Mario Carneiro said:

as an expr, you don't have to do anything because you can just call expr.app and so on, elaboration doesn't happen unless you tell it to

Okay, that makes sense. I thought I'd tried that, but I'll have to go back and check what exactly went wrong. Anyway, thanks!

Gabriel Ebner (May 21 2020 at 19:18):

Pro-tip: expr has a function coercion, so you can write e (f (var 0)).

Jannis Limperg (May 21 2020 at 20:23):

That is equal parts beautiful and horrifying.

Jannis Limperg (May 21 2020 at 20:31):

Okay, here's why my code doesn't work: I'm constructing a pexpr as above, not an expr. So, the real question: Is there a way to apply a local const to an implicit argument in a pexpr?

Rob Lewis (May 21 2020 at 20:34):

Not sure I'm interpreting your question right, are you looking for docs#pexpr.mk_explicit ?

Jannis Limperg (May 21 2020 at 20:49):

Don't know -- is mk_explicit e the equivalent of surface @e?

Jannis Limperg (May 21 2020 at 20:52):

Yes it is! Awesome, thanks.


Last updated: Dec 20 2023 at 11:08 UTC