无法声明受 Monad 约束的 MonadPlus 接口

问题描述

我正在尝试像这样声明 MonadPlus 接口:

I'm trying to declare MonadPlus interface like that:

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 接口是对的吗?如果是，为什么?

What I'm doing wrong? How to fix this? Am I right that Idris has no its own MonadPlus interface? If so, why?

推荐答案

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

In Idris, when you define an interface, the parameter type defaults to Type, so MonadPlus m here is short for MonadPlus (m: Type), and Idris treats m as a Type. This of course doesn't fit with the constraint Monad m, which expects a Type -> Type.

如果你想参数化其他东西，你必须明确，比如

You have to be explicit if you want to parametrize over something else, like

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

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

MonadPlus itself is beyond my knowledge so I don't know about its presence, or lack thereof, in Idris.

这篇关于无法声明受 Monad 约束的 MonadPlus 接口的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！