[Haskell-cafe] What is the exponential version of dependently-typed Vector and Tensor?

15 Jul 2022

      I noticed that the definitions of Vector and Tensor have a parallel
structure.
Vector is an ornamentation of the Peano natural numbers, and Tensor is the
parallel construction with multiplication and the multiplicative identity,
except that the factors are stored in a list instead of directly
multiplying, so
that the dependent typing can ensure that the number of elements in the
tensor
is indeed equal to the product of these factors. (To make it more parallel,
the Nat in Vector could be replaced with a list of ones.)

```haskell
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

import GHC.TypeLits
import Data.Kind
import Numeric.Natural
import Data.Proxy

data Vector (n :: Nat) a where
  Nil  :: Vector 0 a
  Cons :: a -> Vector n a -> Vector (n + 1) a

data Tensor :: forall n. Vector n Nat -> Type -> Type where
    Scalar :: a -> Tensor Nil a
    Dimension :: Vector n (Tensor d a) -> Tensor (Cons n d) a
```

That made me wonder what the exponential version with functions would look
like
and if that is a useful concept, too, or one that also exists in maths? As
going
from Vector to Tensor isn't completely mechanical, I had trouble figuring
out
myself how to go from Tensor to the next higher data structure.

Cheers,
Johannes

[Haskell-cafe] What is the exponential version of dependently-typed Vector and Tensor?

Johannes Riecken