Tensor definition with arbitrarily nested Vects

Question

I'm trying to create a Tensor type, but I'm having trouble working with the type signature for the constructor. In this and this question, they define a Tensor as a Vect of Tensors, and in this question as a type alias for nested Vects, but neither is right for my purposes. I need a Tensor to be atomic (it's not made of other Tensors), and a distinct type (it doesn't inherit methods by virtue of being an alias).

I tried the following, which implicitly pulls out the shape and data type from an arbitrarily-nested Vect via array_type, and wraps it in a minimal Tensor type

import Data.Vect

total array_type: (shape: Vect r Nat) -> (dtype: Type) -> Type
array_type [] dtype = dtype
array_type (d :: ds) dtype = Vect d (array_type ds dtype)

data Tensor : (shape: Vect r Nat) -> (dtype: Type) -> Type where
  MkTensor : array_type shape dtype -> Tensor shape dtype

I've then defined various functions to check it's working at all (not included here). All this compiles fine, but when I try to define a function to multiply every element by two, I get in a real tangle. I've tried to first define it on a nested Vect:

times_two : Num dtype => array_type shape dtype -> array_type shape dtype
times_two (x :: xs) = (times_two x) :: (times_two xs)
times_two x = 2 * x

but I get

When checking left hand side of times_two:
When checking an application of Main.times_two:
Can't disambiguate since no name has a suitable type:
Prelude.List.::, Prelude.Stream.::, Data.Vect.::

Replacing :: with Data.Vect.:: didn't help. Is what I'm trying to do possible? and sensible?

HTNW HTNW · Accepted Answer · 2020-04-12T19:51:49

You can't match on array_type shape dtype since it is not a data type. You need to figure out (i.e. match on) what the shape is before that type will simplify to a data type.

times_two {shape = []} x = 2 * x
times_two {shape = n :: ns} xs = map times_two xs

(In this case, the match on xs is inside map.)

Tensor definition with arbitrarily nested Vects

1 Answers