Не удалось объявить интерфейс MonadPlus, ограниченный для Monad

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)

Что я делаю не так? Как это исправить? Я прав, что у Идриса нет собственного интерфейса MonadPlus? Если да, то почему?

Answer 1

В Идрисе, когда вы определяете интерфейс, тип параметра по умолчанию равен Type, поэтому MonadPlus m здесь является сокращением от MonadPlus (m: Type), а Идрис рассматривает m как Type. Это, конечно, не соответствует ограничению Monad m, которое ожидает Type -> Type.

Вы должны быть явным, если хотите параметризовать что-то еще, например

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

* 1012 Сам *MonadPlus мне неизвестен, поэтому я не знаю о его наличии или отсутствии в Идрисе.