小编Alm*_*ldo的帖子

我一直在玩矢量和矩阵,其中大小按其类型编码,使用新的DataKinds扩展名.它基本上是这样的:

data Nat = Zero | Succ Nat

data Vector :: Nat -> * -> * where
    VNil :: Vector Zero a
    VCons :: a -> Vector n a -> Vector (Succ n) a

现在我们想要像Functor和的典型实例Applicative.Functor简单:

instance Functor (Vector n) where
    fmap f VNil = VNil
    fmap f (VCons a v) = VCons (f a) (fmap f v)

但是对于Applicative实例存在一个问题:我们不知道纯粹返回什么类型.但是,我们可以根据向量的大小来定义实例:

instance Applicative (Vector Zero) where
    pure = const VNil
    VNil <*> VNil …