Konwertowanie liczby naturalnej na typ typu na zwykły numer

Question

Próbuję uzyskać liczbę naturalną na poziomie typu z prostym przykładem implementacji produktu dot. I reprezentuje iloczyn skalarny tak:

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

Teraz można utworzyć monoid wystąpienie (gdzie mappend jest rzeczywisty produkt kropka) dla każdej wielkości iloczynu skalarnego jak poniżej:

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 

ale chcę, aby zdefiniować wiele bardziej ogólny przypadek tak:

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

nie jestem pewien, w jaki sposób przekonwertować liczbę typu jest na szereg regularnych, że mogę pracować z wewnątrz memp funkcja ty.

---

Edit: Byłoby też fajnie mieć funkcję dotplength :: (DotP n) -> n który biegł w czasie O (1), po prostu patrząc na jej typ, zamiast przechodzić przez całą listę.

Answer 1

Aby uzyskać Integer odpowiadającą poziomowi typu naturalne n, można użyć

fromSing (sing :: Sing n) :: Integer 

Po błahy wokół trochę, mam to skompilować:

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