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

Question

我最近了解了促销，并决定尝试编写向量。

{-# 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

但得到 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对于 Vector在任何函数中，我都必须提供额外的无用约束 Applicative' n这实际上适用于任何 n .

有什么更好、更清洁的方法来做到这一点？

Answer 1

你可以直接做同样的:

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 的上下文。实例。