静态已知大小的固定向量作为类型参数的编码

Question

我希望将静态已知的大小编码为任意类型的参数，然后对该类型的值进行内部操作，以便使用该参数对固定向量包中的向量进行操作。

但是，我不知道如何使用这个类型的参数将固定的向量约束为隐含的大小。

非常简单的例子：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Main where

import Data.Vector.Fixed (Arity)
import qualified Data.Vector.Fixed as VF
import Data.Vector.Fixed.Unboxed

newtype Result n = Result Int

compute :: Arity n => Maybe (Result n)
compute = fmap (Result . calc) res
  where
    res = VF.replicateM (Just 1) :: Maybe (Vec n Int)
    calc = VF.sum

unpack :: Arity n => Result n -> Int
unpack (Result x) = x 

comp1 :: Int
comp1 = maybe 0 unpack r 
  where
    r = compute :: Maybe (Result 1)

main :: IO ()
main = print comp1

给出以下错误：

src/Main.hs:18:11: error:
    • Could not deduce: Data.Vector.Fixed.Cont.Peano
                          (n2 GHC.TypeLits.+ 1)
                        ~
                        'Data.Vector.Fixed.Cont.S (Data.Vector.Fixed.Cont.Peano n2)
        arising from a use of ‘VF.replicateM’
      from the context: Arity n
        bound by the type signature for:
                   compute :: Arity n => Maybe (Result n)
        at src/Main.hs:15:1-38
    • In the expression: VF.replicateM (Just 1) :: Maybe (Vec n Int)
      In an equation for ‘res’:
          res = VF.replicateM (Just 1) :: Maybe (Vec n Int)
      In an equation for ‘compute’:
          compute
            = fmap (Result . calc) res
            where
                res = VF.replicateM (Just 1) :: Maybe (Vec n Int)
                calc = VF.sum

src/Main.hs:19:5: error:
    • Could not deduce (Data.Vector.Fixed.Cont.ArityPeano
                          (Data.Vector.Fixed.Cont.Peano n0),
                        GHC.TypeLits.KnownNat n0,
                        Data.Vector.Fixed.Cont.Peano (n0 GHC.TypeLits.+ 1)
                        ~
                        'Data.Vector.Fixed.Cont.S (Data.Vector.Fixed.Cont.Peano n0))
        arising from a use of ‘VF.sum’
      from the context: Arity n
        bound by the type signature for:
                   compute :: Arity n => Maybe (Result n)
        at src/Main.hs:15:1-38
      The type variable ‘n0’ is ambiguous
    • When instantiating ‘calc’, initially inferred to have
      this overly-general type:
        forall (v :: * -> *) a. (VF.Vector v a, Num a) => v a -> a
      NB: This instantiation can be caused by the monomorphism restriction.
      In an equation for ‘compute’:
          compute
            = fmap (Result . calc) res
            where
                res = VF.replicateM (Just 1) :: Maybe (Vec n Int)
                calc = VF.sum

我怀疑GHC没有看到n在Result n中和n在:: Maybe (Vec n Int)中有任何联系。

也许我做错了。

我真正拥有的是一个类型族，对于从1到N的每一个自然数，我需要，例如，声明每个类型为某个类的实例，并在该类方法中使用固定向量。因此，将自然数存储为类型参数，然后，在某些仅受该类型约束的函数中，提取该数字并使用它在固定向量上按此大小进行内部操作。

Answer 1

你快到了！在主体compute中，有一个对类型变量n的引用，但是要做到这一点，实际上需要一个扩展：ScopedTypeVariables。

{-# LANGUAGE ScopedTypeVariables #-}

           -- Must be explicitly bound...
compute :: forall n. Arity n => Maybe (Result n)
compute = fmap (Result . calc) res
  where
    res = VF.replicateM (Just 1) :: Maybe (Vec n Int)  -- ... so it can be referred to here
    calc = VF.sum