4

在 Idris 中，Vect n a是一个数据类型，表示一个长度为 n 的向量，其中包含类型 a 的项。想象一下我有一个功能：

foo : Int -> Vect 4 Int
foo n = [n-1, n, n+1, n*4]

函数的主体并不重要，它可以是任何返回 4 个 Ints 的向量的东西。现在，我想将此函数与 concatMap 一起使用，如下所示：

bar : Vect n Int -> Vect (4*n) Int
bar vals = concatMap foo vals

Bar 是一个函数，它接受长度为 n 的 Int 向量并返回长度为 4*n 的向量。

concatMap 的类型签名是：

Prelude.Foldable.concatMap : Foldable t => Monoid m => (a -> m) -> t a -> m

因此，如果我尝试编译 bar，我会收到错误消息：

 When elaborating right hand side of bar:
     Can't resolve type class Monoid (Vect (plus n (plus n (plus n (plus n 0)))) Int)

这意味着 Vect n Int 不是幺半群的实例。为了使它成为一个幺半群的实例，我需要实现：

Prelude.Algebra.neutral : Monoid a => a

不幸的是，我不确定如何做到这一点。List实现了monoid，如下：

instance Monoid (List a) where
    neutral = []

但是，如果我尝试为 Vect n Int 实现带有中性 = [] 的幺半群，我会收到错误消息：

 When elaborating right hand side of Prelude.Algebra.Vect n Int instance of Prelude.Algebra.Monoid, method neutral:
 |   Can't unify
 |           Vect 0 Int
 |   with
 |           Vect n Int
 |   
 |   Specifically:
 |           Can't unify
 |                   0
 |           with
 |                   n

所以我想知道，我将如何为 Vect 实现幺半群？

4

1 回答 1

7

您不能实现一个幺半群，这样您就可以使用concatMap. 想想 的签名concatMap：

(Foldable t, Monoid m) => (a -> m) -> t a -> m

请注意，函数参数的返回类型和整个函数的返回类型m必须相同。Monoid(a -> m)但是，情况并非如此。Vect n a考虑表达式：

concatMap foo vals

这里foo将有一个类型，你想要a -> Vect 4 a的结果是类型，其中是原始向量的长度。但这不适合该类型，因为您的应用程序需要以下类型：concatMapVect (4*n) anconcatMapconcatMap

(Foldable t, Monoid m, Monoid m1) => (a -> m) -> t a -> m1

其中结果 monoid 和函数返回的值可以是不同的类型，而concatMap强制您使用相同的类型。

[a]并且Vect n a完全不同，因为类型中不[]包含长度，这允许您编写函数。事实上，这允许您为二元运算符创建一个实例和连接。concatMapMonoid[]

当您开始将长度附加到类型时，这种可能性就消失了，因为您不能再混合不同的长度，因此不会Vect n a形成用于连接的幺半群。连接运算符在一般情况下变为类型，特别是它的s 类型是，这明显不同于它的列表类型：。a -> b -> cVectVect n a -> Vect m a -> Vect (n+m) a[a] -> [a] ->[a]

这就是说，您报告的错误是由于在为value的Monoid类编写实例时必须是 type但是是 type 。Vect n aneutralVect n a[]Vect 0 a

但是，您可以为类型类创建不同的实例。如果此类向量的元素是幺半群，那么您可以创建此类向量的幺半群。MonoidVect n a

在这种情况下，他neutral的向量必须是长度n，并且您可以赋予其元素的唯一合理值是neutral元素的Monoid。基本上你希望neutralofVect n a是replicate n neutral。

的二元运算Monoid将是元素之间运算的逐元素应用。

所以实例看起来像：

instance Monoid a => Monoid (Vect n a) where
    neutral = replicate n neutral

instance Semigroup a => Semigroup (Vect n a) where
    Nil <+> Nil = Nil
    (x :: xs) <+> (y :: ys) = (x <+> y) :: (xs <+> ys)

不幸的是，我不是 Idris 用户/程序员，所以我无法准确告诉您如何正确编写此类代码。以上只是一个类似 Haskell 的伪代码，用于给出概念的概念。

于 2014-10-04T14:22:22.777 回答