Converting a type level natural number into a regular number

Question

I'm trying to get the hang of type level natural numbers with a simple example of implementing a dot product. I represent the dot product like this:

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

Now, I can create a monoid instance (where mappend is the actual dot product) for each individual size of the dot product like this:

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

But I want to define a much more general instance like this:

instance Monoid (DotP n) where
    mempty                      = DotP $ replicate n 0
    mappend (DotP xs) (DotP ys) = DotP $ zipWith (*) xs ys

I'm not sure how to convert the type's number into a regular number that I can work with inside the mempty function.

---

Edit: It would also be cool to have a function dotplength :: (DotP n) -> n that ran in time O(1) by just looking up what type it is, rather than having to traverse the whole list.

Answer 1

To get the Integer corresponding to the type level natural n, you can use

fromSing (sing :: Sing n) :: Integer

After fiddling around a bit, I got this to compile:

{-# 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)