Idris - 在 n 维向量上映射操作

Question

我在 Idris 中定义了 n 维向量，如下所示:

import Data.Vect

NDVect : (Num t) => (rank : Nat) -> (shape : Vect rank Nat) -> (t : Type) -> Type
NDVect Z     []      t = t
NDVect (S n) (x::xs) t = Vect x (NDVect n xs t)

然后我定义了以下函数，它将函数 f 映射到张量中的每个条目。

iterateT : (f : t -> t') -> (v : NDVect r s t) -> NDVect r s t'
iterateT {r = Z}   {s = []}    f v = f v
iterateT {r = S n} {s = x::xs} f v = map (iterateT f) v

但是当我尝试在以下函数中调用 iteratorT 时:

scale : Num t => (c : t) -> (v : NDVect rank shape t) -> NDVect rank shape t
scale c v = iterateT (*c) v

我收到以下错误消息，指出类型不匹配，这对我来说似乎很好

 When checking right hand side of scale with expected type
         NDVect rank shape t

 When checking argument v to function Main.iterateT:
         Type mismatch between
                 NDVect rank shape t (Type of v)
         and
                 NDVect r s t (Expected type)

         Specifically:
                 Type mismatch between
                         NDVect rank shape t
                 and
                         NDVect r s t             
         Specifically:
                 Type mismatch between
                         NDVect rank shape t
                 and
                         NDVect r s t

Answer 1

我也一直想知道如何在 Idris 中表达 n 维向量(即张量)。我尝试了问题中的类型定义，但遇到了各种问题，因此我将 NDVect 函数表示为数据类型:

data NDVect : (rank : Nat) -> (shape : Vect rank Nat) -> Type -> Type where
  NDVZ : (value : t) -> NDVect Z [] t
  NDV  : (values : Vect n (NDVect r s t)) -> NDVect (S r) (n::s) t

并实现 map 如下:

nmap : (t -> u) -> (NDVect r s t) -> NDVect r s u
nmap f (NDVZ value) = NDVZ (f value)
nmap f (NDV values) = NDV (map (nmap f) values)

以下内容现在可以使用:

*Main> NDVZ 5
NDVZ 5 : NDVect 0 [] Integer
*Main> nmap (+4) (NDVZ 5)
NDVZ 9 : NDVect 0 [] Integer
*Main> NDV [NDVZ 1, NDVZ 2, NDVZ 3]
NDV [NDVZ 1, NDVZ 2, NDVZ 3] : NDVect 1 [3] Integer
*Main> nmap (+4) (NDV [NDVZ 1, NDVZ 2, NDVZ 3])
NDV [NDVZ 5, NDVZ 6, NDVZ 7] : NDVect 1 [3] Integer

不幸的是，拥有所有类型构造函数会让事情变得有点难看。我很想知道是否有更干净的方法来解决这个问题。

编辑:

这是一个稍微短一些的类型签名，它没有显式编码类型中的张量等级:

data NDVect : (shape : List Nat) -> Type -> Type where
  NDVZ : (value : t) -> NDVect [] t
  NDV  : (values : Vect n (NDVect s t)) -> NDVect (n::s) t

nmap : (t -> u) -> (NDVect s t) -> NDVect s u
nmap f (NDVZ value) = NDVZ (f value)
nmap f (NDV values) = NDV (map (nmap f) values)