无法声明在Monad上约束的MonadPlus接口

Question

我尝试这样声明MonadPlus接口：

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接口，我说的对吗？如果有，原因何在？

Answer 1

在Idris中，当您定义接口时，参数类型默认为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中的存在或缺失。