我试图通过一个实现点积的简单示例来掌握类型级自然数的窍门。我代表这样的点积:
data DotP (n::Nat) = DotP [Int]
deriving Show
现在,我可以为每个单独的点积大小创建一个幺半群实例(mappend
实际的点积在哪里),如下所示:
instance Monoid (DotP 0) where
mempty = DotP $ replicate 0 0
mappend (DotP xs) (DotP ys) = DotP $ zipWith (*) xs ys
instance Monoid (DotP 1) where
mempty = DotP $ replicate 1 0
mappend (DotP xs) (DotP ys) = DotP $ zipWith (*) xs ys
instance Monoid (DotP 2) where
mempty = DotP $ replicate 2 0
mappend (DotP xs) (DotP ys) = DotP $ zipWith (*) xs ys
但我想定义一个更通用的实例,如下所示:
instance Monoid (DotP n) where
mempty = DotP $ replicate n 0
mappend (DotP xs) (DotP ys) = DotP $ zipWith (*) xs ys
我不确定如何将类型的数字转换为可以在 mempty 函数中使用的常规数字。
编辑:拥有一个在 O(1) 时间内运行的函数也很酷dotplength :: (DotP n) -> n
,只需查找它是什么类型,而不必遍历整个列表。