将类型级别的自然数转换为常规数

Question

我试图通过一个简单的实现点积的例子来掌握类型级自然数的窍门。 我这样表示点积：

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也很好，只需查找它是什么类型，而不必遍历整个列表。

Answer 1

要得到类型级别自然n对应的Integer，可以使用

fromSing (sing :: Sing n) :: Integer

在摆弄了一会儿之后，我得到了这个编译：

{-# LANGUAGE DataKinds, KindSignatures, ScopedTypeVariables #-}
import Data.Monoid
import GHC.TypeLits
data DotP (n :: Nat) = DotP [Int]
    deriving Show
instance SingI n => Monoid (DotP n) where
    mempty = DotP $ replicate (fromInteger k) 0
      where k = fromSing (sing :: Sing n)
    mappend (DotP xs) (DotP ys) = DotP $ zipWith (*) xs ys
dotplength :: forall n. SingI n => DotP n -> Integer
dotplength _ = fromSing (sing :: Sing n)