Tensor: Try to use function to compute function type

Stream: new members

[Richard L Ford]

I'm trying to formalize the concept of multidimensional tensors as function type from Fin n types to a target type. I'm using code like this:

def Tensor.{u} (s: Shape) (α: Type u) : Type u:=
  match s with
  | [] => α
  | t::[] => Fin t → α
  | t::ts => Fin t → Tensor ts α

I was expecting that when I used something like Tensor [2, 3] Nat, that it would be turned into
the equivalent of:

Fin 2 -> Fin 3 -> Nat

However, when I have a value t: Tensor [2, 3] Nat and try to do an application, Lean is not recognizing that t is a function type.

Is there a reason this is not working? Is there something different I could do to make it work?

[Yaël Dillies]

Can you include the definition of Shape?

[Richard L Ford]

Sorry,

def Shape := List Nat

[Eric Wieser]

We have a largely abandoned version of this at docs#Holor, which might provide some inspiration

[Eric Wieser]

Your example works for me:

def Shape := List Nat

def Tensor.{u} (s: Shape) (α: Type u) : Type u:=
  match s with
  | [] => α
  | t::[] => Fin t → α  -- you can remove this line
  | t::ts => Fin t → Tensor ts α

variable (t : Tensor [2, 3] Nat)

#check t 0 0

[Richard L Ford]

@Eric Wieser Thanks for the pointer. This looks very interesting. I've not heard of a holor before.

[Richard L Ford]

@Eric Wieser, yes. That example worked for me too. The context in which it does not work is when the shape is a variable. But I guess in that case you have to know that the shape is not empty in order to know that it is a function.

[Richard L Ford]

@Eric Wieser, why has the holor work been largely abandoned? Do you know of another formalization of tensors? I'm doing this work in the context of machine learning, Pytorch, and such.

[Eric Wieser]

I think the simple answer is that it is abandoned due to the lack of anyone interest in working on it.

[Eric Wieser]

A more speculative answer is that the definition is bad; it certainly diverges from the approach used for docs#Matrix

[Eric Wieser]

Notably: using an arbitrary type for indexing, not always Fin n. This lets you have matrices indexed by, say, days of the week, or named color channels, etc.

[Richard L Ford]

So with Matrix, what do people do if they want higher ranks? Do they use matrices as the element type of matrices?

[Kevin Buzzard]

AFAIK nobody really wanted this yet.

[Eric Wieser]

Yes, sorry to be unclear; if anything, my comment above was "your design looks much more similar to the way we designed docs#Matrix than to the way we designed docs#Holor" (and this is probably a good thing). I was certainly not saying "use docs#Matrix instead"!

[Richard L Ford]

@Eric Wieser, thanks for the additional comment. In machine learning, tensors up to rank 4 are common. These have integer shapes which was why I was using Fin n. But if we were to develop theories of higher rank tensors, it does seem it would make sense to use general types for subscripts, like docs#Matrix does, and then one could specialize it to integer indices if desired. I will do more studying about now Matrix works so I do not reinvent the wheel.