Início / user-12288245

Lemma's questions

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

Estou tentando escrever uma função que pega uma instância de classe da minha classe personalizada VectorSpace(que tem o formato class VectorSpace t (n :: Nat) a where) e executa eliminação gaussiana nela. Atualmente, a função se parece com isso:

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)

com as seguintes extensões de linguagem:

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

No entanto, estou recebendo o seguinte erro:

• 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)

Mas adicionar QuantifiedConstraintsleva ao seguinte aviso no forall m. KnownNat me forall n. KnownNat n:

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

e o seguinte erro em mLene 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)

Como posso resolver esse conflito de digitação?

haskell