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

本文介绍了无法声明受 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.