为张量类型定义函子实例 (Idris)答案

【问题标题】：Defining Functor Instance for Tensor Type (Idris)为张量类型定义函子实例 (Idris)
【发布时间】：2016-05-21 20:50:41
【问题描述】：

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

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

如您所见，Tensor 类型由描述张量维度的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 使用的术语，因此非常感谢任何理解错误消息的帮助。

【问题讨论】：

标签： idris

【解决方案1】：

（注意：从 Idris 0.10 开始，instance 关键字已被弃用，应直接省略）。

任务是将函数应用于Scalar 构造函数中的所有元素，否则保持结构不变。因此，我们需要将Scalar 映射到Scalar 和Dimension 到Dimension，并且由于Dimension 包含递归出现的向量，我们应该使用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 是递归调用。

【讨论】：