如何使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 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不是monoid的实例.为了使它成为monoid的一个实例,我需要实现:

Prelude.Algebra.neutral : Monoid a => a

不幸的是,我不知道该怎么做.List实现了monoid,如下所示:

instance Monoid (List a) where
    neutral = []

但是,如果我尝试使用中性= []为Vect n Int实现monoid,我收到错误:

 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实现monoid？

Answer 1

你不能实现一个monoid,这样你就可以使用写下该表达式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在一般情况下变为类型,特别是Vects 的类型Vect n a -> Vect m a -> Vect (n+m) a,这与列表的类型明显不同:[a] -> [a] ->[a].

这就是说,您报告的错误是由于当为Monoid类Vect n a的值编写实例时neutral必须是类型Vect n a但是[]类型Vect 0 a.

但是,您可以为类型类创建不同的实例.如果这样的矢量的元素是幺半群,那么你可以创建这种矢量的幺半群.MonoidVect 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的伪代码来概括这些概念.