我如何为向量组合编写 Functor 和 Applicative？

如何解决我如何为向量组合编写 Functor 和 Applicative？

我正在尝试使用 IDRIS 了解有关依赖类型的更多信息。 我试图模拟的示例使用了 Vectors 的组合。 我了解 Vectors 的 Functor 和 Applicative 实现，但我正在努力为 Composition 实现它们。

data Vector : Nat -> Type -> Type where
    Nil : Vector Z a
    (::) : a -> Vector n a -> Vector (S n) a

Functor (Vector n) where
    map f [] = []
    map f (x::xs) = f x :: map f xs

Applicative (Vector n) where
    pure = replicate _
    fs <*> vs = zipWith apply fs vs

现在 Composition 和 Decomposition-Function 如下所示：

data (:++) : (b -> c) -> (a -> b) -> a -> Type where
    Comp : (f . g) x -> (f :++ g) x

unComp : (f :++ g) a -> (f . g) a
unComp (Comp a) = a

User with Vectors 它封装了一个 Vector of Vectors。 现在我需要一个用于组合 (Vector n) :++ (Vector n) 的 Applicative。 我什至无法让 Functor 工作，主要是想看看我做错了什么。我尝试了以下操作，并且由于已经为 Vectors 实现了 Functor，所以这会起作用

Functor ((Vector n) :++ (Vector n)) where
    map f (Comp [])        = Comp []
    map f (Comp (x::xs))   = Comp ((f x) :: (map f (Comp xs)))

但是编译器给出了一个错误信息：

When checking an application of constructor Main.:::
        Unifying a and Vector (S n) a would lead to infinite value

type a 和 Vector n a 的统一和元素不正是 (::) 的目的吗？ 我显然做错了什么，我无法让它发挥作用。我也有感觉它可能很容易解决，但经过数小时的阅读和尝试后，我仍然不明白。 如果有人能给我建议或向我解释 Functor 和 Applicative 实现的样子，我将不胜感激。

解决方法

更新：Idris 2 现在内置了这个。 Functor for Compose、Applicative for Compose

我认为您可以像使用 Haskell's Compose 一样实现 Functor 和 Applicative 的一般实例。

newtype Compose f g a = Compose { getCompose :: f (g a) }

instance (Functor f,Functor g) => Functor (Compose f g) where
    fmap f (Compose x) = Compose (fmap (fmap f) x)
    a <$ (Compose x) = Compose (fmap (a <$) x)

instance (Applicative f,Applicative g) => Applicative (Compose f g) where
    pure x = Compose (pure (pure x))
    Compose f <*> Compose x = Compose (liftA2 (<*>) f x)
    liftA2 f (Compose x) (Compose y) =
      Compose (liftA2 (liftA2 f) x y)

要回答您的具体问题（但不要这样做）：

Functor ((Vector n) :++ (Vector n)) where
    map f (Comp x) = Comp $ map (map f) x