How to determine whether a dependent type that doesn't fit the monad instance is categorically a monad

[Using Idris syntax and terminology, but the question is not about Idris]

If a monad interface (or type class) has a constraint requiring applicative functor, a monad instance can be written by implementing either bind: (>>=) : Monad m => m a -> (a -> m b) -> m b, or join : Monad m => m (m a) -> m a, or both. However, this is a much more constrained and specific type of monad than the general concept of monad in category theory.

In a dependently typed language, it is not uncommon to stick some kind of size into the type in order to allow the typechecker to recognize well-founded recursion, etc. The unfortunate impact is that because bind and join may not be size-preserving operations, you can loose your monad instance, and thus not be able to use whatever syntactic sugar the language may provide, etc. That's okay though; let's set that aside. What I'm wondering more fundamentally is if you've only lost your instance of Monad, or if your type has actually stopped being a monad. If you have a type k : Nat -> Type -> Type, might not pure : a -> k n a and (>>=) : k n a -> (a -> k m b) -> k (op n m) b / join : k n (k m a) -> k (op n m) a still satisfy the conditions to be a monad for some op : Nat -> Nat -> Nat, e.g. +?

I'll give a specific example: a freer monad indexed by size in order to allow for total operations.

```
||| http://okmij.org/ftp/Computation/free-monad.html
module Freer

%default total
%access public export

data FFree : (Type -> Type) -> Nat -> Type -> Type where
FPure : a -> FFree g n a
FImpure : g x -> (x -> FFree g n a) -> FFree g (S n) a

Functor (FFree g n) where
map f (FPure x) = FPure (f x)
map f (FImpure u q) = FImpure u (map f . q)

pure : a -> FFree g n a
pure = FPure

promote : {m : Nat} -> FFree g n a -> FFree g (n + m) a
promote (FPure x) = FPure x
promote (FImpure u q) = FImpure u (promote . q)

assocS : (m : Nat) -> (n : Nat) -> m + S n = S (m + n)
assocS Z n = Refl
assocS (S m) n = cong $ assocS m

So, there are potentially many answers to this sort of question. One is that there are many possible categories on which there can be monads. The rules for establishing that something is a monad will ultimately be the same, but the details will differ depending on the specific category chosen. So, since there is a natural number index involved, perhaps a monad on a category of natural number indexed types is in order, although your presentation is not precisely that. Or, perhaps you can also quantify over the natural number to get a monad that is the 'total space' of all the individual fibers. (It's also not clear to me why you need the index in this example, unless Idris has a feature that makes the type small because of it.)

However, another answer is that whether something 'is a monad' is kind of the wrong thing to worry about. Especially with examples like this, what is going on is that we are constructing the 'free algebra' of some embedded language we want to work with. Monads show up because they are one of the ways that algebra is dealt with in category theory. So because we're doing algebra, we can phrase it in terms of (a particular construction of certain) monads. But it can also be presented it in other ways as well.

The presentation you're using originates in Haskell (I think), and it's convenient there, because of impredicativity and no concern for logical consistency/termination. You can easily write down the, 'free monad over a type operator.' It's also convenient because Haskell has features that make things presented as Monad nicer to use than other presentations.

However, if Idris is not (as) accepting of definitions like that, it seems sensible to re-evaluate whether some other presentation that is accepted can encode all the things you want. For instance, there are ways of specifying strictly positive functors in more obvious ways, which give rise to e.g. W-types:

data W (A : Type) (B : A → Type) : Type where
  con : (a : A) → (y : B a → W A B) → W A B

and it's possible to construct free monads based on this:

data Free (A : Type) (B : A → Type) (X : Type) : Type where
  pure : X → Free A B X
  branch : (a : A) → (B a → Free A B X) → Free A B X

This is the free monad over the polynomial functor given by A and B (the A-fold sum of B a-fold products of X). But this is by no means the only option.

So, it seems to me that unless there is some syntax sugar or similar reason to prefer a particular solution (or you have other reasons), it's better to worry about whether you have built the algebraic structure you wanted in a way that is easy to use for whatever you actually wanted to use it for, and not whether it adheres to some particular way of doing it that works well in a different language.

And to loop around, if the size is just there for getting everything to termination check, maybe it also doesn't matter if it's any actual notion of monad from category theory. If you erased the sizes and it fit the definition of a normal monad, and the sizes are only there for book keeping, maybe that's good enough (as long as it doesn't obstruct you in more practical ways).

StackExchange Computer Science Q#97808, answer score: 4