Zulip Chat Archive

Stream: new members

Topic: extending structures with implicit parameters


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

Kenny Lau (Feb 21 2020 at 20:02):

so make \a in foo explicit

Arjun Pitchanathan (Feb 21 2020 at 20:02):

So is it impossible to have it implicit?

Kevin Buzzard (Feb 21 2020 at 20:03):

How is Lean supposed to guess the implicit argument?

Arjun Pitchanathan (Feb 21 2020 at 20:04):

So is there any way to specify it explicitly?

Kevin Buzzard (Feb 21 2020 at 20:04):

Maybe make the \a in foo explicit?

Kenny Lau (Feb 21 2020 at 20:04):

lol

Kevin Buzzard (Feb 21 2020 at 20:04):

I don't know of any other way

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

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?

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.

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!

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

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

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!

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

Mario Carneiro (Feb 21 2020 at 22:15):

I notice you put a type ascription on b though

Arjun Pitchanathan (Feb 21 2020 at 22:16):

Ah, right

Arjun Pitchanathan (Feb 21 2020 at 22:16):

But it also seems to work without it

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

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!

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.

Reid Barton (Feb 22 2020 at 02:20):

(which is not true for a lemma)

Nicolò Cavalleri (May 23 2021 at 23:18):

Is there still no solution to this? I need to extend a structure by putting implicit parameters in spots that are filled by type class inference

Kevin Buzzard (May 24 2021 at 06:50):

If the type of a parameter is a class then surely it should be in square brackets at all times?

This is a weird thread, it's people complaining that they can't do things which I can't ever imagine one would need to do. Is this a big #xy issue?

Kevin Buzzard (May 24 2021 at 06:51):

Can you post an #mwe?


Last updated: Dec 20 2023 at 11:08 UTC