How to access applied argument by parameter name?

Stream: new members

[Avi Craimer]

In Lean 4 if you have a function or data constructor with a bunch of arguments having already been applied, is there a way to get the arguments. Without pattern matching.
Here is an example of what I'd like to be able to do:

def f (a:Nat) (b:Nat) (c:Nat) (d:Nat) : Nat
:= -- ...some implementation...

 def withArgs := f 1 2 3 4
#eval withArgs.b   -- 2
#eval withArgs.c   -- 3

I know the dot notation only works for structures. But is there other syntax that allows on to get the value that has been previously applied to a function or constructor? I know you can use pattern matching to do this but it would often be convenient to just use the name of the argument.

[Tomas Skrivan]

I doubt that this is possible. How would you even do this with pattern matching? Don't you need f to be a constructor of an inductive type for pattern matching?

[Avi Craimer]

Ok, assume that f is an constructor for an inductive type. Is there a way to access the arguments?

[Tomas Skrivan]

I don't think so, that is what structures are for. They are an inductive data type with a single constructor with all these projections defined automatically.

[Avi Craimer]

So then is there a way to easy transform a constructed value of an inductive type into a structure so you can access the fields?

Also, related to this, when defining inductive type constructors I've have difficulty using pattern matching inside the constructor definition. I can't figure out the syntax for it. I guess that is really what is motivating the question.

But also it would be nice to avoid the repetitiveness of having to write out the same pattern matching over and over in each constructor.

[Tomas Skrivan]

Can you give an example of what are you trying to do?

[Tomas Skrivan]

Well you can bundle all the parameters of a constructor to a structure. Would that help?

[Tomas Skrivan]

The constructor would accept only the structure.

[Tomas Skrivan]

Ahh the example is the other question you asked, right?

[Avi Craimer]

Ok, here is an example which doesn't work. I want to get the last argument applied to C1 inside C2.

inductive Foo : Nat -> Type u :=
| C1 (a:Nat) (b:Nat) (c:Nat) (d:Nat) : Foo 0
| C2 (C1 _ _ _ d) : Foo d

[Avi Craimer]

Tomas Skrivan said:

Well you can bundle all the parameters of a constructor to a structure. Would that help?

Yes, that would help. How do you do that?

[Avi Craimer]

Tomas Skrivan said:

Ahh the example is the other question you asked, right?

It is one possible solution to the other question I asked. Although in that specific case I'd still prefer to do it with a local function definition so I can have a consistent interface between the different constructors of Morph and Constraint.

[Tomas Skrivan]

Not sure if I follow, is the type of C2 this Foo 0 -> Foo d(what ever d is`)?

[Tomas Skrivan]

What would C2 (C2 (C1 1 2 3 0)) be?

[Avi Craimer]

This example, is silly, but here the type of C2 would be (Foo n) -> Foo n. It's not valid because we haven't matched all the patterns for each constructor. This part of what I don't know how to do. Here d is the last argument to C1, which is of type Nat.

It isn't essential that d be used in the type of C2. It could be fed into a subsequent arguement. Here it is fed into a non-inductive function f, to produce a value of type Bar.

inductive Foo  :=
| C1 (a:Nat) (b:Nat) (c:Nat) (d:Nat) : Foo
| C2 (C1 _ _ _ d) (f d): Bar : Foo

Sorry if this doesn't make sense. I'm very new to Lean. I'm probably trying to impose patterns from other languages on it. If there is a more paradigmatic way to do it I'd be interested to learn what it is.

[Tomas Skrivan]

Still what is the type of C2 in this example, it is unclear to me?

[Avi Craimer]

I guess in the modified example, the type of C2 would be Foo -> Bar -> Foo.

[Tomas Skrivan]

I think it would be better to explain what are you trying to do and then we can figure out how to write it in Lean.

[Tomas Skrivan]

I guess in the modified example, the type of C2 would be Foo -> Bar -> Foo.

Than again, it is unclear what would C2 (C2 (C1 1 2 3 4) bar1) bar2) mean as the outer C2 is not getting result of C1 in its first argument thus you do not know what d is.

[Avi Craimer]

Tomas Skrivan said:

I think it would be better to explain what are you trying to do and then we can figure out how to write it in Lean.

I'm trying to write a constructor C that pattern matches on fields from other constructors and then uses those values to define subsequent fields and/or the type of C.

[Avi Craimer]

Tomas Skrivan said:

I guess in the modified example, the type of C2 would be Foo -> Bar -> Foo.

Than again, it is unclear what would C2 (C2 (C1 1 2 3 4) bar1) bar2) mean as the outer C2 is not getting result of C1 in its first argument thus you do not know what d is.

Right, so then you'd want do have a default case for what to do if you don't match C1.

[Tomas Skrivan]

I'm trying to write a constructor C that pattern matches on fields from other constructors and then uses those values to define subsequent fields and/or the type of C.

And you are trying to do this because you want to achieve what?

[Tomas Skrivan]

Something like this does not work for you?

structure Data where
  (a b c d : Nat)

inductive Foo : Nat → Type where
| C1 (data : Data) : Foo data.d
| C2 (foo : Foo n) : Foo n

[Mario Carneiro]

The short answer is that you can't do that, this is known as an inductive-inductive type and it goes beyond the axiomatic strength of lean. But I suspect, like Tomas Skrivan says, that this simply isn't the problem you actually want to solve (#xy) and a reformulation has a better chance of being solved

[Avi Craimer]

Mario Carneiro said:

The short answer is that you can't do that, this is known as an inductive-inductive type and it goes beyond the axiomatic strength of lean. But I suspect, like Tomas Skrivan says, that this simply isn't the problem you actually want to solve (#xy) and a reformulation has a better chance of being solved

Thank you this helps. So what I was trying to do isn't supported. I'll indeed need to find a work around. Are there any code examples for defining things like composition with equational constraints, e.g., for strict monoidal n-categories.

[Avi Craimer]

Tomas Skrivan said:

Something like this does not work for you?

structure Data where
  (a b c d : Nat)

inductive Foo : Nat → Type where
| C1 (data : Data) : Foo data.d
| C2 (foo : Foo n) : Foo n

I will have a think and see if can rework it into this pattern. One issue is that in my actual use case, the structure Data would contain components with types that are defined recursively.

[Mario Carneiro]

Could you give a MWE?

[Mario Carneiro]

I'm not even sure what you want the system to produce