haskell - 如何使 Vect n Int 成为 Monoid 的实例

Question

在 idris ，Vect n a是一种数据类型，表示包含类型 a 的项的 n 长度向量。想象一下我有一个功能:

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

函数体并不重要，它可以是任何返回 4 个整数向量的东西。现在，我想将这个函数与 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实现了幺半群，如下:

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 实现幺半群？

Answer 1

你不能实现一个幺半群，这样你就可以使用 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 ，以及 concatMap 的结果你想要的是类型 Vect (4*n) a哪里 n是原始向量的长度。但这不适合 concatMap键入因为您有一个应用程序 concatMap这需要一个类型，如:

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

其中结果 monoid 和函数返回的值可以是不同的类型，而 concatMap强制您使用相同的类型。
[a]和 Vect n a完全不同，因为 []不包括类型中的长度，这允许你写一个 concatMap功能。事实上，这允许您制作 Monoid [] 的实例并连接为二元运算符。

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

这就是说，您报告的错误是由于为 Monoid 编写实例时造成的。 Vect n a类(class) neutral 的值必须是 Vect n a 类型但是 []类型为 Vect 0 a .

但是，您可以为 Monoid 创建不同的实例。类型类结束 Vect n a .
如果这样的向量的元素是幺半群，那么你可以创建这样的向量的幺半群。

在这种情况下，他 neutral向量的长度必须为 n ，您可以赋予其元素的唯一合理值是 neutral元素 Monoid .
基本上你想要 neutral的 Vect 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 的伪代码，用于给出概念的概念。