我试图通过一个实现点积的简单示例来掌握类型级自然数的窍门。我这样表示点积:
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) 时间内运行,只需查找它是什么类型,而不是必须遍历整个列表。
最佳答案
要获取类型级别自然n
对应的Integer
,可以使用
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)
关于haskell - 将类型级别自然数转换为常规数,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/12924782/