Could not deduce (Dim n0)-CodePudding

I want to build a Hilbert matrix using the linear package and convert it to a list of lists. While this seems an easy task the type level constraints come into my way:

import Linear
import Linear.V
import Data.Vector qualified as V

-- | Outer (tensor) product of two vectors
outerWith :: (Functor f, Functor g, Num a) => (a -> a -> a) -> f a -> g a -> f (g a)
{-# INLINABLE outerWith #-}
outerWith f a b = fmap (\x -> fmap (f x) b) a

hilbertV :: forall a n. (Fractional a, Dim n) => Integer -> V n (V n a)
hilbertV n =
  let v = V $ V.fromList $ fromIntegral <$> [1..n]
      w = V $ V.fromList $ fromIntegral <$> [0..n-1]
  in luInv $ outerWith ( ) w v

listsFromM :: V n (V n a) -> [[a]]
listsFromM m = vToList (vToList <$> m)

vToList :: V n a -> [a]
vToList = V.toList . toVector

hilbertL :: forall a. (Fractional a) => Integer -> [[a]]
hilbertL n = listsFromM (hilbertV n)

When doing this the following error arises in the last line hilbertL n = listsFromM (hilbertV n):

bench/Solve.hs:28:26: error:
    • Could not deduce (Dim n0) arising from a use of ‘hilbertV’
      from the context: Fractional a
        bound by the type signature for:
                   hilbertL :: forall a. Fractional a => Integer -> [[a]]
        at bench/Solve.hs:27:1-56
      The type variable ‘n0’ is ambiguous
      These potential instances exist:
        three instances involving out-of-scope types
          instance GHC.TypeNats.KnownNat n => Dim n -- Defined in ‘Linear.V’
          instance Data.Reflection.Reifies s Int =>
                   Dim (Linear.V.ReifiedDim s)
            -- Defined in ‘Linear.V’
          instance forall k (n :: k) a. Dim n => Dim (V n a)
            -- Defined in ‘Linear.V’
    • In the first argument of ‘listsFromM’, namely ‘(hilbertV n)’
      In the expression: listsFromM (hilbertV n)
      In an equation for ‘hilbertL’: hilbertL n = listsFromM (hilbertV n)

How can i get this to compile?

CodePudding user response：

First, the type of HilbertV is unsafe. You shouldn't pass in an Integer size if size should be determined from the type! I think you want this:

{-# LANGUAGE TypeApplications, UnicodeSyntax #-}

hilbertV :: ∀ a n. (Fractional a, Dim n) => V n (V n a)
hilbertV = luInv $ outerWith ( ) w v
 where v = V $ V.fromList $ fromIntegral <$> [1..n]
       w = V $ V.fromList $ fromIntegral <$> [0..n-1]
       n = reflectDim @n []

(The [] just fills the proxy argument with the most concise way to generate a value-less functor input, since it is easier to pass in the type information with -XTypeApplications.)

In fact, I'd avoid even passing around n twice at all. Instead, why not factor out the marginal generation:

hilbertV :: ∀ a n. (Fractional a, Dim n) => V n (V n a)
hilbertV = luInv $ outerWith ( ) w v
 where v = fromIntegral <$> enumFinFrom 1
       w = fromIntegral <$> enumFinFrom 0

enumFinFrom :: ∀ n a . (Enum a, Dim n) => a -> V n a
enumFinFrom ini = V . V.fromList $ take (reflectDim @n []) [ini..]

Now, for hilbertL the problem is that you have a dependent type size. The trick to deal with that are Rank2-quantified functions; linear offers reifyDim/reifyVector etc. for the purpose.

hilbertL :: ∀ a . Fractional a => Int -> [[a]]
hilbertL n = reifyDim n hilbertL'
 where hilbertL' :: ∀ n p . Dim n => p n -> [[a]]
       hilbertL' _ = listsFromM $ hilbertV @n

Alternatively, you could also change hilbertV to take a proxy argument for the size and then just hand that in. I've always found this a bit ugly, but it's actually more compact in this case:

hilbertV :: ∀ a n p . (Fractional a, Dim n) => p n -> V n (V n a)
hilbertV np = luInv $ outerWith ( ) w v
 where v = V $ V.fromList $ fromIntegral <$> [1..n]
       w = V $ V.fromList $ fromIntegral <$> [0..n-1]
       n = reflectDim np

hilbertL :: ∀ a . Fractional a => Int -> [[a]]
hilbertL n = reifyDim n (\np -> listsFromM $ hilbertV np)