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 n
apply : FFree g n (a -> b) -> FFree g m a -> FFree g (m + n) b
apply {n} {m} (FPure f) x =
promote $ map f x
apply {n=S n} {m} (FImpure u q) x =
let y = flip apply x . 904
q
in rewrite assocS m n in FImpure u y
bind : (a -> FFree g n b) -> FFree g m a -> FFree g (n + m) b
bind {n} {m} f (FPure x) = promote $ f x
bind {n} {m=S m} f (FImpure u f') =
let y = bind f . f'
in rewrite assocS n m in FImpure u y
join : FFree g m (FFree g n a) -> FFree g (n + m) a
join = bind id
This allow my monad methods to be total for my freer monad. But... is it still a valid monad? I do not see why adding some typelevel information would stop it from being one; other than some typelevel fanciness in the form of rewrite ... in ... etc. the method implementations are the same as those given in the "Freer Monads, More Extensible Effects" paper. However, I am used to seeing the monad laws written in terms of Monad, which I am no longer able to implement here since e.g. Free g 3 ≠ Free g 2.
How do I prove or disprove that, Monad interface and syntactic sugar aside, I still have a monad here? 875