在类型安全向量上使用归纳定义的 Applicative 实例
making use of inductively defined Applicative instances on type safe vectors
我正在尝试写下 （有限维自由） 向量空间的 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)
| ^^^^^^^^^^^
我在 Haskell 中没有过多地使用依赖类型，但这应该是可能的。我设法得到了一些可以编译的东西，但我认为还有更好的方法...
诀窍是能够生成可以递归的东西，它携带足够的类型信息，而实际上不需要已经有 Vector。这允许我们将两个 Applicative 实例折叠成一个 Applicative 实例（不幸的是添加了一个约束，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，但我们只能有矩阵，其中维度是 "true" Natural，所以我们能做的最好的就是 forall (n :: Natural) . Finite n => Matrix a n n 事实证明我在这里错了，实际上可以做到
经过一些恐吓（以及在火车上几个小时）的证明，我想到了这个。
如果你把 Finiteness 的证明推迟到最后，你可以乘以任何东西......我们要写的条款是直截了当的。
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 的额外构造函数，具有 Rank 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 是一个 CPS'd vdiag。
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
我正在尝试写下 （有限维自由） 向量空间的 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)
| ^^^^^^^^^^^
我在 Haskell 中没有过多地使用依赖类型，但这应该是可能的。我设法得到了一些可以编译的东西，但我认为还有更好的方法...
诀窍是能够生成可以递归的东西，它携带足够的类型信息，而实际上不需要已经有 Vector。这允许我们将两个 Applicative 实例折叠成一个 Applicative 实例（不幸的是添加了一个约束，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，但我们只能有矩阵，其中维度是 "true" Natural，所以我们能做的最好的就是 forall (n :: Natural) . Finite n => Matrix a n n 事实证明我在这里错了，实际上可以做到
经过一些恐吓（以及在火车上几个小时）的证明，我想到了这个。
如果你把 Finiteness 的证明推迟到最后，你可以乘以任何东西......我们要写的条款是直截了当的。
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 的额外构造函数，具有 Rank 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 是一个 CPS'd vdiag。
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