约束依赖类型集合，使其在args和return之间匹配

Question

我想写一个函数，它接受一个依赖类型的集合(我不太在意是哪种类型)，并返回另一个相同类型的集合，但可能具有不同的值。元素的形式为

data Tensor : (Vect r Nat) -> Type where

例如，一个函数接受(Tensor [2, 3, 4], Tensor [2], Tensor [])或(Tensor [3],)并返回相同类型的值。

What I've try

• 使用依赖对:接受一个List (s ** Tensor s)。我不知道如何约束输出具有相同的类型。
• 使用元组，但我不确定如何将元素类型固定为Tensor

Answer 1

您可以编写一个由所有Tensors的完整形状索引的函数，而不仅仅是其中的任何一个。每个Tensor的形状是一个List Nat，所以它们的一个列表的形状是一个List (List Nat):

import Data.Vect 
data Tensor : (Vect r Nat) -> Type where
data Tensors : List (List Nat) -> Type where
Nil : Tensors []
Cons : Tensor (fromList ns) -> Tensors nss ->  Tensors (ns :: nss)

下面是一个保持形状的map函数的例子:

mapTensors 
: ({0 r : Nat} -> {0 ns : Vect r Nat} -> Tensor ns -> Tensor ns) -> 
Tensors nss -> Tensors nss
mapTensors f Nil = Nil
mapTensors f (Cons t ts) = Cons (f t) (mapTensors f ts)