无法声明 MonadPlus 接口受 Monad 约束

【问题标题】：Failed to declare MonadPlus interface constrained on Monad无法声明 MonadPlus 接口受 Monad 约束
【发布时间】：2020-08-01 15:11:29
【问题描述】：

我正在尝试这样声明 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 界面，我说得对吗？如果有，为什么？

【问题讨论】：

标签： monads idris

【解决方案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 中是否存在。

【讨论】：