时间戳

首页 > 解决方案 > 如何为 Vector-Composition 编写 Functor 和 Applicative？

vector - 如何为 Vector-Composition 编写 Functor 和 Applicative？

问题描述

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

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

现在合成和分解函数看起来像这样：

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

使用向量的用户它封装了向量的向量。现在我需要一个 Applicative 的 Composition (Vector n) :++ (Vector n)。我什至无法让 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 实现的外观，我将不胜感激。

标签： vectorfunctoridrisdependent-typeapplicative

解决方案

更新：Idris 2 现在有这个内置的。Compose 的Functor , Compose的Applicative

我认为您可以使用HaskellFunctor的Compose实现一个通用实例。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

推荐阅读