如何制作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该表达式的第三行有错误.

所以,我使用了以下hack.

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实例提供一些上下文.