monads - 无法声明 MonadPlus 接口(interface)受 Monad 约束

Question

我试图像这样声明 MonadPlus 接口(interface):

module NanoParsec.Plus

%access public export

interface Monad m => MonadPlus m where
    zero : m a
    plus : m a -> m a -> m a

但是有一个错误:

  |
5 | interface Monad m => MonadPlus m where
  |           ~~~~~~~
When checking type of constructor of NanoParsec.Plus.MonadPlus#Monad m:
When checking argument m to type constructor Prelude.Monad.Monad:
        Type mismatch between
                Type (Type of m)
        and
                Type -> Type (Expected type)

我做错了什么？如何解决这个问题？ Idris 没有自己的 MonadPlus 接口(interface)，我说得对吗？如果是这样，为什么？

Answer 1

在Idris中，定义接口(interface)时，参数类型默认为Type，所以这里的MonadPlus m是MonadPlus (m: Type)的简写，Idris 将 m 视为 Type。这当然不符合 Monad m 约束，它需要一个 Type -> Type。

如果你想参数化其他东西，比如

，你必须明确

interface Monad m => MonadPlus (m: Type -> Type) where
    zero : m a
    plus : m a -> m a -> m a

MonadPlus 本身超出了我的知识范围，所以我不知道它在 Idris 中是否存在。