我试图写下(有限维自由)向量空间的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的帮助下，我设法解决了前面的问题，这足以为Semigroupoid定义一个实例
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)
| ^^^^^^^^^^^
我没有在Haskell 中过多地使用依赖类型，但这应该是可能的。我已经设法得到了一些可以编译的东西，但我认为有更好的方法......
诀窍是能够生成可以递归的东西，该内容携带足够的类型信息，而实际上不需要已经有Vector。这允许我们将两个应用程序实例折叠为单个应用程序实例(不幸的是，添加了一个约束，Finite希望以后不会引起问题)
{-# LANGUAGE DataKinds, PolyKinds, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, FlexibleContexts, GADTs, DeriveTraversable, StandaloneDeriving, ScopedTypeVariables #-}
module Vector where
import Control.Category
import Data.Proxy
data Natural = Z | S Natural
data SNat n where
SZ :: SNat Z
SS :: Finite n => SNat n -> SNat (S n)
class Finite (a :: Natural) where
toSNat :: proxy a -> SNat a
instance Finite Z where
toSNat _ = SZ
instance (Finite a) => Finite (S a) where
toSNat _ = SS (toSNat (Proxy :: Proxy a))
data Vec (n :: Natural) a where
VNil :: Vec Z a
VCons :: (Finite n) => a -> Vec n a -> Vec (S n) a
deriving instance Functor (Vec n)
deriving instance Foldable (Vec n)
deriving instance Traversable (Vec n)
instance (Finite n) => Applicative (Vec n) where
pure (a :: a) = go (toSNat (Proxy :: Proxy n))
where go :: forall (x :: Natural) . SNat x -> Vec x a
go SZ = VNil
go (SS m) = VCons a (go m)
(fv :: Vec n (a -> b)) <*> (xv :: Vec n a) = go (toSNat (Proxy :: Proxy n)) fv xv
where go :: forall (x :: Natural) . SNat x -> Vec x (a -> b) -> Vec x a -> Vec x b
go SZ VNil VNil = VNil
go (SS m) (VCons f fs) (VCons x xs) = VCons (f x) (go m fs xs)
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
data Matrix a i j where
Matrix :: (Finite i, Finite j) => 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)
编辑：Matrix不是一个类别。没有身份——我们需要forall (n :: Natural) . Matrix a n n
不幸的是，Haskell的所有种类都居住着Any，所以我们需要能够有一个Matrix a Any Any，但我们只能有维度为"真"Naturals的矩阵，所以我们能做的最好的事情就是forall (n :: Natural) . Finite n => Matrix a n n事实证明我错了，实际上可以做到
经过一些恐吓证明(以及在火车上几个小时)，我想出了这个。
如果你把Finite性证明推迟到最后，你可以乘以任何东西......我们要写的术语是海峡。
vdiag :: forall a i j. a -> a -> a -> KNat i -> KNat j -> Vec i (Vec j a)
vdiag u d l = go
where
go :: forall i' j'. KNat i' -> KNat j' -> Vec i' (Vec j' a)
go (KS i) (KS j) =
VCons (VCons d $ vpure u j)
(VCons l <$> go i j)
go KZ _ = VNil
go (KS i) KZ = vpure VNil (KS i)
vpure :: a -> KNat m -> Vec m a
vpure x KZ = VNil
vpure x (KS n) = VCons x $ vpure x n
但是我们不知道当我们实际需要将它们用于Category.id时，i和j会是什么(除了它们是相等的)。 我们CPS他们！ 给出了一个额外的构造函数来Matrix a，具有秩 2 约束。
data Matrix a i j where
DiagonalMatrix :: (Finite i => KNat i -> Vec i (Vec i a)) -> Matrix a i i
-- ^^^^^^^^^ ^
Matrix :: (Finite i, Finite j) => Vec i (Vec j a) -> Matrix a i j
每当我们碰巧需要将这样的事情相乘时，我们都可以使用我们知道内部索引的事实，即我们知道从另一个相乘的项中k：
instance Num a => Semigroupoid (Matrix a) where
o :: forall a i j k. Num a => Matrix a k j -> Matrix a i k -> Matrix a i j
Matrix x `o` Matrix y =
Matrix (vmult (sequenceA x ) y)
DiagonalMatrix fx `o` Matrix y =
Matrix (vmult (sequenceA (fx (toFNat (Proxy :: Proxy k)))) y)
Matrix x `o` DiagonalMatrix fy =
Matrix (vmult (sequenceA x ) (fy (toFNat (Proxy :: Proxy k))))
也就是说，除非它们都是对角线。 无论如何，它们都是相同的，因此我们现在可以使用稍后为所有三个获得的索引：
DiagonalMatrix fx `o` DiagonalMatrix fy = DiagonalMatrix $
i -> vmult (sequenceA (fx i)) (fy i)
正是由于这一步，有必要将 CPS 的Matrix限制为仅平方。 起初，我一直只尝试CPSing，但这需要最终用户记住所有中间索引并证明它们，而不仅仅是结果的索引。 虽然我确信这可以发挥作用，至少对于一个类别而言，这是不必要和严厉的。
无论如何，我们现在完成了，id是一个CPSvdiag.
instance Num a => Category (Matrix a) where
(.) = o
id = DiagonalMatrix $ i -> vdiag 0 1 0 i i
当然，从Matrix a中提取行和列需要您知道您要求的矩阵有多大。
unMatrix :: (Finite i, Finite j) => Matrix a i j -> Vec i (Vec j a)
unMatrix (Matrix x) = x
unMatrix (DiagonalMatrix fx) = fx (toFNat (Proxy))
type Zero = Z
type One = S Z
type Two = S One
type Three = S Two
type Four = S Three
f :: Vec Two (Vec Three Int)
f = VCons (VCons 1 $ VCons 2 $ VCons 3 VNil)
$ VCons (VCons 4 $ VCons 5 $ VCons 6 VNil)
$ VNil
g :: Vec Four (Vec Two Int)
g = VCons (VCons 1 $ VCons 2 VNil)
$ VCons (VCons 3 $ VCons 4 VNil)
$ VCons (VCons 5 $ VCons 6 VNil)
$ VCons (VCons 7 $ VCons 8 VNil)
$ VNil
fg = unMatrix $ Matrix f . id . Matrix g
-- ^^
但这并不算是太大的义务。
> fg
VCons (VCons 9 (VCons 12 (VCons 15 VNil))) (VCons (VCons 19 (VCons 26 (VCons 33 VNil))) (VCons (VCons 29 (VCons 40 (VCons 51 VNil))) (VCons (VCons 39 (VCons 54 (VCons 69 VNil))) VNil)))
为了完整起见，这是整个事情：https://gist.github.com/danbornside/f44907fe0afef17d5b1ce93dd36ce84d