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

Question

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

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

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

我试过的

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

标签： idrisdependent-type

Answer 1

您可以编写一个由所有 s 的完整形状索引的函数Tensor，而不仅仅是其中的任何一个。每个的形状Tensor是 a List Nat，所以它们列表的形状是 a 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)