我试图写下Category（有限维自由）向量空间，但我似乎无法说服 GHC 任何给定长度的索引向量都是Applicative.
这就是我所拥有的：
{-# LANGUAGE DataKinds, PolyKinds, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, FlexibleContexts, GADTs, DeriveTraversable, StandaloneDeriving #-}
-- | Quick(slow) and dirty typesafe vectors
module Vector where
import Control.Category
向量是带有长度参数的列表
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)
要获得类别，我们需要矩阵乘法。明显的实现使索引与我们通常想要的有点倒退。
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
编辑
在@Probie 的帮助下，我设法解决了前面的问题，这足以为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)
但是我在定义时遇到了与以前类似的问题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)))
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
似乎没有办法为此需要一个附带条件。
结束编辑
对于上下文，这是我以前的，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)
| ^^^^^^^^^^^