7

内積を実装する簡単な例を使用して、型レベルの自然数のコツをつかもうとしています。私はこのように内積を表します：

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

これで、次のように、内積の個々のサイズごとにモノイド インスタンス (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

しかし、私は次のようなもっと一般的なインスタンスを定義したいと思います:

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) で実行される関数を持つこともクールです。

4

1 に答える 1

8

Integerタイプレベルの Natural に対応するを取得するには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)
于 2012-10-17T00:31:56.543 に答える