Getting last element of general n-tuple possible?

Stream: new members

[Kaarel August Kurik]

Hi! I've been wondering whether it's possible to write a function that extracts the last element of a general n-tuple (the one with right-associative Prod, not the (Fin n -> a) stuff). First thing I tried was matching on the type constructor, but that doesn't seem to be possible.

I tried looking for prior discussion about this, but couldn't find any. I imagine you can run into the same problem in many different guises though.

[Niels Voss]

You could do it with typeclasses, like

set_option autoImplicit false
universe u v w
class HasLast (α : Type u) (γ : outParam (Type v)) where
  getLast : α → γ

instance (priority := low) (α : Type u) (β : Type v) : HasLast (α × β) β where
  getLast p := p.snd

instance (α : Type u) (β : Type v) (γ : Type w) [HasLast β γ] : HasLast (α × β) γ where
  getLast p := HasLast.getLast p.snd

#eval HasLast.getLast (3, 6, 5, 1, 8) -- 8
#eval HasLast.getLast ("asdf", Nat, 4.3, fun (_ : Unit) => (), false) -- false

But I don't think this is a very good solution. Can you explain what you are trying to accomplish?

[Eric Wieser]

Prod tuples aren't very well behaved, as it's ambiguous what their length is if you intend one of the elements of the tuple to itself be a Prod

[Kaarel August Kurik]

That's a neat solution!
The only pragmatic goal here was to implement generic indexing on n-tuples, so I figured getting the last element would be a good simplification to test that. Other than that, I was just curious about how Lean's features support (or don't) this sort of thing.

[Tomas Skrivan]

I wrote something about code like this, it might be of interest https://lecopivo.github.io/scientific-computing-lean/Miscellaneous/Typeclasses-as-Interfaces-and-Function-Overloading/#Scientific-Computing-in-Lean--Miscellaneous--Typeclasses-as-Interfaces-and-Function-Overloading

[Niels Voss]

The only pragmatic goal here was to implement generic indexing on n-tuples, so I figured getting the last element would be a good simplification to test that. Other than that, I was just curious about how Lean's features support (or don't) this sort of thing.

It's possible that getting the last element of a n-tuple is actually much harder than getting the ith element of an n-tuple. This is because getting the size of an n-tuple is hard. Consider the following:
(3, "asdf", true, 3.5)
Should this be interpreted as a member of Nat × String × Bool × Float or as a member of Nat × String × (Bool × Float)? Both of these types are exactly the same, since × by default associates to the right. And you can imagine defining a new type def T := Bool × Float or abbrev T := Bool × Float and asking whether getting the last element should "see through" T. So, no, getting the last element is not a simplification of getting the n-th element, it is actually more challenging.

If you wanted to get the ith element, it is probably possible with metaprogramming, I'm just not quite sure how. The reason that this is easier than getting the last element is that it is right associative, so you can just iterate Prod.snd a bunch of times possibly followed by Prod.fst, and you get the same result if you place parentheses on the right (like around Bool × Float).