<div dir="ltr">I noticed that the definitions of Vector and Tensor have a parallel structure.<br>Vector is an ornamentation of the Peano natural numbers, and Tensor is the<br>parallel construction with multiplication and the multiplicative identity,<br>except that the factors are stored in a list instead of directly multiplying, so<br>that the dependent typing can ensure that the number of elements in the tensor<br>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.)<br><br>```haskell<br><div>{-# LANGUAGE AllowAmbiguousTypes #-}</div><div>{-# LANGUAGE DataKinds #-}</div>{-# LANGUAGE GADTs #-}<br>{-# LANGUAGE PolyKinds #-}<br>{-# LANGUAGE RankNTypes #-}<br>{-# LANGUAGE ScopedTypeVariables #-}<br>{-# LANGUAGE TypeFamilies #-}<br>{-# LANGUAGE TypeOperators #-}<br><br>import GHC.TypeLits<br>import Data.Kind<br>import Numeric.Natural<br>import Data.Proxy<br><br>data Vector (n :: Nat) a where<br>  Nil  :: Vector 0 a<br>  Cons :: a -> Vector n a -> Vector (n + 1) a<br><br>data Tensor :: forall n. Vector n Nat -> Type -> Type where<br>    Scalar :: a -> Tensor Nil a<br>    Dimension :: Vector n (Tensor d a) -> Tensor (Cons n d) a<br>```<br><br>That made me wonder what the exponential version with functions would look like<br>and if that is a useful concept, too, or one that also exists in maths? As going<br>from Vector to Tensor isn't completely mechanical, I had trouble figuring out<br><div>myself how to go from Tensor to the next higher data structure.</div><div><br></div><div>Cheers,</div><div>Johannes<br></div></div>