Vector is to Tensor as Tensor is to ...

Tequilensor.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}

import Data.Functor.Identity
import Data.Kind
import GHC.TypeLits
import Numeric.Fin -- from https://github.com/ekmett/numeric-fin/

type Vector (n :: Nat) = (->) (Fin n)

type Tensor (ns :: [Nat]) = (->) (Rec Fin ns)

type Tequilensor (ns :: [[Nat]]) a = Rec (Rec Fin) ns -> a

type Fun = (->)

type Funs ns = (->) (Rec Identity ns)

data Rec (f :: i -> Type) (xs :: [i]) where
   Nil :: Rec f '[]
   Cons :: f a -> Rec f as -> Rec f (a ': as)

xs :: Vector 2 Int
xs FZ = 11
xs (FS FZ) = 22

ys :: Tensor [2,3] Int
ys (Cons FZ (Cons FZ Nil)) = 11  -- [0,0]
ys (Cons FZ (Cons (FS FZ) Nil)) = 22  -- [0,1]
ys (Cons FZ (Cons (FS (FS FZ)) Nil)) = 33  -- [0,2]
ys (Cons (FS FZ) (Cons (FS (FS (FS FZ))) Nil)) = 44  -- [1,0]
ys (Cons (FS FZ) (Cons (FS (FS (FS (FS FZ)))) Nil)) = 55  -- [1,1]
ys (Cons (FS FZ) (Cons (FS (FS (FS (FS (FS FZ))))) Nil)) = 66  -- [1,2]

zs :: Tequilensor [[2,3],[1,2]] Int
zs (Cons (Cons FZ (Cons FZ Nil)) (Cons (Cons FZ (Cons FZ Nil)) Nil)) = 11
-- etc.