How to define a function that uses a list which product of numbers is the same as the amount of element in matrix in Haskell using GADTs?

Question

I have a matrix representation of

data ListN (dim :: Nat) a where
    Nil  :: ListN Zero a
    Cons :: a -> ListN n a -> ListN (Succ n) a
infixr 5 `Cons`

data Tensor (dims :: [Nat]) a where
    Dense :: (Product dims ~ n) => ListN n a -> Tensor dims a
    Sparse :: Tensor n a

where Product makes sure dims is equal with n when you take the product of all the elements of dims. Now I would like to have a creator function and a function that changes the dimensions of the tensor data type.

1. I would like to have one function that changes the dimensions of the matrix, but only if the product of a given [Nat] is equal to the dims of the matrix that has to be changed. I already thought of something like: reshape :: (Product lm ~ l, Product (ns :: [Nat]) ~ n, l ~ n ) => Tensor ns a -> lm -> Tensor lm a. But that doesn't type check.
2. I would also like to have a function that can create a Tensor when given a [Nat] but once again that list should have a product that is the same as the amount of elements of a given ListN n a. I thought of fromList :: (Product lm ~ l, Product (ns :: [Nat]) ~ n, l ~ n ) => ListN n a -> lm -> Tensor lm a. But that also doesn't type check.

Answer 1

I'm guessing the error you're encountering is the most obvious problem with those types - lm doesn't have kind Type, as is required by the kind of (->). This is easy to fix. Just remove it. It's a type that already appears in the signature in the place you actually need it. Type inference does all you need.

Filling in the standard stuff you left out:

{-# Language DataKinds, TypeFamilies, UndecidableInstances, StandaloneKindSignatures #-}

data Nat = Zero | Succ Nat

type Add :: Nat -> Nat -> Nat
type family Add m n where
    Add Zero n = n
    Add (Succ m) n = Succ (Add m n)

type Mult :: Nat -> Nat -> Nat
type family Mult m n where
    Mult Zero n = Zero
    Mult (Succ m) n = Add n (Mult m n)

type Product :: [Nat] -> Nat
type family Product xs where
    Product '[] = Succ Zero
    Product (x : xs) = Mult x (Product xs)

data ListN (dim :: Nat) a where
    Nil  :: ListN Zero a
    Cons :: a -> ListN n a -> ListN (Succ n) a
infixr 5 `Cons`

data Tensor (dims :: [Nat]) a where
    Dense :: (Product dims ~ n) => ListN n a -> Tensor dims a
    Sparse :: Tensor n a

Then these just work:

reshape :: (Product ns ~ Product lm) => Tensor ns a -> Tensor lm a
reshape (Dense l) = Dense l
reshape Sparse = Sparse

fromList :: (Product lm ~ n) => ListN n a -> Tensor lm a
fromList = Dense

Note that I simplified the constraints in each signature, too.

In reshape that was just to reduce redundancy. Matching on the Dense constructor brings the constraint into scope, which then is enough to allow it to synthesize the constraint it needs to package up in the new Dense constructor.

For fromList, I just simplified it down to the type of Dense. It is, after all, exactly the same function. (I can still see why you'd want to export it with a name that hides the internals though, so I understand why it might exist.)