小编Hei*_*ell的帖子

因此,Functor制作1-1逻辑数据流 - a Lens.所述Applicative使得n-1个数据流的逻辑-一个Traversal.在Applicative上Choice Profunctor使得"打破部分"机制-一个Prism.

有没有涉及任何有趣的已知结构Monad,MonadPlus等功能或一些其他子集Profunctors？

我有这些类型的家庭：

type family xs ++ ys where
  '[]      ++ ys = ys
  (x : xs) ++ ys = x : (xs ++ ys)

type family Drop n xs where
  Drop  O         xs  = xs
  Drop (S n) (_ : xs) = Drop n xs

type family Length xs where
  Length '[] = O
  Length  (x : xs) = S (Length xs)

在某些时候，GHC 想要证明

forall a. Drop (Length a) (a ++ c) ~ c

我曾经把它推到一些构造函数的上下文中。

我如何普遍证明这个属性？