タイプレベルの自然数を通常の数値に変換する

Question

ドットプロダクトを実装する簡単な例で、タイプレベルの自然数のハングアップを取得しようとしています。私はこのようなドット積を表す：

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

ここで、Iはモノイドインスタンスを作成することができる（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 

私はMEMP内で作業することができ、通常の数にタイプの番号を変換するかどうかはわかりません

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

：しかし、私はこのようなより多くの一般的なインスタンスを定義したいです関数。

---

編集：また、ちょうどそれがむしろリスト全体をトラバースするより、何であるかの種類検索することで、時間O（1）で実行した機能dotplength :: (DotP n) -> nを持ってクールになります。

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)