如何约束依赖类型集合的入参与返回值类型匹配

你可以通过以下两种常用方案实现要求的类型约束：

方案1：使用携带元素类型信息的依赖列表（异构列表） #

你之前使用List (s ** Tensor s)失败的核心原因是：普通依赖对列表的类型仅能约束元素是Tensor，但不会记录每个位置Tensor的具体shape，因此无法约束输出列表与输入列表每个位置的类型一一对应。
你可以自定义一个将shape序列作为类型参数的依赖列表类型：

-- 定义携带shape序列信息的Tensor集合类型，类型参数ss是所有元素的shape列表
data TensorList : List (n ** Vect n Nat) -> Type where
  TNil : TensorList []
  TCons : Tensor s -> TensorList ss -> TensorList ((_ ** s) :: ss)

此时你要的函数类型可以直接定义为：

processTensorList : TensorList ss -> TensorList ss

该签名自动约束输入输出的ss完全一致，因此每个位置的Tensorshape完全匹配，符合你的要求。
示例调用：传入TCons (Tensor [2,3,4]) $ TCons (Tensor [2]) $ TCons (Tensor []) TNil时，返回值类型与输入完全对齐。

方案2：使用带约束的元组 #

如果要使用元组作为输入输出类型，你只需要额外定义一个「元组所有元素都是Tensor」的类型谓词，配合自动隐参数实现约束：

-- 递归将元组转换为类型列表，用于后续约束检查
TupleTypeList : Nat -> Type -> List Type
TupleTypeList Z _ = []
TupleTypeList (S k) (a, b) = a :: TupleTypeList k b
TupleTypeList (S Z) a = [a]

-- 定义元组所有元素都是Tensor的约束
AllTensorTuple : Nat -> Type -> Type
AllTensorTuple n t = All (\ty => Exists (\s => ty = Tensor s)) (TupleTypeList n t)

-- 最终函数签名：输入输出元组类型完全一致，且满足所有元素都是Tensor的约束
processTuple : {n : Nat} -> {t : Type} -> {auto prf : AllTensorTuple n t} -> t -> t

该方案可以直接匹配你的示例场景：传入(Tensor [2,3,4], Tensor [2], Tensor [])或(Tensor [3],)这类任意长度的Tensor元组时，编译器会自动构造约束证明，同时保证返回值与入参类型完全相同。

内容的提问来源于stack exchange，提问作者joel