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

Question

我试图通过一个实现点积的简单例子来获得类型级自然数的悬念.我代表这样的点积:

data DotP (n::Nat) = DotP [Int]
    deriving Show

现在,我可以mappend为点积的每个单独大小创建一个monoid实例(实际的点积),如下所示:

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函数中使用的常规数字.

---

编辑:dotplength :: (DotP n) -> n通过查找它的类型而不是必须遍历整个列表来拥有一个在时间O(1)中运行的函数也是很酷的.

Answer 1

要获得Integer对应的自然类型级别n,您可以使用

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)