I am trying to write Categoryvector spaces (finite-dimensional free) but I cannot convince the GHC that any indexed length vector matters Applicative,
here's what i have:
{-
-- | Quick(slow) and dirty typesafe vectors
module Vector where
import Control.Category
Vectors are lists with a length parameter
data Natural = Z | S Natural
data Vec (n :: Natural) a where
VNil :: Vec Z a
VCons :: a -> Vec n a -> Vec (S n) a
deriving instance Functor (Vec n)
deriving instance Foldable (Vec n)
deriving instance Traversable (Vec n)
To get a category, we need matrix multiplication. The obvious implementation makes indexes a bit backward from what we usually want.
vmult :: Num a => Vec i (Vec k a) -> Vec j (Vec k a) -> Vec j (Vec i a)
-- ^ ^ ^ ^ ^ ^
vmult _ VNil = VNil
vmult xs (VCons y ys) = VCons (dotProduct y <$> xs) $ vmult xs ys
dotProduct :: Num a => Vec n a -> Vec n a -> a
dotProduct VNil VNil = 0
dotProduct (VCons x xs) (VCons y ys) = x * y + dotProduct xs ys
EDIT
using @Probie help , I was able to solve an earlier problem, which is enough to define an instance for Semigroupoids
data KNat n where
KZ :: KNat Z
KS :: Finite n => KNat n -> KNat (S n)
class Finite (a :: Natural) where toFNat :: proxy a -> KNat a
instance Finite Z where toFNat _ = KZ
instance Finite n => Finite (S n) where toFNat _= KS (toFNat (Proxy :: Proxy n))
instance Finite n => Applicative (Vec n) where
pure :: forall a. a -> Vec n a
pure x = go (toFNat (Proxy :: Proxy n))
where
go :: forall (m :: Natural). KNat m -> Vec m a
go KZ = VNil
go (KS n) = VCons x $ go n
(<*>) :: forall a b. Vec n (a -> b) -> Vec n a -> Vec n b
nfs <*> nxs = go (toFNat (Proxy :: Proxy n)) nfs nxs
where
go :: forall (m :: Natural). KNat m -> Vec m (a -> b) -> Vec m a -> Vec m b
go KZ VNil VNil = VNil
go (KS n) (VCons f fs) (VCons x xs) = VCons (f x) (go n fs xs)
data Matrix a i j where
Matrix :: (Finite i, Finite j) => Vec i (Vec j a) -> Matrix a i j
instance Num a => Semigroupoid (Matrix a) where
Matrix x `o` Matrix y = Matrix (vmult (sequenceA x) y)
but I ran into a similar problem as before when defining Category.id:
instance Num a => Category (Matrix a) where
(.) = o
id :: forall (n :: Natural). Matrix a n n
id = Matrix (go (toFNat (Proxy :: Proxy n)))
where
go :: forall (m :: Natural). (KNat m) -> Vec m (Vec m a)
go KZ = VNil
go (KS n) = VCons (VCons 1 (pure 0)) (VCons 0 <$> go n)
, Applicative (Vec n) , Finite n.
src/Vector.hs:59:8: error:
• Could not deduce (Finite n) arising from a use of ‘Matrix’
from the context: Num a
bound by the instance declaration at src/Vector.hs:56:10-37
Possible fix:
add (Finite n) to the context of
the type signature for:
Control.Category.id :: forall (n :: Natural). Matrix a n n
• In the expression: Matrix (go (toFNat (Proxy :: Proxy n)))
In an equation for ‘Control.Category.id’:
Control.Category.id
= Matrix (go (toFNat (Proxy :: Proxy n)))
where
go :: forall (m :: Natural). (KNat m) -> Vec m (Vec m a)
go KZ = VNil
go (KS n) = VCons (VCons 1 (pure 0)) (VCons 0 <$> go n)
In the instance declaration for ‘Category (Matrix a)’
|
59 | id = Matrix (go (toFNat (Proxy :: Proxy n)))
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
, .
end edits
. , , Vec n Applicative
instance Applicative (Vec Z) where
pure _ = VNil
_ <*> _ = VNil
instance Applicative (Vec n) => Applicative (Vec (S n)) where
pure a = VCons a $ pure a
VCons f fs <*> VCons x xs = VCons (f x) (fs <*> xs)
, a ...
data Matrix a i j where
Matrix :: Vec i (Vec j a) -> Matrix a i j
, ...
instance Num a => Category (Matrix a) where
Matrix x . Matrix y = Matrix $ (vmult (sequenceA x) y)
-- ^^^^^^^^^
:
src/Vector.hs:36:42: error:
• Could not deduce (Applicative (Vec c))
arising from a use of ‘sequenceA’
from the context: Num a
bound by the instance declaration at src/Vector.hs:35:10-37
• In the first argument of ‘vmult’, namely ‘(sequenceA x)’
In the second argument of ‘($)’, namely ‘(vmult (sequenceA x) y)’
In the expression: Matrix $ (vmult (sequenceA x) y)
|
36 | Matrix x . Matrix y = Matrix $ (vmult (sequenceA x) y)
| ^^^^^^^^^^^