相关疑难解决方法(0)

我最近学习了促销,并决定尝试写矢量.

{-# LANGUAGE DataKinds, GADTs, KindSignatures #-}
module Vector where
  data Nat = Next Nat | Zero
  data Vector :: Nat -> * -> * where
    Construct :: t -> Vector n t -> Vector ('Next n) t
    Empty :: Vector 'Zero t
  instance Functor (Vector n) where
    fmap f a =
      case a of
        Construct x b -> Construct (f x) (fmap f b)
        Empty -> Empty

到目前为止,一切正常.但是在尝试制作Vector实例时我遇到了一个问题Applicative.

instance Applicative (Vector n) where
  a <*> …