idris - 定义张量类型的仿函数实例 (Idris)

Question

我最近一直在学习 Idris，并决定尝试编写一个简单的张量库。我首先定义类型。

data Tensor : Vect n Nat -> Type -> Type
  Scalar : a -> Tensor [] a
  Dimension : Vect n (Tensor d a) -> Tensor (n::d) a

如您所见，类型 Tensor 由描述张量维度的 Nat 的 Vect 和一个类型来参数化，描述它的内容。到目前为止，一切都很好。接下来，我决定尝试使 Tensor 类型为 Functor。

instance Functor (Tensor d) where
  map f (Scalar x)    = f x
  map f (Dimension x) = map f x

idris 给了我以下错误。

Unifying `b` and `Tensor [] b` would lead to infinite type

好的。从错误中，我认为问题可能是 map 的第一个模式过于具体(即，当 map 的类型声明接受任何张量时，仅接受标量)。这看起来很奇怪，但我想我应该尝试使用 with 语句重写它。

dimensions : {d : Vect n Nat} -> Tensor d a -> Vect n Nat
dimensions {d} _ = d

instance Functor (Tensor d) where
  map f t with (dimensions t)
    map f (Scalar x)    | []     = f x
    map f (Dimension x) | (_::_) = map f x

但是我遇到了同样的错误。我在 Haskell 方面有相当多的经验，但我仍然不太习惯一般依赖类型编程中使用的术语，特别是 Idris 所使用的术语，因此任何帮助理解错误消息的帮助将不胜感激。

Answer 1

(注意:从 Idris 0.10 开始，instance 关键字已弃用，应简单地忽略)。

任务是将函数应用于Scalar 构造函数中的所有元素，但在其他方面保持结构不变。因此，我们需要将 Scalar 映射到 Scalar，将 Dimension 映射到 Dimension，并且由于 Dimension code> 包含递归出现的向量，我们应该使用 Vect 的 map 来访问它们。

Functor (Tensor d) where
  map f (Scalar x)     = Scalar (f x)
  map f (Dimension xs) = Dimension (map (map f) xs)

因此，在 map (map f) xs 中，第一个 map 用于映射 Vect，而 map f 是递归调用。