如何制作Applicative的固定长度向量实例？

最近了解了推广，决定尝试写向量。

{-# 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 <*> b =
    case a of
      Construct f c ->
        case b of
          Construct x d -> Construct (f x) (c <*> d)
      Empty -> Empty
  pure x = _

我不知道该怎么做pure。我试过这个：

case n of
  Next _ -> Construct x (pure x)
  Zero -> Empty

but got Variable not in scope: n :: Nat第一行的错误和Couldn't match type n with 'Zero对于这个表达式的第三行。

所以，我使用了以下技巧。

class Applicative' n where
  ap' :: Vector n (t -> u) -> Vector n t -> Vector n u
  pure' :: t -> Vector n t
instance Applicative' n => Applicative' ('Next n) where
  ap' (Construct f a) (Construct x b) = Construct (f x) (ap' a b)
  pure' x = Construct x (pure' x)
instance Applicative' 'Zero where
  ap' Empty Empty = Empty
  pure' _ = Empty
instance Applicative' n => Applicative (Vector n) where
  (<*>) = ap'
  pure = pure'

它完成了工作，但并不漂亮。它引入了一个无用的类Applicative'。每次我想使用Applicative for Vector在任何函数中，我都必须提供额外的无用约束Applicative' n这实际上适用于任何n.

更好、更干净的方法是什么？

你可以直接做同样的事情：

instance Applicative (Vector Zero) where
  a <*> b = Empty
  pure x = Empty

instance Applicative (Vector n) => Applicative (Vector (Next n)) where
  a <*> b = 
    case a of
      Construct f c ->
        case b of
          Construct x d -> Construct (f x) (c <*> d)
  pure x = Construct x (pure x)

我可以推断：对于不同类型的类，代码应该是类型感知的。如果你有多个实例，不同的类型会得到不同的实现，这很容易解决。但是，如果您尝试使用单个非递归实例来实现，则运行时基本上没有有关类型的信息，并且始终相同的代码仍然需要决定要处理哪种类型。当您有输入参数时，您可以利用 GADT 来提供类型信息。但对于pure没有输入参数。所以你必须有一些背景Applicative实例。