I'm trying to write down the Category of (finite-dimensional free)vector spaces, but I can't seem to convince GHC that any given length indexed vector is Applicative.
here's what I have:
{-# LANGUAGE DataKinds, PolyKinds, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, FlexibleContexts, GADTs, DeriveTraversable, StandaloneDeriving #-}
-- | 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 the category, we need matrix multiplication. The obvious implementation makes the indices come out a little backwards from what we normally 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
with @Probie's help, I've managed to solve the earlier problem, which is sufficient 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 run 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)
Instead of needing to summon an Applicative (Vec n) from thin air, I now need a 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)))
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
There seems to be no way out of needing a side condition for this.
end edits
For context, This is what I had before, Vec n is inductively 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)
to get a category instance, we need to rearrange the a behind the indices...
data Matrix a i j where
Matrix :: Vec i (Vec j a) -> Matrix a i j
But there's no way to rearrange the indices themselves without rearranging one of the terms, too...
instance Num a => Category (Matrix a) where
Matrix x . Matrix y = Matrix $ (vmult (sequenceA x) y)
-- ^^^^^^^^^
However:
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)
| ^^^^^^^^^^^
