Conversione di un numero naturale di livello di tipo in un numero regolare

Question

Sto cercando di ottenere il blocco dei numeri naturali di tipo livello con un semplice esempio di implementazione di un prodotto con punti. Io rappresento il prodotto scalare in questo modo:

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

Ora, posso creare un'istanza monoide (dove mappend è il prodotto scalare reale) per ogni singola dimensione del prodotto scalare in questo modo:

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 

ma voglio definire un'istanza molto più generale come questo:

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

non sono sicuro di come convertire il numero del tipo in un numero regolare che posso lavorare con dentro la MEMP funzione.

---

Edit: Sarebbe anche bello avere una funzione dotplength :: (DotP n) -> n che correva nel tempo O (1) da solo guardando in su che tipo è, piuttosto che dover attraversare l'intero elenco.

Answer 1

Per ottenere risultati Integer corrispondente al livello di tipo naturale n, è possibile utilizzare

fromSing (sing :: Sing n) :: Integer 

Dopo armeggiare intorno un po ', ho ottenuto questo per compilare:

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