约束依赖类型的集合以匹配 args 和 return

【问题标题】：Constrain collection of dependent types to match between args and return约束依赖类型的集合以匹配 args 和 return
【发布时间】：2021-10-09 13:04:41
【问题描述】：

我想编写一个函数，它接收一个依赖类型的集合（我不太在意什么类型），并返回另一个相同类型但可能具有不同值的集合。元素的形式

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

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

我的尝试

使用依赖对：接受List (s ** Tensor s)。然后我不知道如何将输出限制为具有相同的类型。
使用元组，但我不确定如何将元素类型修复为Tensor

【问题讨论】：

标签： idris dependent-type

【解决方案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)

【讨论】：