问题描述
我正在尝试使用 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