---
title:        Dependently typed tensors
author:       [Stefano Gogioso, Ayberk Tosun]
date-started: 2025-02-19
---

Summary of my understanding of a discussion (2025-02-13) with Stefano Gogioso on
dependently typed tensors.

\begin{code}

{-# OPTIONS --safe --without-K #-}

open import UF.FunExt

module gist.DependentlyTypedTensors (fe : Fun-Ext) where

open import MLTT.Fin
open import MLTT.Spartan
open import UF.Base
open import UF.Equiv

\end{code}

We work in a module parameterized by a type `R`. This can be thought of as the
carrier of a ring, but we are not interested in the ring structure in this gist.

\begin{code}

module Tensor (R : 𝓀₀  Μ‡) where

\end{code}

A vector of length `n` over `R` is a function `Fin n β†’ R`

\begin{code}

 Vector : β„• β†’ 𝓀₀  Μ‡
 Vector n = Fin n β†’ R

\end{code}

An `m` by `n` matrix over `R` is a function `Fin m Γ— Fin n β†’ R`. It has `m`
rows and `n` columns.

\begin{code}

 Matrix : β„• β†’ β„• β†’ 𝓀₀  Μ‡
 Matrix m n = (Fin m Γ— Fin n) β†’ R

\end{code}

This readily generalizes to a rank-`r` tensor over `R`.

\begin{code}

 Rank-[_]-Tensor : (r : β„•) β†’ (Fin r β†’ β„•) β†’ 𝓀₀  Μ‡
 Rank-[_]-Tensor r d = ((i : Fin r) β†’ Fin (d i)) β†’ R

\end{code}

Vectors are just rank-1 tensors.

\begin{code}

 vector-is-rank-1-tensor : (n : β„•) β†’ Vector n ≃ Rank-[ 1 ]-Tensor (Ξ» _ β†’ n)
 vector-is-rank-1-tensor n = s , qinvs-are-equivs s (r , sec , ret)
  where
   s : Vector n β†’ Rank-[ 1 ]-Tensor (Ξ» _ β†’ n)
   s v i = v (i 𝟎)

   r : Rank-[ 1 ]-Tensor (Ξ» _ β†’ n) β†’ Vector n
   r Ο‘ i = Ο‘ (Ξ» _ β†’ i)

   sec : r ∘ s ∼ id
   sec = Ξ» _ β†’ refl

   ret : s ∘ r ∼ id
   ret Ο‘ = dfunext fe †
    where
     † : (i : Fin 1 β†’ Fin n) β†’ s (r Ο‘) i ＝ Ο‘ i
     † i = s (r Ο‘) i      ＝⟨ refl ⟩
           r Ο‘ (i 𝟎)      ＝⟨ refl ⟩
           Ο‘ (Ξ» _ β†’ i 𝟎)  ＝⟨ ‑    ⟩
           Ο‘ i            ∎
            where
             ‑ : Ο‘ (Ξ» _ β†’ i 𝟎) ＝ Ο‘ i
             ‑ = ap Ο‘ (dfunext fe Ξ» { 𝟎 β†’ refl })

\end{code}

Matrices are rank-2 tensors.

\begin{code}

 _by_ : {X : π“₯  Μ‡} β†’ X β†’ X β†’ Fin 2 β†’ X
 _by_ x y 𝟎 = x
 _by_ x y 𝟏 = y

 matrix-is-rank-2-tensor : (m n : β„•)
                         β†’ Matrix m n ≃ Rank-[ 2 ]-Tensor (m by n)
 matrix-is-rank-2-tensor m n = s , qinvs-are-equivs s (r , sec , ret)
  where
   s : Matrix m n β†’ Rank-[ 2 ]-Tensor (m by n)
   s Ο† Ξ½ = Ο† (Ξ½ 𝟎 , Ξ½ 𝟏)

   doubletonβ€² : Fin m β†’ Fin n β†’ (k : Fin 2) β†’ Fin ((m by n) k)
   doubletonβ€² i j 𝟎 = i
   doubletonβ€² i j 𝟏 = j

   r : Rank-[ 2 ]-Tensor (m by n) β†’ Matrix m n
   r Ο‘ (i , j) = Ο‘ (doubletonβ€² i j)

   sec : r ∘ s ∼ id
   sec = Ξ» _ β†’ refl

   ret : s ∘ r ∼ id
   ret Ο‘ = dfunext fe †
    where
     † : (s ∘ r) Ο‘ ∼ id Ο‘
     † Ξ½ = s (r Ο‘) Ξ½                    ＝⟨ refl ⟩
           r Ο‘ (Ξ½ 𝟎 , Ξ½ 𝟏)              ＝⟨ refl ⟩
           Ο‘ (doubletonβ€² (Ξ½ 𝟎) (Ξ½ 𝟏))   ＝⟨ ‑    ⟩
           Ο‘ Ξ½                          ∎
            where
             ΞΎ : doubletonβ€² (Ξ½ 𝟎) (Ξ½ 𝟏) ∼ Ξ½
             ξ 𝟎 = refl
             ξ 𝟏 = refl

             ‑ = ap Ο‘ (dfunext fe ΞΎ)

\end{code}

We now generalize tensors as to be able to consider arbitrary index types.
Previously, we had a function `d : Fin r β†’ β„•`, whose product
`Ξ  i : Fin r , Fin (d i)` gave us the _shape_ of the tensor in consideration.
We now work with a generalized shape function `S : I β†’ π“₯  Μ‡`.

\begin{code}

 Shape-[_]-Tensor : {I : 𝓀₀  Μ‡} β†’ (I β†’ 𝓀₀  Μ‡) β†’ 𝓀₀  Μ‡
 Shape-[_]-Tensor {I} S = ((i : I) β†’ S i) β†’ R

\end{code}

The previous notion of `Rank-[ r ]-Tensor d` can now be reconstructed as a
special case.

\begin{code}

 finite-shape : (r : β„•) (d : Fin r β†’ β„•)
              β†’ Rank-[ r ]-Tensor d ＝ Shape-[_]-Tensor (Fin ∘ d)
 finite-shape _ _ = refl

\end{code}