在 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 实现幺半群?
最佳答案
你不能实现一个幺半群,这样你就可以使用 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 的伪代码,用于给出概念的概念。
关于haskell - 如何使 Vect n Int 成为 Monoid 的实例,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/26193400/