Zulip Chat Archive

Stream: new members

Topic: extending structures with implicit parameters


view this post on Zulip Arjun Pitchanathan (Feb 21 2020 at 19:55):

How does one extend a structure that has implicit parameters? Consider

structure foo {α : Type} := (a : α)
structure bar {α : Type} extends foo :=
(b : α)

Lean apparently will not infer the parameter:

don't know how to synthesize placeholder
context:
α : Type
 Type

And neither are we able to specify it explicitly:

structure foo {α : Type} := (a : α)
structure bar {α : Type} extends @foo α :=
(b : α)

gives the error:

invalid 'structure', expression must be a 'parent' structure

I found this but there doesn't seem to be a resolution there

view this post on Zulip Kenny Lau (Feb 21 2020 at 20:02):

so make \a in foo explicit

view this post on Zulip Arjun Pitchanathan (Feb 21 2020 at 20:02):

So is it impossible to have it implicit?

view this post on Zulip Kevin Buzzard (Feb 21 2020 at 20:03):

How is Lean supposed to guess the implicit argument?

view this post on Zulip Arjun Pitchanathan (Feb 21 2020 at 20:04):

So is there any way to specify it explicitly?

view this post on Zulip Kevin Buzzard (Feb 21 2020 at 20:04):

Maybe make the \a in foo explicit?

view this post on Zulip Kenny Lau (Feb 21 2020 at 20:04):

lol

view this post on Zulip Kevin Buzzard (Feb 21 2020 at 20:04):

I don't know of any other way

view this post on Zulip Arjun Pitchanathan (Feb 21 2020 at 20:04):

As in, can I have it implicit in both foo and bar and specify it explicitly in the extends part, like I'm trying to do with the @foo

view this post on Zulip Kevin Buzzard (Feb 21 2020 at 20:05):

Right, I don't know how to make that work. You can see in the conversation you linked to that Chris fixed it by making the argument explicit. How can Lean guess the implicit argument? It might be foo nat or something, that would be a valid solution right?

view this post on Zulip Arjun Pitchanathan (Feb 21 2020 at 20:07):

True, I was hoping there would be a way to at least specify it ourselves -- seems there isn't. Thanks for your help.

view this post on Zulip Kevin Buzzard (Feb 21 2020 at 20:14):

Aah I see, yeah that makes sense. I don't know how to do it, perhaps some more CS person than me can suggest a fix. Nice question!

view this post on Zulip Mario Carneiro (Feb 21 2020 at 21:18):

I think it would make sense for the @foo α to work. That should be filed as a bug

view this post on Zulip Mario Carneiro (Feb 21 2020 at 21:20):

But as Kenny and Kevin say, I can't see any reason for foo as defined to make sense. Lean can never infer that argument so it should not be implicit

view this post on Zulip Arjun Pitchanathan (Feb 21 2020 at 22:10):

Okay, I just figured out that \a is always implicit infoo.mk, which was what I was really trying to do. I now realize that Kevin was probably asking how lean could infer \a in a general context when one uses foo rather than in my snippet, after extends. It makes sense to me now, thanks!

view this post on Zulip Arjun Pitchanathan (Feb 21 2020 at 22:13):

Also, here is one possible example where lean can infer the argument

inductive option {α : Type} : Type
| none {} : option
| some (a : α) : option
def has_val {α : Type} (a : α) : option  Prop
| option.none := false
| (option.some (b : α)) := a = b

view this post on Zulip Mario Carneiro (Feb 21 2020 at 22:15):

I notice you put a type ascription on b though

view this post on Zulip Arjun Pitchanathan (Feb 21 2020 at 22:16):

Ah, right

view this post on Zulip Arjun Pitchanathan (Feb 21 2020 at 22:16):

But it also seems to work without it

view this post on Zulip Mario Carneiro (Feb 21 2020 at 22:20):

I guess this is an instance of the fact that lean can infer the argument to foo in F in the following pattern:

variable (foo :  {α : Type}, Type)
variable (bar : Type  Type)
variable (f :  {α}, @foo α  bar α)

#check λ (F : foo) (b : bar ), f F = b

In your case, f is foo.rec

view this post on Zulip Arjun Pitchanathan (Feb 21 2020 at 23:16):

Yes, I guess it should work for basically any expression that forces the types to be equal

variable (foo :  {α : Type}, Type)
variable (bar : Type  Type)
variable (r :  {α β}, @foo α  bar α  β)
#check λ (F : foo) (b : bar ), r F b

Thanks a lot!

view this post on Zulip Reid Barton (Feb 22 2020 at 02:20):

This has_val example also only works because it is a def and the body of a def is taken into account when checking the type.

view this post on Zulip Reid Barton (Feb 22 2020 at 02:20):

(which is not true for a lemma)


Last updated: May 13 2021 at 18:26 UTC