主页 / user-12288245

Lemma's questions

Martin Hope
Lemma
Asked: 2025-02-18 23:04:31 +0800 CST
  • 7

我正在尝试编写一个函数，该函数接受我的自定义类的类实例VectorSpace（其形式为class VectorSpace t (n :: Nat) a where）并对其执行高斯消元法。当前该函数如下所示：

rowEchelon
    :: ( forall m. KnownNat m
       , forall n. KnownNat n
       , Field a
       , VectorSpace t m a
       , VectorSpace t n a
       )
    => (forall k b. t k b -> Int -> b) -- ^ Indexing function
    -> t m (t n a)  -- ^ Matrix
    -> t m (t n a)  -- ^ Resultant row-echelon matrix
rowEchelon indexFunc = loop 0 0
  where
    loop h k matrix
        | h >= mLen || k >= nLen = matrix
        | otherwise = undefined

    mLen = natVal (Proxy :: Proxy m)
    nLen = natVal (Proxy :: Proxy n)

具有以下语言扩展：

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

但是，我收到以下错误：

• Illegal polymorphic type: forall (m1 :: Nat). KnownNat m1
  A constraint must be a monotype
• In the type signature:
    rowEchelon :: (forall m. KnownNat m,
                   forall n. KnownNat n,
                   Field a,
                   VectorSpace t m a,
                   VectorSpace t n a) =>
                  -- | Indexing function
                  (forall k b. t k b -> Int -> b)
                  -> -- | Matrix
                     t m (t n a)
                     -> -- | Resultant row-echelon matrix
                        t m (t n a)
• Perhaps you intended to use QuantifiedConstraints (typecheck)

但是添加QuantifiedConstraints会导致在forall m. KnownNat m和中出现以下警告forall n. KnownNat n：

This binding for ‘[m or n depending on the line]’ shadows the existing binding

mLen和上出现以下错误nLen：

• Couldn't match kind ‘*’ with ‘GHC.Num.Natural.Natural’
  When matching types
    proxy0 :: Nat -> *
    Proxy :: * -> *
  Expected: proxy0 [n1 or n2]
    Actual: Proxy n0
• In the first argument of ‘natVal’, namely ‘(Proxy :: Proxy [m or n])’
  In the expression: natVal (Proxy :: Proxy [m or n])
  In an equation for ‘nLen’: nLen = natVal (Proxy :: Proxy [m or n]) (typecheck -Wdeferred-type-errors)

我该如何解决这个打字冲突？

haskell