Zulip Chat Archive

Stream: general

Topic: Eta expand implicit arguments


view this post on Zulip 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.)

view this post on Zulip Mario Carneiro (May 21 2020 at 16:57):

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

view this post on Zulip Reid Barton (May 21 2020 at 17:11):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip Gabriel Ebner (May 21 2020 at 19:18):

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

view this post on Zulip Jannis Limperg (May 21 2020 at 20:23):

That is equal parts beautiful and horrifying.

view this post on Zulip 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?

view this post on Zulip Rob Lewis (May 21 2020 at 20:34):

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

view this post on Zulip Jannis Limperg (May 21 2020 at 20:49):

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

view this post on Zulip Jannis Limperg (May 21 2020 at 20:52):

Yes it is! Awesome, thanks.


Last updated: May 12 2021 at 22:15 UTC