[Agda] Any examples of monad use in Agda?

[jleivent at comcast.net]

Does anyone know where I can find some examples of monad usage in Agda, not just monad definitions?

I am having some difficulty with a monad I defined, especially when I fmap a function that produces a type: given f : A -> Set, and ma : M A, do fmap f ma, and get a useable result, meaning a type that can be used to declare things.

It seems like I need a strange monadic function like this: setout : M Set -> Set, such that forall (A : Set) -> setout (return A) == M A.  With this I can do the following:

  q : setout (fmap f ma)


Also, I have found a particular dependent variety of bind to be helpful:

bind== : {A : Set} -> (ma : M A) -> (f : (a : A) -> ma == return a -> MB) -> MB

meaning that the function f gets both the value in the monad and an equality proof tying that value back to the monadic input.

But, I'm not sure if or why I should need either setout or bind==.  Certainly neither is definable from return and normal bind alone.  And the apparent need for them is independent of the computation in the monad.